z3 - 是否有可能在 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

据我所知，您关于最后一个方程不一致的断言与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。