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 MkSolver() that now causes some of my queries that returned unsat in 4.1 to now return unknown in 4.3. In particular, I had been using the Context option ELIM_QUANTIFIERS set to true, which has been deprecated according to an error message I receive when trying to use the solver:
QUANT_ELIM option is deprecated, please consider using the 'qe' tactic.
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 qe, 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):
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
If there is an equivalent solver-tactic in 4.3 to what MkSolver 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: MBQI = true, AUTO_CONFIG = false, ELIM_NLARITH_QUANTIFIERS = true, EMATCHING = true, MACRO_FINDER = true, PI_PULL_QUANTIFIERS = true, PULL_NESTED_QUANTIFIERS = true, DISTRIBUTE_FORALL = true, and PULL_NESTED_QUANTIFIERS = true.
Here is an example query that now returns unknown, which previously returned unsat (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 LB, LS, vmin, and vmax are all real constants [with assertions equating them to constant values, e.g., LS = 7], and q is a function from integers to bitvectors, x is a function from integers to reals, next is a function from integers to integers, and last is an integer, and likewise for their primed versions; also, note that part of it is nonlinear, e.g., delta * t_1 and delta * t_2):
(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
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.