z3 - 在 z3 中设置策略选项

Question

当使用 z3 解决 SMT2 文件并应用策略（例如，“(apply qfbv)”）时，如何为该策略设置选项？例如，QFBV 有一个选项“cache-all”，默认设置为 false。如何使用 SMT2 文件将其设置为 true？或者这不可能使用 SMT2 语言？

Answer 1

您可以使用组合器using-params。组合!器是 的简写using-params。这是一个使用该策略的小示例simplify（在线试用：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

您可以使用using-params组合器。(help-tactic)在线输入Z3 SMT 给我这个片段：

- (using-params <tactic> <attribute>*)使用给定的属性执行给定的策略，其中<attribute> ::= <keyword> <value>.！是 using-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))