z3 中未解释的 int 常量

Question

是否可以在 z3 中将 int 常量视为未解释？例如，将 tuple(project(t, 0), project(t, 1)) = t 视为 tuple(project(t, left), project(t, right)) = t。上下文：我的方程基本上在 QF_UF 中，但因为它们包含 int 常量，所以我不得不使用带有整数运算的逻辑，这有时会导致不终止。

Answer 1

您可以将 Int 声明为未解释的排序，只要您将逻辑设置为尚未定义的逻辑即可：

(set-logic QF_UF)

(declare-sort Int 0)
(declare-fun f ((Int)) Int)

(declare-fun i () Int)
(assert (distinct (f i) (f i)))
(check-sat)

z3 说：

unsat

如果您添加：

(assert (= (f 2) 2))

然后你得到：

(error "line 8 column 15: Sort mismatch at argument #1 for function (declare-fun f (Int) Int) supplied sort is Int")

这样可以避免混淆。（尽管错误消息读起来相当混乱！）

如果您将逻辑设置为：

(set-logic QF_LIA)

然后 z3 说：

(error "line 3 column 18: sort already defined Int")

所以，这也行。有关详细信息，请参阅 SMTLib specification 的第 4.2.3 节。

希望对您有所帮助！

z3 中未解释的 int 常量

Uninterpreted int Constants in z3

z3