Z3解決當量如何使用

Question

我想了解如何使用解決當量，我預計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)) 

我可以指定什麼varibales應該簡化？任何其他的風格都可以完成這項工作？

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