Z3 Solver中Tactic的使用

Z3求解器是微软开发的一款定理证明器。可以用来证明定理，也可以用于求解。其基本用法并不复杂，通过现有的教程，结合源码中提供的示例就可以理解。除了基础的用法以外，Z3还提供了一系列Tactic辅助计算和证明。

本文将介绍Tactic的一些用法，以及部分Tactic的效果。本文总体基于Z3的Python API来写。本文的基本材料来自Z3的API Documentation以及代码中提供的C++示例，以及根据以上资料进行的实验。本文使用的Z3版本是4.8.0。

Tactic 简介

什么是 Tactic

Tactic在Z3中可以对一组约束（Goal）进行形式转换、求解或简化，便于对约束进行进一步的处理。

Tactic 的基本使用方法

>>> t = Tactic("simplify")
>>> x = Int('x')
>>> c = x > 0
>>> t(c)
[[Not(x <= 0)]]

可用的 Tactic 列表

本列表通过describe_tactics()获得所有可用的Tactic类型及其描述。

ackermannize_bv : A tactic for performing full Ackermannization on bv instances.
subpaving : tactic for testing subpaving module.
horn : apply tactic for horn clauses.
horn-simplify : simplify horn clauses.
nlsat : (try to) solve goal using a nonlinear arithmetic solver.
qfnra-nlsat : builtin strategy for solving QF_NRA problems using only nlsat.
nlqsat : apply a NL-QSAT solver.
qe-light : apply light-weight quantifier elimination.
qe-sat : check satisfiability of quantified formulas using quantifier elimination.
qe : apply quantifier elimination.
qsat : apply a QSAT solver.
qe2 : apply a QSAT based quantifier elimination.
qe_rec : apply a QSAT based quantifier elimination recursively.
sat : (try to) solve goal using a SAT solver.
sat-preprocess : Apply SAT solver preprocessing procedures (bounded resolution, Boolean constant propagation, 2-SAT, subsumption, subsumption resolution).
ctx-solver-simplify : apply solver-based contextual simplification rules.
smt : apply a SAT based SMT solver.
psmt : builtin strategy for SMT tactic in parallel.
unit-subsume-simplify : unit subsumption simplification.
aig : simplify Boolean structure using AIGs.
add-bounds : add bounds to unbounded variables (under approximation).
card2bv : convert pseudo-boolean constraints to bit-vectors.
degree-shift : try to reduce degree of polynomials (remark: :mul2power simplification is automatically applied).
diff-neq : specialized solver for integer arithmetic problems that contain only atoms of the form (<= k x) (<= x k) and (not (= (- x y) k)), where x and y are constants and k is a numeral, and all constants are bounded.
eq2bv : convert integer variables used as finite domain elements to bit-vectors.
factor : polynomial factorization.
fix-dl-var : if goal is in the difference logic fragment, then fix the variable with the most number of occurrences at 0.
fm : eliminate variables using fourier-motzkin elimination.
lia2card : introduce cardinality constraints from 0-1 integer.
lia2pb : convert bounded integer variables into a sequence of 0-1 variables.
nla2bv : convert a nonlinear arithmetic problem into a bit-vector problem, in most cases the resultant goal is an under approximation and is useul for finding models.
normalize-bounds : replace a variable x with lower bound k <= x with x’ = x - k.
pb2bv : convert pseudo-boolean constraints to bit-vectors.
propagate-ineqs : propagate ineqs/bounds, remove subsumed inequalities.
purify-arith : eliminate unnecessary operators: -, /, div, mod, rem, is-int, to-int, ^, root-objects.
recover-01 : recover 0-1 variables hidden as Boolean variables.
bit-blast : reduce bit-vector expressions into SAT.
bv1-blast : reduce bit-vector expressions into bit-vectors of size 1 (notes: only equality, extract and concat are supported).
bv_bound_chk : attempts to detect inconsistencies of bounds on bv expressions.
propagate-bv-bounds : propagate bit-vector bounds by simplifying implied or contradictory bounds.
propagate-bv-bounds-new : propagate bit-vector bounds by simplifying implied or contradictory bounds.
reduce-bv-size : try to reduce bit-vector sizes using inequalities.
bvarray2uf : Rewrite bit-vector arrays into bit-vector (uninterpreted) functions.
dt2bv : eliminate finite domain data-types. Replace by bit-vectors.
elim-small-bv : eliminate small, quantified bit-vectors by expansion.
max-bv-sharing : use heuristics to maximize the sharing of bit-vector expressions such as adders and multipliers.
blast-term-ite : blast term if-then-else by hoisting them.
cofactor-term-ite : eliminate term if-the-else using cofactors.
collect-statistics : Collects various statistics.
ctx-simplify : apply contextual simplification rules.
der : destructive equality resolution.
distribute-forall : distribute forall over conjunctions.
dom-simplify : apply dominator simplification rules.
elim-term-ite : eliminate term if-then-else by adding fresh auxiliary declarations.
elim-uncnstr : eliminate application containing unconstrained variables.
injectivity : Identifies and applies injectivity axioms.
snf : put goal in skolem normal form.
nnf : put goal in negation normal form.
occf : put goal in one constraint per clause normal form (notes: fails if proof generation is enabled; only clauses are considered).
pb-preprocess : pre-process pseudo-Boolean constraints a la Davis Putnam.
propagate-values : propagate constants.
reduce-args : reduce the number of arguments of function applications, when for all occurrences of a function f the i-th is a value.
reduce-invertible : reduce invertible variable occurrences.
simplify : apply simplification rules.
elim-and : convert (and a b) into (not (or (not a) (not b))).
solve-eqs : eliminate variables by solving equations.
split-clause : split a clause in many subgoals.
symmetry-reduce : apply symmetry reduction.
tseitin-cnf : convert goal into CNF using tseitin-like encoding (note: quantifiers are ignored).
tseitin-cnf-core : convert goal into CNF using tseitin-like encoding (note: quantifiers are ignored). This tactic does not apply required simplifications to the input goal like the tseitin-cnf tactic.
fpa2bv : convert floating point numbers to bit-vectors.
qffp : (try to) solve goal using the tactic for QF_FP.
qffpbv : (try to) solve goal using the tactic for QF_FPBV (floats+bit-vectors).
qffplra : (try to) solve goal using the tactic for QF_FPLRA.
default : default strategy used when no logic is specified.
qffd : builtin strategy for solving QF_FD problems.
pqffd : builtin strategy for solving QF_FD problems in parallel.
sine-filter : eliminate premises using Sine Qua Non
qfbv-sls : (try to) solve using stochastic local search for QF_BV.
nra : builtin strategy for solving NRA problems.
qfaufbv : builtin strategy for solving QF_AUFBV problems.
qfauflia : builtin strategy for solving QF_AUFLIA problems.
qfbv : builtin strategy for solving QF_BV problems.
qfidl : builtin strategy for solving QF_IDL problems.
qflia : builtin strategy for solving QF_LIA problems.
qflra : builtin strategy for solving QF_LRA problems.
qfnia : builtin strategy for solving QF_NIA problems.
qfnra : builtin strategy for solving QF_NRA problems.
qfuf : builtin strategy for solving QF_UF problems.
qfufbv : builtin strategy for solving QF_UFBV problems.
qfufbv_ackr : A tactic for solving QF_UFBV based on Ackermannization.
ufnia : builtin strategy for solving UFNIA problems.
uflra : builtin strategy for solving UFLRA problems.
auflia : builtin strategy for solving AUFLIA problems.
auflira : builtin strategy for solving AUFLIRA problems.
aufnira : builtin strategy for solving AUFNIRA problems.
lra : builtin strategy for solving LRA problems.
lia : builtin strategy for solving LIA problems.
lira : builtin strategy for solving LIRA problems.
skip : do nothing tactic.
fail : always fail tactic.
fail-if-undecided : fail if goal is undecided.
macro-finder : Identifies and applies macros.
quasi-macros : Identifies and applies quasi-macros.
ufbv-rewriter : Applies UFBV-specific rewriting rules, mainly demodulation.
bv : builtin strategy for solving BV problems (with quantifiers).
ufbv : builtin strategy for solving UFBV problems (with quantifiers).

