Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

prevent solution from being simplified

Tags:

z3

I want to the solution got back from z3 without simplification using let statements.

For example if I give the following:

(declare-const x Int)
  (elim-quantifiers (exists ((x.1 Int)) 
    (and (or (and (= (- x.1 2) 0) (<= (- x.1 9) 0)) 
             (and (or (= (- x.1 2) 0) (and (<= (- x.1 4) 0) 
                                      (and (<= (- 4 x.1) 0) 
                                           (<= (- x.1 11) 0)))) (<= (- x.1 9) 0))) (= (- (+ x.1 2) x) 0))))

I get back the solution as:

(let ((a!1 (and (or (and (<= x 4) (>= x 4)) (and (<= x 6) (>= x 6) (<= x 13)))
                (<= x 11))))
    (or (and (<= x 4) (>= x 4) (<= x 11)) a!1))

Is there a way to tell Z3 not to extract some complex expressions into a let statement ? It will be easier for me to parse the result if I get the answer flat without let statement.

like image 265
sriraj Avatar asked Nov 19 '12 22:11

sriraj


1 Answers

We can set the following options to prevent the Z3 pretty printer from using lets

(set-option :pp-min-alias-size 1000000)
(set-option :pp-max-depth      1000000)

Any big number will do the trick.

We have to keep in mind that it may not be feasible to display some formulas that contain a lot of shared sub-expressions when we avoid the lets. Internally, Z3 stores the formulas as DAGs instead of Trees. If we do not use the lets, the pretty-print of such formulas may be exponentially bigger than their internal representation. So, we should not abuse the options above.

like image 189
Leonardo de Moura Avatar answered Oct 06 '22 22:10

Leonardo de Moura