是否有可能在 Z3 中或在传递到 Z3 之前检测到不一致的方程？

Question

我正在使用 z3 使用以下示例。

f=Function('f',IntSort(),IntSort())
n=Int('n')
c=Int('c')
s=Solver()
s.add(c>=0)
s.add(f(0)==0)
s.add(ForAll([n],Implies(n>=0, f(n+1)==f(n)+10/(n-c))))

最后一个等式不一致（因为 n=c 会使它不确定）。但是，Z3 无法检测到这种不一致。有什么方法可以让 Z3 检测到它，或者任何其他可以检测到它的工具？

Answer 1

据我所知， 你断言最后一个方程 不一致 与 [=28 的文档不符=]SMT-LIB 标准。页面 Theories: Reals 说：

Since in SMT-LIB logic all function symbols are interpreted as total functions, terms of the form (/ t 0) are meaningful in every instance of Reals. However, the declaration imposes no constraints on their value. This means in particular that

for every instance theory T and

for every value v (as defined in the :values attribute) and closed term t of sort Real,

there is a model of T that satisfies (= v (/ t 0)).

同样，页面 Theories: Ints 说：

See note in the Reals theory declaration about terms of the form (/ t 0).

The same observation applies here to terms of the form (div t 0) and (mod t 0).

因此，有理由相信 SMT-LIB 兼容工具永远不会为给定的公式打印 unsat。

Answer 2

Z3 不检查是否被零除，因为正如 Patrick Trentin 提到的那样，根据 SMT-LIB，被零除的语义是 returns 一个未知值。

您可以手动要求 Z3 检查是否被零除，以确保您永远不会依赖被零除。（这很重要，例如，如果您正在建模一种语言，其中被零除具有与 SMT-LIB 不同的语义。）

对于您的示例，这将如下所示：

(declare-fun f (Int) Int)

(declare-const c Int)

(assert (>= c 0))

(assert (= (f 0) 0))

; check for division by zero
(push)
(declare-const n Int)
(assert (>= n 0))

(assert (= (- n c) 0))
(check-sat)  ; reports sat, meaning division by zero is possible
(get-model)  ; an example model where division by zero would occur
(pop)

;; Supposing the check had passed (returned unsat) instead, we could
;; continue, safely knowing that division by zero could not happen in
;; the following.
(assert (forall ((n Int)) 
                (=> (>= n 0) 
                    (= (f (+ n 1)) 
                       (+ (f n) (/ 10 (- n c)))))))

是否有可能在 Z3 中或在传递到 Z3 之前检测到不一致的方程？

Is it possible to detect inconsistent equations in Z3, or before passing to Z3?

solver

divide-by-zero

smt

z3