CODEWITHSUNDEEP
z3smt
user1487718
user1487718

Reputation:

how to simplify the result of hiding variable using z3?

I wish to hide some variables and get the simplified results.

I wish to hide c1, c2 and d as follows:

(declare-const v1 Real)
(declare-const v2 Real)
(elim-quantifiers (exists ((c1 Real) (c2 Real)(d Real)) 
                          (and (<= c1 10.0) (>= c2 5.0) (>= d 0.0) 
                               (= v1 (+ c1 d)) 
                               (= v2 (+ c2 d)))))

However the result seems complex, in fact, the result should be v2>=5.0 & v1<= v2+5.0, I used to use (apply ctx-solver-simplify) the code is 

(declare-const v1 Real)
(declare-const v2 Real)
(assert (elim-quantifiers (exists ((c1 Real) (c2 Real)(d Real)) 
                                  (and (<= c1 10.0) (>= c2 5.0) (>= d 0.0)
                                       (= v1 (+ c1 d)) 
                                       (= v2 (+ c2 d))))))
(apply ctx-solver-simplify)

However, when I add apply ....There is and error,the script can not work. could someone help me to fix it?

Upvotes: 0

Views: 185

Answers (1)

pad
pad

Reputation: 41290

You can use then tactic to apply quantifier elimination to the formula and apply context simplification to all sub-goals produced:

(declare-const v1 Real)
(declare-const v2 Real)
(assert (exists ((c1 Real) (c2 Real)(d Real)) 
                                  (and (<= c1 10.0) (>= c2 5.0) (>= d 0.0)
                                       (= v1 (+ c1 d)) 
                                       (= v2 (+ c2 d)))))
(apply (then qe ctx-solver-simplify))

The result is v2 >= 5.0 and v1 - v2 <= 5.0 which is quite close to what you want.

Upvotes: 2

Related Questions