Tactic 使用中相关的类

Goal

Goal表示希望最终的解满足的条件。可以通过add，append或insert向其中不断插入表达式，增加约束。也可以通过数组下标获得其中的subgoal。

例子：

>>> t = Then(Tactic("simplify"), Tactic("normalize-bounds"), Tactic("solve-eqs"))
>>> g = Goal()
>>> g.add(x > 10)
>>> g.add(y == x + 3)
>>> g.add(z > y)
>>> r = t(g)
>>> r
[[Not(k!714 <= -1), Not(z <= 14 + k!714)]]
>>> subgoal = r[0]
>>> subgoal
[Not(k!714 <= -1), Not(z <= 14 + k!714)]
>>> subgoal[0]
Not(k!714 <= -1)

k!714等表示的是变量，这是因为normalize-bounds这一Tactic会进行变量形式的转化。

Probe

Probe用于从Goal中获取信息，后续可以根据信息决定接下来的处理方式。具体的使用例子参见”Tactic使用中涉及的函数“部分。

可用的Probe关键字（使用describe_probes()获得）：
ackr-bound-probe : A probe to give an upper bound of Ackermann congruence lemmas that a formula might generate.
is-unbounded : true if the goal contains integer/real constants that do not have lower/upper bounds.
is-pb : true if the goal is a pseudo-boolean problem.
arith-max-deg : max polynomial total degree of an arithmetic atom.
arith-avg-deg : avg polynomial total degree of an arithmetic atom.
arith-max-bw : max coefficient bit width.
arith-avg-bw : avg coefficient bit width.
is-qflia : true if the goal is in QF_LIA.
is-qfauflia : true if the goal is in QF_AUFLIA.
is-qflra : true if the goal is in QF_LRA.
is-qflira : true if the goal is in QF_LIRA.
is-ilp : true if the goal is ILP.
is-qfnia : true if the goal is in QF_NIA (quantifier-free nonlinear integer arithmetic).
is-qfnra : true if the goal is in QF_NRA (quantifier-free nonlinear real arithmetic).
is-nia : true if the goal is in NIA (nonlinear integer arithmetic, formula may have quantifiers).
is-nra : true if the goal is in NRA (nonlinear real arithmetic, formula may have quantifiers).
is-nira : true if the goal is in NIRA (nonlinear integer and real arithmetic, formula may have quantifiers).
is-lia : true if the goal is in LIA (linear integer arithmetic, formula may have quantifiers).
is-lra : true if the goal is in LRA (linear real arithmetic, formula may have quantifiers).
is-lira : true if the goal is in LIRA (linear integer and real arithmetic, formula may have quantifiers).
is-qfufnra : true if the goal is QF_UFNRA (quantifier-free nonlinear real arithmetic with other theories).
is-qfbv-eq : true if the goal is in a fragment of QF_BV which uses only =, extract, concat.
is-qffp : true if the goal is in QF_FP (floats).
is-qffpbv : true if the goal is in QF_FPBV (floats+bit-vectors).
is-qffplra : true if the goal is in QF_FPLRA.
memory : amount of used memory in megabytes.
depth : depth of the input goal.
size : number of assertions in the given goal.
num-exprs : number of expressions/terms in the given goal.
num-consts : number of non Boolean constants in the given goal.
num-bool-consts : number of Boolean constants in the given goal.
num-arith-consts : number of arithmetic constants in the given goal.
num-bv-consts : number of bit-vector constants in the given goal.
produce-proofs : true if proof generation is enabled for the given goal.
produce-model : true if model generation is enabled for the given goal.
produce-unsat-cores : true if unsat-core generation is enabled for the given goal.
has-quantifiers : true if the goal contains quantifiers.
has-patterns : true if the goal contains quantifiers with patterns.
is-propositional : true if the goal is in propositional logic.
is-qfbv : true if the goal is in QF_BV.
is-qfaufbv : true if the goal is in QF_AUFBV.
is-quasi-pb : true if the goal is quasi-pb.

