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

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

  • Tactic 简介

    • 什么是 Tactic
    • Tactic 的基本使用方法
  • 可用的 Tactic 列表
  • Tactic 使用中相关的类
    • Goal
    • Probe
  • 部分 Tactic 说明
    • simplify
    • solves-eq
    • split-clause
    • skip
    • fail
    • bit-blast
    • aig
    • sat
    • smt
    • normalize-bounds
    • lia2pb
    • pb2bv
    • factor
  • Tactic 使用中涉及的函数
    • Repeat
    • OrElse
    • TryFor
    • With
    • Tactic.solver
    • FailIf
    • When
    • Cond

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。

Z3 Solver中Tactic的使用相关推荐

  1. 【z3 solver手动安装】

    TSN领域有很多文章使用z3 solver求解约束可满足性问题.典型的工作包括Silviu S. Craciunas 等人的Scheduling Real-Time Communication in ...

  2. [Mesh Order]lumerical MODE软件EME Solver中结构重叠区域(clapping)求解过程中的优先级问题

    当仿真区域中出现重叠区域时就存在求解优先级的问题,使用以下两个方面可以解决 不使用index monitor 使用index monitor 一.不使用index monitor 在编辑structu ...

  3. 实数在java中的表示,java - 如何在Z3（Java）中从模型中获取实数值作为小数（双精度）？ - SO中文参考 - www.soinside.com...

    我正在尝试从Model计算的Solver中获取Real值.但是,即使我将pp.decimal设置为true(在SMT2文件中和使用Global.setParameter),只有在打印模型本身时才会遵循 ...

  4. 10以内逆向运算题_Z3在逆向中运用

    亲爱的,关注我吧 9/17 文章共计7370个词 预计阅读10分钟 来和我一起阅读吧 介绍 Z3 在工业应用中实际上常见于软件验证.程序分析等.然而由于功能实在强大,也被用于很多其他领域.CTF 领域 ...

  5. SMT Z3 C++版本简易教程（以python版本为对照）

    近期因为科研工作需要,将原本以python实现的z3项目以c++重写,由于缺少c++版本的相关教程,花费了较多时间,故在完成当前项目后制作该简易教程(仅包含个人理解和个人在开发过程中遇到的困难之处), ...

  6. Z3约束器详细学习（0）—Z3安装|语句详解

    推荐肉丝r0ysue课程(包含安卓逆向与js逆向): 参考资料: Z3 API IN PYTHON 中文文档 1. Z3安装 linux安装Z3 git clone https://github.co ...

  7. Z3求解器简介以及特定约束条件下求出所有可行解

    Z3求解器 1.Z3求解器简介: Z3是微软研究院开发的高性能定理证明器.Z3用于许多应用,如:软件/硬件验证和测试,约束解决,混合系统的分析,安全,生物学(在硅分析),和几何问题. 2.Z3求解器u ...

  8. Caffe部署中的几个train-test-solver-prototxt-deploy等说明二

    Caffe部署中的几个train-test-solver-prototxt-deploy等说明<二> 发表于2016/9/15 20:39:52  1049人阅读 分类: 神经网络与深度学 ...

  9. Ceres Solver Document学习笔记

    Ceres Solver Document学习笔记 Ceres Solver Document学习笔记 1. 基本概念 2. 基本方法 2.1 CostFunction 2.2 AutoDiffCos ...

最新文章

  1. 简述BT下载技术及其公司发展现状
  2. 周志华教授发表首届国际学习与推理联合大会IJCLR开场Keynote：探索从纯学习到学习+推理的AI...
  3. Spring 的优秀工具类盘点
  4. 抽象类与接口 day-11.2
  5. wcf rest系列文章
  6. 我在斯坦福做科研的碎碎念
  7. 我的世界SkyPixel像素天空HTML官网源码
  8. 求素数算法（C语言）
  9. DG SG childSG fatherSG
  10. Sentinel降级_RT_分布式系统集群限流_线程数隔离_削峰填谷_流量控制_速率控制_服务熔断_服务降级---微服务升级_SpringCloud Alibaba工作笔记0039
  11. 常用Physionet命令整理
  12. 网络流(最大流) CQOI 2015 BZOJ 3931 网络吞吐量
  13. 根据身份证号匹配对应的城市编码
  14. 2021，自动驾驶的“五代十国”
  15. 工作汇报计时器小工具介绍
  16. 电脑哪个服务器可以玩无限连击,无尽之剑3手把手教你无限连击攻略
  17. Moses安装全记录
  18. c语言中格式符号错误,C语言中符号格式说明
  19. html 支持ssi,shtml网页SSI使用详解
  20. layui引入第三方依赖

热门文章

  1. git提交项目时候，忽略一些文件
  2. java五子棋ai_Java五子棋Ai-权值法
  3. java静态类读取配置文件内容
  4. matlab求莱斯分布pdf,Matlab累积分布函数cdf与概率密度函数pdf
  5. 在ESP8266上控制WS2812灯带及热释电传感器原码
  6. 数据信息汇总的7种基本技术总结
  7. 基于联咏NT96670/675/672芯片全高清记录器方案开发的产品规格参数
  8. 【GNSS】单点定位程序总结 二 时间系统模块
  9. 正六面体用若干种颜色染色的问题解法
  10. TCWeb使用的tablib标准