StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

POContext.MkSolver() Changes between Z3 versions 4.1 and 4.3
text
Body
copied!<p>Recently I was upgrading an application that uses the .NET API from Z3 version 4.1 to version 4.3. However, I noticed there has been a change in <code>MkSolver()</code> that now causes some of my queries that returned <code>unsat</code> in 4.1 to now return <code>unknown</code> in 4.3. In particular, I had been using the <code>Context</code> option <code>ELIM_QUANTIFIERS</code> set to true, which has been deprecated according to an error message I receive when trying to use the solver:</p> <p><code>QUANT_ELIM option is deprecated, please consider using the 'qe' tactic.</code></p> <p>Without this option enabled, some of my queries may receive unknown. I have tried using a variety of tactics in 4.3, including the quantifier elimination <code>qe</code>, but unfortunately, I have not been able to figure out an equivalent set of tactics to what MkSolver in Z3 4.1 created. For example, the following does not work (i.e., I still get unknown in 4.3 for queries that I got unsat for in 4.1):</p> <pre><code>Context z3 = new Context(); Params p = z3.MkParams(); p.Add("produce-models", true); p.Add("candidate-models", true); p.Add("mbqi", true); p.Add("auto-config", false); p.Add("ematching", true); p.Add("pull-nested-quantifiers", true); Tactic tqe = z3.With(z3.MkTactic("qe"), p); Tactic tsmt = z3.With(z3.MkTactic("smt"), p); Tactic t = z3.Repeat(tqe, tsmt); Solver s = t.Solver; ... // assert and check assertions </code></pre> <p>If there is an equivalent solver-tactic in 4.3 to what <code>MkSolver</code> created in 4.1, what is it or how can I go about figuring it out? I used a variety of other context options in 4.1, which I have tried to use in the appropriate tactics in 4.3, such as: <code>MBQI = true</code>, <code>AUTO_CONFIG = false</code>, <code>ELIM_NLARITH_QUANTIFIERS = true</code>, <code>EMATCHING = true</code>, <code>MACRO_FINDER = true</code>, <code>PI_PULL_QUANTIFIERS = true</code>, <code>PULL_NESTED_QUANTIFIERS = true</code>, <code>DISTRIBUTE_FORALL = true</code>, and <code>PULL_NESTED_QUANTIFIERS = true</code>.</p> <p>Here is an example query that now returns <code>unknown</code>, which previously returned <code>unsat</code> (note that it is unsat only with some additional assertions, which are quite long, but this is the format of the assertion that now gives unknown. Here <code>LB</code>, <code>LS</code>, <code>vmin</code>, and <code>vmax</code> are all real constants [with assertions equating them to constant values, e.g., <code>LS = 7</code>], and <code>q</code> is a function from integers to bitvectors, <code>x</code> is a function from integers to reals, <code>next</code> is a function from integers to integers, and <code>last</code> is an integer, and likewise for their primed versions; also, note that part of it is nonlinear, e.g., <code>delta * t_1</code> and <code>delta * t_2</code>):</p> <pre><code>(set-option :auto-config false) ;(set-option :elim-quantifiers true) (set-option :elim-nlarith-quantifiers true) (set-option :mbqi true) (set-option :produce-models true) (set-option :proof-mode 1) (declare-const LB Real) (declare-const LS Real) (declare-const vmin Real) (declare-const vmax Real) (declare-const Base (_ BitVec 2)) (declare-const N Int) (declare-fun q (Int) (_ BitVec 2)) (declare-fun |q'| (Int) (_ BitVec 2)) (declare-fun x (Int) Real) (declare-fun |x'| (Int) Real) (declare-fun next (Int) Int) (declare-fun |next'| (Int) Int) (declare-const last Int) (declare-const |last'| Int) (declare-const t_1 Real) (declare-const t_2 Real) (declare-const delta Real) (assert (= Base #b01)) (assert (= vmin 1.0)) (assert (= vmax 2.0)) (assert (= LS 7.0)) (assert (= LB 28.0)) (assert (not (=> (and (forall ((i Int) (j Int)) (=> (and (>= i 1) (<= i N) (>= j 1) (<= j N)) (=> (and (not (= i j)) (= (q i) Base) (= (q j) Base) (= (next j) i)) (>= (- (x i) (x j)) LS)))) (exists ((t_1 Real)) (and (>= t_1 0.0) (forall ((h Int)) (=> (and (>= h 1) (<= h N)) (and (exists ((delta Real)) (forall ((t_2 Real)) (=> (and (>= t_2 0.0) (<= t_2 t_1)) (and true true (or (not (= (q h) Base)) (and (<= (+ (x h) (* delta t_2)) LB) (or (not (>= (+ (x h) (* delta t_2)) LB)) (= t_1 t_2)) (= (|x'| h) (+ (x h) (* delta t_1))) (>= delta vmin) (<= delta vmax))) true)))) (= (q h) (|q'| h)) (= (next h) (|next'| h)) (= last |last'|))))))) (forall ((i Int) (j Int)) (or (not (and (>= i 1) (<= i N) (>= j 1) (<= j N))) (not (and (not (= i j)) (= (|q'| i) Base) (= (|q'| j) Base) (= (|next'| j) i))) (>= (+ (|x'| i) (* (- 1.0) (|x'| j))) LS)))))) (check-sat) ; toggles between unknown and sat when toggling elim-nlarith-quantifiers </code></pre> <p>Essentially, I'd like to create the tactic-solver corresponding to whatever solver is being used here, as this toggling behavior is what I was seeing in 4.1, but don't see in 4.3, since I can't use ELIM_QUANT via Context options anymore. </p>

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