部分 Tactic 说明

simplify

simplify主要的作用是改写原有表达式，可以接受以下参数（通过help_simplify()获得）。

algebraic_number_evaluator (bool) simplify/evaluate expressions containing (algebraic) irrational numbers. (default: true)
arith_ineq_lhs (bool) rewrite inequalities so that right-hand-side is a constant. (default: false)
arith_lhs (bool) all monomials are moved to the left-hand-side, and the right-hand-side is just a constant. (default: false)
bit2bool (bool) try to convert bit-vector terms of size 1 into Boolean terms (default: true)
blast_distinct (bool) expand a distinct predicate into a quadratic number of disequalities (default: false)
blast_distinct_threshold (unsigned int) when blast_distinct is true, only distinct expressions with less than this number of arguments are blasted (default: 4294967295)
blast_eq_value (bool) blast (some) Bit-vector equalities into bits (default: false)
bv_extract_prop (bool) attempt to partially propagate extraction inwards (default: false)
bv_ineq_consistency_test_max (unsigned int) max size of conjunctions on which to perform consistency test based on inequalities on bitvectors. (default: 0)
bv_ite2id (bool) rewrite ite that can be simplified to identity (default: false)
bv_le_extra (bool) additional bu_(u/s)le simplifications (default: false)
bv_not_simpl (bool) apply simplifications for bvnot (default: false)
bv_sort_ac (bool) sort the arguments of all AC operators (default: false)
bv_trailing (bool) lean removal of trailing zeros (default: false)
bv_urem_simpl (bool) additional simplification for bvurem (default: false)
bvnot2arith (bool) replace (bvnot x) with (bvsub -1 x) (default: false)
cache_all (bool) cache all intermediate results. (default: false)
elim_and (bool) conjunctions are rewritten using negation and disjunctions (default: false)
elim_rem (bool) replace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))). (default: false)
elim_sign_ext (bool) expand sign-ext operator using concat and extract (default: true)
elim_to_real (bool) eliminate to_real from arithmetic predicates that contain only integers. (default: false)
eq2ineq (bool) expand equalities into two inequalities (default: false)
expand_power (bool) expand (^ t k) into (* t … t) if 1 < k <= max_degree. (default: false)
expand_select_store (bool) replace a (select (store …) …) term by an if-then-else term (default: false)
expand_store_eq (bool) reduce (store …) = (store …) with a common base into selects (default: false)
expand_tan (bool) replace (tan x) with (/ (sin x) (cos x)). (default: false)
flat (bool) create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor (default: true)
gcd_rounding (bool) use gcd rounding on integer arithmetic atoms. (default: false)
hi_div0 (bool) use the ‘hardware interpretation’ for division by zero (for bit-vector terms) (default: true)
hoist_cmul (bool) hoist constant multiplication over summation to minimize number of multiplications (default: false)
hoist_mul (bool) hoist multiplication over summation to minimize number of multiplications (default: false)
ignore_patterns_on_ground_qbody (bool) ignores patterns on quantifiers that don’t mention their bound variables. (default: true)
ite_extra_rules (bool) extra ite simplifications, these additional simplifications may reduce size locally but increase globally (default: false)
local_ctx (bool) perform local (i.e., cheap) context simplifications (default: false)
local_ctx_limit (unsigned int) limit for applying local context simplifier (default: 4294967295)
max_degree (unsigned int) max degree of algebraic numbers (and power operators) processed by simplifier. (default: 64)
max_memory (unsigned int) maximum amount of memory in megabytes (default: 4294967295)
max_steps (unsigned int) maximum number of steps (default: 4294967295)
mul2concat (bool) replace multiplication by a power of two into a concatenation (default: false)
mul_to_power (bool) collpase (* t … t) into (^ t k), it is ignored if expand_power is true. (default: false)
pull_cheap_ite (bool) pull if-then-else terms when cheap. (default: false)
push_ite_arith (bool) push if-then-else over arithmetic terms. (default: false)
push_ite_bv (bool) push if-then-else over bit-vector terms. (default: false)
push_to_real (bool) distribute to_real over * and +. (default: true)
rewrite_patterns (bool) rewrite patterns. (default: false)
som (bool) put polynomials in som-of-monomials form (default: false)
som_blowup (unsigned int) maximum number of monomials generated when putting a polynomial in sum-of-monomials normal form (default: 4294967295)
sort_store (bool) sort nested stores when the indices are known to be different (default: false)
sort_sums (bool) sort the arguments of + application. (default: false)
split_concat_eq (bool) split equalities of the form (= (concat t1 t2) t3) (default: false)
udiv2mul (bool) convert constant udiv to mul (default: false)

