z3 - z3での戦術オプションの設定

Question

z3を使用してSMT2ファイルを解決し、戦術を適用する場合（たとえば、「（apply qfbv）」）、その戦術のオプションを設定するにはどうすればよいですか？たとえば、QFBVには、デフォルトでfalseに設定されているオプション「cache-all」があります。SMT2ファイルを使用してtrueに設定するにはどうすればよいですか？または、SMT2言語を使用してこれを行うことはできませんか？

Answer 1

コンビネータを使用できますusing-params。コンビネータ!はの省略形ですusing-params。これは、戦術を使用した小さな例です（ http://rise4fun.com/Z3/JaZsimplifyでオンラインで試してください）。

(declare-const x Int)
(declare-const y Int)

(assert (= (+ x 1) (+ y 3)))


(apply simplify)
(echo ">>>> Using arith-lhs := True, and eq2ineq := True")
(apply (using-params simplify :arith-lhs true :eq2ineq true))
;; ! is a shorthand for using-params
(apply (! simplify :arith-lhs true :eq2ineq true))

Answer 2

using-paramsコンビネータを使用できます。オンライン(help-tactic)でZ3SMTと入力すると、 次のフラグメントが表示されます。

- (using-params <tactic> <attribute>*)指定された属性を使用して指定された戦術を実行します。ここで<attribute> ::= <keyword> <value>.！-paramsを使用するためのシンタックスシュガーです。

タイプチェックされた例を次に示します（意味があるかどうかはわかりません）。

(declare-const x (_ BitVec 16))
(declare-const y (_ BitVec 16))

(assert (= (bvor x y) (_ bv13 16)))
(assert (bvslt x y))

(apply (using-params qfbv :cache-all true))