SMT:检查功能的唯一性和整体性 [英] SMT: check uniqueness and totality of function

问题描述

Give 是一个函数及其行为的描述:

Given is a function and a description of its behavior:

add: (ℤ ∪ {Error, None})² → (ℤ ∪ {Error, None})

For x ∈ (ℤ ∪ {Error, None}):
add(x, None) = add(None, x) = None

For x ∈ (ℤ ∪ {Error}):
add(x, Error) = add(Error, x) = Error

For x, y ∈ ℤ:
add(x, y) = x + y

如何将此描述转换为 SMT(我使用的是 Z3)并检查该描述是否定义了一个完整的功能?

How can I transform this description to SMT (I'm using Z3) and check whether the description defines a total function?

为了让您了解我想要实现的目标:最后，我想生成以最少分支数实现此功能的 Python 代码.例如:

To give you an idea what I want to achieve: in the end I want to generate Python code implementing this function with the minimum number of branches. For example:

def add(x, y):
    if x is None or y is None:
        return None
    if x is Error or y is Error:
        return Error
    return x + y

这是我目前尝试过的:

(declare-datatypes () ((ABC (int (val Int)) error none)))
(declare-fun f (ABC ABC) ABC)
(assert (forall ((x ABC)) (=> (or (is-int x) (= x error) (= x none)) (= (f none x) none))))
(assert (forall ((x ABC)) (=> (or (is-int x) (= x error) (= x none)) (= (f x none) none))))
(assert (forall ((x ABC)) (=> (or (is-int x) (= x error)) (= (f error x) error))))
(assert (forall ((x ABC)) (=> (or (is-int x) (= x error)) (= (f x error) error))))
(assert (forall ((x ABC) (y ABC)) (=> (and (is-int x) (is-int y)) (= (f x y) (int (+ (val x) (val y)))))))
(check-sat)
(get-model)

此超时.

在简化模型中的函数解释中，我描述了一个更简单的 f 公理化其中 int 是单个案例，导致有限多个案例.我能否以某种方式告诉 Z3，int 中的具体 val 无关紧要，并且实际上有很多情况?

In Simplify function interpretation in model I described a simpler axiomatization of f where int is a single case, resulting in finitely many cases. Can I somehow tell Z3 that the concrete val in int doesn't matter and there are effectively finitely many cases?

推荐答案

检查唯一性:你的公理化是好的；您只需要为两个函数复制"它，然后要求两个值使它们不同:

To check uniqueness: Your axiomatization is good; you just need to "replicate" it for two functions then ask for two values such that they differ:

(declare-datatypes () ((ABC (int (val Int)) error none)))

(declare-fun f (ABC ABC) ABC)
(assert (forall ((x ABC)) (=> (or (is-int x) (= x error) (= x none)) (= (f none x) none))))
(assert (forall ((x ABC)) (=> (or (is-int x) (= x error) (= x none)) (= (f x none) none))))
(assert (forall ((x ABC)) (=> (or (is-int x) (= x error)) (= (f error x) error))))
(assert (forall ((x ABC)) (=> (or (is-int x) (= x error)) (= (f x error) error))))
(assert (forall ((x ABC) (y ABC)) (=> (and (is-int x) (is-int y)) (= (f x y) (int (+ (val x) (val y)))))))

(declare-fun g (ABC ABC) ABC)
(assert (forall ((x ABC)) (=> (or (is-int x) (= x error) (= x none)) (= (g none x) none))))
(assert (forall ((x ABC)) (=> (or (is-int x) (= x error) (= x none)) (= (g x none) none))))
(assert (forall ((x ABC)) (=> (or (is-int x) (= x error)) (= (g error x) error))))
(assert (forall ((x ABC)) (=> (or (is-int x) (= x error)) (= (g x error) error))))
(assert (forall ((x ABC) (y ABC)) (=> (and (is-int x) (is-int y)) (= (g x y) (int (+ (val x) (val y)))))))

; check that there is no {x,y} such that f and g differ on:
(declare-const x ABC)
(declare-const y ABC)
(assert (not (= (f x y) (g x y))))

(check-sat)
(get-model)

Z3为此迅速返回unsat；意味着 f 和 g 不能不同.现在，您可以尝试注释掉 f 和/或 g 的一些断言并请求一个模型.根据您注释掉的断言，Z3 可能会为 f 和 g 提出一个模型，使它们具有不同的行为；OR 它仍然可以超时，尝试构建一个模型来这样做.在存在量词的情况下，您真的不能指望 SMT 求解器有更好的表现.

Z3 quickly returns unsat for this; meaning f and g cannot differ. Now, you can try commenting out some of the asserts for f and/or g and ask for a model. Depending on which asserts you comment out, Z3 might come up with a model for f and g such that they have different behavior; OR it can still time-out, trying to construct a model to do so. In the presence of quantifiers, you can't really expect anything better from an SMT solver.

这篇关于SMT:检查功能的唯一性和整体性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！