最近、.NET API を使用するアプリケーションを Z3 バージョン 4.1 からバージョン 4.3 にアップグレードしていました。ただし、 4.1MkSolver()で返されたクエリの一部が4.3 で返されるようになったという変更があることに気付きました。特に、私は true に設定されたオプションを使用していましたが、ソルバーを使用しようとしたときに受け取ったエラー メッセージに従って廃止されました。unsatunknownContextELIM_QUANTIFIERS
QUANT_ELIM option is deprecated, please consider using the 'qe' tactic.
このオプションを有効にしないと、クエリの一部が不明を受け取る場合があります。私は 4.3 で量指定子の除去を含むさまざまな戦術を使用してみましたqeが、残念ながら、Z3 4.1 の MkSolver が作成したものと同等の一連の戦術を見つけることができませんでした。たとえば、以下は機能しません (つまり、4.1 で unsat になったクエリに対して、4.3 でも unknown になります)。
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
4.1 で作成されたものと同等のソルバー戦術が 4.3 にある場合MkSolver、それは何ですか、またはそれを理解するにはどうすればよいですか? 4.1 ではさまざまなコンテキスト オプションを使用しましたがMBQI = true、 4.3AUTO_CONFIG = falseでは適切な戦術で使用しようとしました。ELIM_NLARITH_QUANTIFIERS = trueEMATCHING = trueMACRO_FINDER = truePI_PULL_QUANTIFIERS = truePULL_NESTED_QUANTIFIERS = trueDISTRIBUTE_FORALL = truePULL_NESTED_QUANTIFIERS = true
unknown以前に返された を返すクエリの例を次に示しますunsat(非常に長いアサーションがいくつか追加されているだけで unsat であることに注意してください。ただし、これは現在不明を返すアサーションの形式です。ここLBで、LS、vmin、およびvmaxはすべて実数です。定数 [それらを定数値と同等にするアサーションを使用して、たとえば、LS = 7]、およびqは整数からビットベクトルへxの関数、 は整数から実数へnextの関数、 は整数から整数への関数、およびlastは整数であり、プライミングされたバージョンについても同様です; また、その一部は非線形であることに注意してください (例: delta * t_1and 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
基本的に、ここで使用されているソルバーに対応するタクティック ソルバーを作成したいと思います。このトグル動作は 4.1 で見られたものですが、Context を介して ELIM_QUANT を使用できないため、4.3 では見られません。もはやオプション。