z3 - 超时原因？

Question

我是使用 Z3 的新手。但我想了解，在输入到Z3的以下程序中超时的原因：

(declare-fun ADDR (Int) Int)
(declare-fun STAR (Int Int) Int)
(declare-fun VAR (Int Int) Int)
(declare-const error Int)

(assert (forall ((x Int)) (= x (STAR (ADDR x) 0))) );causes a timeout?
(assert (forall ((x Int)) (>= (ADDR x) 4000)) )
(assert (not (= (VAR  error 0) 1)))
(check-sat)
(get-model)

我的另一个问题是，forall 3.2 版有什么新东西吗？我必须在 (x Int) 周围加上额外的括号，否则会引发错误。

谢谢。

Answer 1

这个公式是可满足的，Z3 没能为其建立模型。如果禁用量化公式的模型查找器，则可以避免超时。

(set-option :auto-config false)
(set-option :mbqi false)

如果您这样做，Z3 将返回未知和“候选模型”。Z3 指南中讨论了这个问题。

因为 Z3 3.x 完全兼容SMT 2.0 标准，所以需要额外的括号。