Z3 Solver 超时与抽象环答案

【问题标题】：Z3 Solver timing out with abstract ringZ3 Solver 超时与抽象环
【发布时间】：2018-08-21 02:19:40
【问题描述】：

我正在尝试使用 Z3 求解器定义一个抽象的半环，但是每当我尝试使用该环执行任何操作时，求解器似乎永远运行。

目前我有以下 Z3 smt 代码：

; declare the ring elements
(declare-sort R)

(declare-fun add (R R) R)
(declare-fun mul (R R) R)

(declare-fun one () R)
(declare-fun zero () R)

; the add properties
(assert (forall ((a R)) (= (add a zero) a)))
(assert (forall ((a R) (b R)) (= (add a b) (add b a))))
(assert (forall ((a R) (b R) (c R)) (= (add (add a b) c) (add a (add b c)))))

; the multiply properties
(assert (forall ((a R)) (= (mul a one) a)))
(assert (forall ((a R)) (= (mul a zero) zero)))
(assert (forall ((a R) (b R)) (= (mul a b) (mul b a))))
(assert (forall ((a R) (b R) (c R)) (= (mul (mul a b) c) (mul a (mul b c)))))

; distributive
(assert (forall ((a R) (b R) (c R)) (= (mul a (add b c)) (add (mul a b) (mul a c)))))

; different elements
(assert (distinct zero one))

; Either of the following blocks on their own cause the solver to run seemingly forever
(declare-fun fubar () R)
(assert (= fubar (mul fubar one)))

(assert (= zero (mul zero one)))



(set-option :timeout 100000)
(check-sat)
(get-model)

【问题讨论】：

第一步，向量词添加显式触发器，以减少导致匹配循环的可能性。检查量词统计信息或使用 Axiom Profiler (bitbucket.org/viperproject/axiom-profiler) 查看匹配循环是否可以解释您观察到的较差性能。

标签： z3

【解决方案1】：

由于大量使用量词，我非常怀疑 Z3 是否适合这类问题。有限模型查找和电子匹配并不容易。也许好的旧定理证明在这里可能是更好的选择，或者至少对基数非常明确，因此可以删除量化。（诚然，这仅适用于小型域。）

【讨论】：