z3 - Z3solve-eq如何使用

Question

我正在尝试了解如何使用solve-eq，我希望Z3能够解决这个问题

(declare-const mem (Array Int Int))
(declare-const adr_a Int)
(declare-const a Int)
(assert (= (select mem adr_a) a))
(assert (<= 0 (select mem adr_a)))
(apply solve-eqs)

进入

(<= 0 a)

但我得到了

(<= 0 (select mem adr_a))

我可以指定应该简化哪些变量吗？任何其他策略可以完成这项工作吗？

Answer 1

简单的例子：

(declare-const a Int)
(declare-const b Int)
(assert (= b a))
(assert (<= 0 b))
(apply solve-eqs)

输出是：

(goals (goal (<= 0 a) :precision precise :depth 1) )