例子：
原有条件：x > 0, y > 0, x = y + 2
SMT-LIB：
(> x 0.0)
(> y 0.0)
(= x (+ y 2.0))
默认处理后：
(not (<= x 0.0))
(not (<= y 0.0))
(= x (+ 2.0 y))

solves-eq

solves-eq的主要作用是利用高斯消元法消元。

例子：
原有条件：x > 0, y > 0, x = y + 2
SMT-LIB:
(> x 0.0)
(> y 0.0)
(= x (+ y 2.0))
处理后：
(not (<= y (- 2.0)))
(not (<= y 0.0))

split-clause

split-clause的作用是将一连串“或”表达式分解成逐个单表达式。

例子：
原有条件：x < 0 || x > 0, x = y + 1, y < 0
SMT-LIB:
(or (< x 0.0) (> x 0.0))
(= x (+ y 1.0))
(< y 0.0)
处理后：
subgoal 0
(goal
(< x 0.0)
(= x (+ y 1.0))
(< y 0.0))
subgoal 1
(goal
(> x 0.0)
(= x (+ y 1.0))
(< y 0.0))

skip

skip的作用是无事发生，类比python中的pass。

fail

fail的作用是让处理失败，抛出Z3Exception。

bit-blast

bit-blast的作用是将BitVector表达式转化为SAT（Boolean satisfiability problem，布尔可满足性问题）。在调用本tactic前，需要先调用simplify。
例子：
原有条件：32x + y = 13，y > -100，(x & y) < 10，x, y均为16位BitVector
simplify(mul2concat=True)和solve-eqs处理后:
[[Concat(Extract(10, 0, x), 0) == 13 + 65535*y,
Not(y <= 65436),
Not(10 <= ~(~x | ~y))]]
bit-blast处理后：
[[k!144,
Not(Not(Or(Not(k!159),
Not(Or(Not(k!158),
Not(Or(k!158,
Not(Or(Not(k!157),
Not(Or(k!157,
Not(Or(Not(k!156),
Not(Or(k!156,
Not(Or(Not(k!155),
Not(Or(…, …)),
Or(Not(…),
Not(…),
……（略）

aig

aig的作用是利用AIG（And-Inverter Graph）简化布尔表达式。

例子：
原有条件为bit-blast处理后的条件。
aig处理后：
[[k!176,
Or(Not(k!191),
Not(Or(Not(k!190),
Or(Not(k!189),
Or(Not(k!188),
Or(Not(k!187),
Or(Not(k!186),
Or(Not(k!185),
Or(Not(k!184),
Or(Not(k!183),
Not(Or(k!182,
Or(k!181,
Not(Or(Not(k!180),
Or(Not(k!179),
Or(Not(k!178),
Not(Or(…, …))))))))))))))))))),
……（略）

sat

sat的作用是解答一个SAT问题。

例子：

>>> t = Then(With(Tactic("simplify"), mul2concat=True), Tactic("solve-eqs"), Tactic("bit-blast"), Tactic("aig"), Tactic("sat"))
>>> s = t.solver()
>>> x = BitVec('x', 16)
>>> y = BitVec('y', 16)
>>> s.add(x * 32 + y == 13)
>>> s.add(y > -100)
>>> s.add((x & y) < 10)
>>> s.check()
sat
>>> s.model()
[y = 8205, x = 1792]

smt

smt的作用是提供一个基于SAT的solver。

例子：

>>> t1 = Tactic("smt")
>>> x, y = Ints('x y')
>>> s = t1.solver()
>>> s.add(x > y + 1)
>>> s.check()
sat
>>> s.model()
[y = -2, x = 0]

normalize-bounds

normalize-bounds的作用是将有下界k的变量x改写为x – k的形式。

例子：
原有条件：x > 0, y > 0, z > 0, 3y + 2x = z, x, y, z均为int
normalize-bounds处理后：3y’ + 2x’ - z’ = -4
由于x, y, z均为int，所以实际上下界均为1,因此被改写为x’ = x – 1， y’ = y – 1, z’ = z - 1，得到以上结果。

lia2pb

lia2pb的作用是将有界的变量拆成一系列值介于0和1之间的变量。

例子：
原有条件：! (x <= -1), ! (x >= 9)
lia2pb处理后：! (x’ + 2x’’ + 4x’’’ + 8x’’’’ <= -1), ! (x’ + 2x’’ + 4x’’’ + 8x’’’’ >= 9)
其中，x’, x’’, x’’’, x’’’’均要求x >= 0 且 x <= 1。

pb2bv

pb2bv的作用是将伪布尔约束改造为BitVector。

例子：
原有条件：0 < x < 10, 0 < y < 10, 0 < z < 10, 3y + 2x = z
先经过simplify (arith_lhs=True, som=True)和normalize-bounds处理，再经过lia2pb处理，得到：
! (x’ + 2x’’ + 4x’’’ + 8x’’’’ <= -1)
! (x’ + 2x’’ + 4x’’’ + 8x’’’’ >= 9)
! (y’ + 2y’’ + 4y’’’ + 8y’’’’ <= -1)
! (y’ + 2y’’ + 4y’’’ + 8y’’’’ >= 9)
! (z’ + 2z’’ + 4z’’’ + 8z’’’’ <= -1)
! (z’ + 2z’’ + 4z’’’ + 8z’’’’ >= 9)
3y’ + 6y’’ + 12y’’’ + 24y’’’’ + 2x’ + 4x’’ + 8x’’’ + 16x’’’’ - z’ - 2z’’ - 4z’’’ - 8z’’’’ = -4
0 <= x’, x’’, x’’’, x’’’’, y’, y’’, y’’’, y’’’’, z’, z’’, z’’’, z’’’’ <= 1

经过pb2bv处理：
True, !a’ || !a’’, True, !b’ || !b’’, True, !c’ || !c’’
11 <= (unsigned) If (b’, 11, 0) + If (a’, 11, 0) + If (b’’, 11. 0) + If (a’’, 8, 0) + If(!c’, 8, 0) +If (b’’’, 6, 0) + If(a’’’, 4, 0) + If(!c’’, 4, 0) + If(b’’’’, 3 , 0) + If(a’’’’, 2, 0) + If (!c’’’, 2, 0) + If (!c’’’’, 1, 0)
True * 24 (对应原有的12个变量，各自有两个约束，>=0，<=1)
!a’ || !a’’’, !a’ || !a’’’’, !b’ || !b’’’, !b’ || !b’’’’, !c’ || !c’’’, !c’ || !c’’’’
79 <= (unsigned) If (b’, 24, 0) + If (a’, 16, 0) + If (b’’, 12. 0) + If (a’’, 8, 0) + If(!c’, 8, 0) +If (b’’’, 6, 0) + If(a’’’, 4, 0) + If(!c’’, 4, 0) + If(b’’’’, 3 , 0) + If(a’’’’, 2, 0) + If (!c’’’, 2, 0) + If (!c’’’’, 1, 0)

factor

factor的作用是对多项式进行因式分解。

例子：
原有条件：x2 - 2x – 8 = 0
factor处理后：Or (x – 4 = 0, x + 2 = 0)

Tactic 使用中涉及的函数

Repeat

Repeat的作用是重复使用参数中的tactic，直到tactic不再修改任何内容，或者到达设置的最大次数为止。

API：

Repeat(t, max = 4294967295, ctx = None) # 其中t是输入的tactic，max是最大次数。

例子：
原有条件：x = 0 || x = 1, y = 0 || y = 1, x > y
经过split-clause处理一次：
x = 0, y = 0 || y = 1, x > y
x = 1, y = 0 || y = 1, x > y
使用Repeat(OrElse(Tactic(‘split-clause’), Tactic(‘skip’)))处理后：
x = 0, y = 0, x > y
x = 0, y = 1, x > y
x = 1, y = 0, x > y
x = 1, y = 1, x > y
Repeat的max参数=实际执行次数–1。同上一例子，若max设为0（Repeat(OrElse(Tactic(‘split-clause’), Tactic(‘skip’)), 0)）,则结果与只处理一次相同。若max设为1,则结果与不设相同。

OrElse

OrElse的作用是，先执行第一个参数，若执行失败则执行第二个。在C++中用“|”表示。

API：

OrElse(ts, ks)

例子参见Repeat的例子。

TryFor

TryFor的作用是返回一个tactic，此tactic要求在设定的时间（单位ms）中完成处理，否则处理失败。

API：

TryFor (t, ms, ctx = None) # t为传入的tactic，ms为时间。

With

With的作用是返回一个tactic，此tactic要求使用With中传入的参数作为参数。

API：

With(t, args, keys) # t是传入的tactic，args和keys似乎是指向不同格式的参数形式。args是数组格式，keys是字典格式。

例子：

t = With(Tactic(‘simplify’), som=True)

原有条件：(x + 1) * (y + 2) = 0
经t处理后：2x + y + xy = -2
可见t和simplify(, som=True) 等价

Tactic.solver

Tactic.solver的作用是利用本tactic生成一个solver。

API：

Tactic.solver(self)

例子：
参见Tactic中sat的例子。

FailIf

FailIf的作用是根据输入的Probe获得的信息，若结果为真，则fail。

API：

FailIf (p, ctx=None) # p是传入的Probe。

例子：

>>> g = Goal()
>>> x, y, z = Ints('x y z')
>>> g.add(x + y + z > 0)
>>> p = Probe("num-consts")
>>> p(g)
3.0
>>> t = FailIf(p > 2)
>>> t(g)
Z3Exception: fail-if tactic
>>> g = Goal()
>>> g.add(x + y > 0)
>>> t(g)
[[x + y > 0]]

When

When的作用是根据输入的Probe获得的信息，若结果为真，则执行后续的tactic。

API：

When(p, t, ctx=None) # p是Probe，t是tactic。

例子：

>>> t = When(Probe('size') > 2, Tactic('simplify'))
>>> x, y = Ints('x y')
>>> g = Goal()
>>> g.add(x > 0)
>>> g.add(y > 0)
>>> t(g)
[[x > 0, y > 0]]
>>> g.add(x == y + 1)
>>> t(g)
[[Not(x <= 0), Not(y <= 0), x == 1 + y]]

Cond

Cond的作用是根据输入的Probe获得的信息，若结果为真，则执行第一个tactic，否则执行第二个。

API：

Cond(p, t1, t2, ctx=None) # p是Probe，t1和t2分别为两个tactic。