StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>You can currently use integers to encode PB constraints. You have to bound the variables to be in the interval 0, 1. For example:</p> <pre><code> (set-logic QF_LIA) (declare-const n1 Int) (declare-const n2 Int) (assert (<= 0 n1)) (assert (<= n1 1)) (assert (<= 0 n2)) (assert (<= n2 1)) (assert (>= (+ n1 n2) 1)) (check-sat) </code></pre> <p>If you set the logic to QF_LIA, then Z3 will automatically try to re-encode these constraints using bit-vectors. In the verbose output you will see that Z3 invokes a tactic pb2bv that does the rewriting for you</p> <pre><code>z3 ty.smt2 /v:10 (simplifier :num-exprs 10 :num-asts 171 :time 0.00 :before-memory 0.77 :after-memory 0.77) (propagate-values :num-exprs 10 :num-asts 171 :time 0.00 :before-memory 0.77 :after-memory 0.77) (ctx-simplify :num-steps 17) (ctx-simplify :num-exprs 10 :num-asts 171 :time 0.00 :before-memory 0.77 :after-memory 0.77) (simplifier :num-exprs 10 :num-asts 171 :time 0.00 :before-memory 0.77 :after-memory 0.77) (solve_eqs :num-exprs 10 :num-asts 171 :time 0.00 :before-memory 0.77 :after-memory 0.77) (elim-uncnstr-vars :num-exprs 10 :num-asts 171 :time 0.00 :before-memory 0.77 :after-memory 0.77) (simplifier :num-exprs 10 :num-asts 173 :time 0.00 :before-memory 0.77 :after-memory 0.77) (pb2bv :num-exprs 4 :num-asts 180 :time 0.00 :before-memory 0.77 :after-memory 0.77) (simplifier :num-exprs 3 :num-asts 178 :time 0.00 :before-memory 0.77 :after-memory 0.77) (propagate-values :num-exprs 3 :num-asts 178 :time 0.00 :before-memory 0.77 :after-memory 0.77) (solve_eqs :num-exprs 3 :num-asts 178 :time 0.00 :before-memory 0.77 :after-memory 0.77) (max-bv-sharing :num-exprs 3 :num-asts 178 :time 0.00 :before-memory 0.77 :after-memory 0.77) (bit-blaster :num-exprs 3 :num-asts 178 :time 0.00 :before-memory 0.77 :after-memory 0.77) (aig :num-exprs 3 :num-asts 178 :time 0.00 :before-memory 0.77 :after-memory 0.77) (ast-table :capacity 640 :size 178) (sat-status :inconsistent false :vars 2 :elim-vars 0 :lits 2 :assigned 0 :binary-clauses 1 :ternary-clauses 0 :clauses 0 :del-clause 0 :avg-clause-size 2.00 :memory 0.77) </code></pre>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload