Setting tactic option in z3

Question

When using z3 to solve SMT2 files and applying a tactic, (e.g., "(apply qfbv)"), how do I set an option for that tactic? For example, QFBV has an option "cache-all" that by default is set to false. How can I set it to true using SMT2 files? Or is this not possible using the SMT2 language?

Answer 1

You can use the combinator using-params. The combinator ! is a shorthand for using-params. Here is a small example using the tactic simplify (Try it online at: http://rise4fun.com/Z3/JaZ).

(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

You can use using-params combinator. Typing (help-tactic) in Z3 SMT online gives me this fragment:

- (using-params <tactic> <attribute>*) executes the given tactic using the given attributes, where <attribute> ::= <keyword> <value>. ! is a syntax sugar for using-params.

Here is a type-checked example (not sure that it makes sense):

(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))