Z3求解方程如何使用

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) )