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

Могу ли я указать, какие варибалы должны быть упрощены? любая другая тактика могла бы выполнить эту работу?

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