CODEWITHSUNDEEP
z3smtsat
DvH
DvH

Reputation: 41

trying an example from rise4fun / z3 / tutorial / strategies

some example from the rise4fun-site:

(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(declare-const a Int)        ;  this is added

(assert (= a 3 ))            ; this is added:  a := 3
(assert (< 0 x  10))         ; rewritten, but same constraint
(assert (< 0 y  10))
(assert (< 0 z  10))

(assert (= (+ (* 3 y) (* 2 x)) z))        ; plain function from rise4fun
;(assert (= (+ (* a y) (* 2 x)) z))       ; here literal 3 is replaced by a

(check-sat-using (then (using-params simplify :arith-lhs true :som true)
                       normalize-bounds
                       lia2pb
                       pb2bv
                       bit-blast
                       sat))
(get-model)
(get-info :version)

when i comment the plain function from rise4fun and uncomment my function, the solver will fail to produce a result and respond with 'unknown' (tried with 4.8.0). Isn't the solver or some preprocessor smart enough to see that 'a' is just a constant with fixed value 3?

Upvotes: 1

Views: 181

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8393

That's right, the simplify tactic is not smart enough to propagate values because it would be too expensive in general. However, ctx-simplify or propagate-values do the job. For instance:

(check-sat-using (then (using-params simplify :arith-lhs true :som true)
                       propagate-values
                       normalize-bounds
                       lia2pb
                       pb2bv
                       bit-blast
                       sat))

Upvotes: 1

Related Questions