高性能的求解程序，如Z3，集成了许多手工的启发式算法证明方法组合。虽然这些启发式组合倾向于对已知类型的问题进行高度调整，但它们很容易在新类型的问题上表现得非常糟糕。随着solver开始获得不同领域的科学家和工程师的关注，这个问题变得越来越紧迫，在许多情况下，对求解器启发式的更改可以产生巨大的差异。

Z3实现了一种精心策划的推理引擎方法，其中“大”的符号推理步骤被表示为函数(或策略，tactics)，tactics 由tacticals的组合组成。Tactics把公式集称为Goals.

当一个tactic应用于某个goal G时，可能会出现四种不同的结果。该tactic

表明G是可满足的(即可行的)
表明G是不可满足的(即不可行的)
产生一系列的子目标
失败。

当将一个goal G规约为一系列子目标G1, ... , Gn时,我们面临着模型转换的问题。模型转换器利用子目标Gi的模型构建G的模型。

simplify 和 solve-eqs

在下面的例子中，我们创建了一个由三个公式组成的Goal g，以及一个由两个内置tactic:simplify和solve-eqs 组成的Tactic t 。simplify策略对公式进行了等价简化。solver-eqs策略采用高斯消元法来消去变量。实际上，solve-eqs并不仅仅局限于线性方程，它还可以消除任意变量。然后，Then把simplify策略应用到输入目标上，把solve-eqs应用到simplify产生的每个子目标上。在这个例子中只产生了一个子目标。

!pip install "z3-solver"from z3 import *x, y = Reals('x y')
g  = Goal()
g.add(x > 0, y > 0, x == y + 2)
print(g)t1 = Tactic('simplify')
t2 = Tactic('solve-eqs')
t  = Then(t1, t2)
print(t(g))
'''
[x > 0, y > 0, x == y + 2]
[[Not(y <= -2), Not(y <= 0)]]
'''

在上面的例子中，变量x被忽略了，没有出现在结果中

split-clause

在z3中，我们说一个子句是 Or(f_1 , ... , f_n)形式的约束，策略split-clause将从输入目标中选择一个子句Or(f_1,...,f_n)，把它切分成n个子目标

x, y = Reals('x y')
g  = Goal()
g.add(Or(x < 0, x > 0), x == y + 1, y < 0)t = Tactic('split-clause')
r = t(g)
for g in r: print(g)
'''
[x < 0, x == y + 1, y < 0]
[x > 0, x == y + 1, y < 0]
'''

describe_tactics()

Z3配备了许多内置tactics。命令describe_tactics()提供了所有内置tactics的简短描述。

descripbe_tactics()配备了以下的tactic组合，又叫tacticals

Then(t,s)将t应用到输入目标，将s应用于t产生的每个子目标
OrElse(t,s)首先将t应用于给定目标，如果失败，则返回s应用于给定目标的结果。
Repeat(t)，一直应用给定的策略，直到没有子目标被它修改。
Repeat(t,n)，一直应用给定策略，直到没有子目标被它修改，或者迭代次数大于n。
TryFor(t, ms)将策略t应用于输入目标，如果没有在ms毫秒内返回，则失败。
With(t, params)使用给定的参数应用给定的策略。

下面的例子演示了如何使用这些组合。

x, y, z = Reals('x y z')
g = Goal()
g.add(Or(x == 0, x == 1), Or(y == 0, y == 1), Or(z == 0, z == 1),x + y + z > 2)# Split all clauses"
split_all = Repeat(OrElse(Tactic('split-clause'),Tactic('skip')))
print(split_all(g))split_at_most_2 = Repeat(OrElse(Tactic('split-clause'),Tactic('skip')),1)
print(split_at_most_2(g))# Split all clauses and solve equations
split_solve = Then(Repeat(OrElse(Tactic('split-clause'),Tactic('skip'))),Tactic('solve-eqs'))print(split_solve(g))
'''
[[x == 0, y == 0, z == 0, x + y + z > 2],[x == 0, y == 0, z == 1, x + y + z > 2],[x == 0, y == 1, z == 0, x + y + z > 2],[x == 0, y == 1, z == 1, x + y + z > 2],[x == 1, y == 0, z == 0, x + y + z > 2],[x == 1, y == 0, z == 1, x + y + z > 2],[x == 1, y == 1, z == 0, x + y + z > 2],[x == 1, y == 1, z == 1, x + y + z > 2]]
[[x == 0, y == 0, Or(z == 0, z == 1), x + y + z > 2],[x == 0, y == 1, Or(z == 0, z == 1), x + y + z > 2],[x == 1, y == 0, Or(z == 0, z == 1), x + y + z > 2],[x == 1, y == 1, Or(z == 0, z == 1), x + y + z > 2]]
[[]]
'''

在策略split_solve中，策略solve-eqs会释放所有目标，只保留一个。因此这个策略会生成一个目标：可满足(可行的)的空目标（empty goal）

遍历子目标

x, y, z = Reals('x y z')
g = Goal()
g.add(Or(x == 0, x == 1), Or(y == 0, y == 1), Or(z == 0, z == 1),x + y + z > 2)# Split all clauses"
split_all = Repeat(OrElse(Tactic('split-clause'),Tactic('skip')))
for s in split_all(g):print(s)
'''
[x == 0, y == 0, z == 0, x + y + z > 2]
[x == 0, y == 0, z == 1, x + y + z > 2]
[x == 0, y == 1, z == 0, x + y + z > 2]
[x == 0, y == 1, z == 1, x + y + z > 2]
[x == 1, y == 0, z == 0, x + y + z > 2]
[x == 1, y == 0, z == 1, x + y + z > 2]
[x == 1, y == 1, z == 0, x + y + z > 2]
[x == 1, y == 1, z == 1, x + y + z > 2]
'''

solver()

可以使用solver()方法将策略转换为求解器对象。如果策略产生空目标，则相关的求解器返回sat。如果策略产生包含False的单个目标，则求解器返回unsat。否则，它返回unknown。

bv_solver = Then('simplify', 'solve-eqs', 'bit-blast', 'sat').solver()x, y = BitVecs('x y', 16)
solve_using(bv_solver, x | y == 13, x > y)
'''
[y = 0, x = 13]
'''

在上面的例子中，策略bv_solver实现了使用equation solving, bit-blasting 的一个基本的位向量求解器 , 和一个命题SAT求解器。注意，命令Tactic被禁止。如果参数是字符串，所有的Z3Py combinators都会自动调用Tactic命令。最后，命令solve_using是solve命令的一个变体，其中第一个参数指定要使用的求解器。

With和aig

在下面的例子中，我们直接使用求解器API而不是命令solve_using。我们使用With来配置我们的求解器。我们还包括试图用And-Inverted Graphs压缩布尔公式的aig策略。

bv_solver = Then(With('simplify', mul2concat=True),'solve-eqs', 'bit-blast', 'aig','sat').solver()
x, y = BitVecs('x y', 16)
bv_solver.add(x*32 + y == 13, x & y < 10, y > -100)
print(bv_solver.check())
m = bv_solver.model()
print(m)
print(x*32 + y, "==", m.evaluate(x*32 + y))
print(x & y, "==", m.evaluate(x & y))
'''
sat
[y = 10509, x = 1720]
x*32 + y == 13
x & y == 8
'''

smt

策略smt将覆盖Z3中的主要求解器作为一个策略。

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

整数运算

现在，我们展示如何使用SAT实现整数运算的求解器。求解器只有在每个变量都有下界和上界的情况下才完整。

s = Then(With('simplify', arith_lhs=True, som=True),'normalize-bounds', 'lia2pb', 'pb2bv', 'bit-blast', 'sat').solver()
x, y, z = Ints('x y z')
solve_using(s, x > 0, x < 10, y > 0, y < 10, z > 0, z < 10,3*y + 2*x == z)
# It fails on the next example (it is unbounded)
s.reset()
solve_using(s, 3*y + 2*x == z)
'''
[z = 7, y = 1, x = 2]
failed to solve
'''

`Tactics`与`solvers`结合

例如，我们可以对一个目标应用一个策略，生成一组子目标，然后选择其中一个子目标，并使用求解器解决它。下一个示例演示如何做到这一点，以及如何使用模型转换器将子目标的模型转换为原始目标的模型。

t = Then('simplify', 'normalize-bounds', 'solve-eqs')x, y, z = Ints('x y z')
g = Goal()
g.add(x > 10, y == x + 3, z > y)r = t(g)
# r contains only one subgoal
print(r)s = Solver()
s.add(r[0])
print(s.check())
# Model for the subgoal
print(s.model())
# Model for the original goal
print(r[0].convert_model(s.model()))
'''
[[Not(k!91 <= -1), Not(z <= 14 + k!91)]]
sat
[z = 15]
[z = 15, y = 14, x = 11]
'''

Probes

Probes(又称formula measures)是在目标之上进行评估的。上面的布尔表达式可以使用关系操作符和布尔连接词来构建。如果给定目标不满足条件cond，则策略FailIf(cond)失败。Z3Py中提供了许多数值和布尔度量。descripbe_probes()命令提供了所有内置probes的列表。

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.
'''

在下面的例子中，我们使用FailIf构建了一个简单的策略。它还表明probe可以直接应用到目标上。

x, y, z = Reals('x y z')
g = Goal()
g.add(x + y + z > 0)p = Probe('num-consts')
print("num-consts:", p(g))t = FailIf(p > 2)
try:t(g)
except Z3Exception:print("tactic failed")print("trying again...")
g = Goal()
g.add(x + y > 0)
print(t(g))
'''
num-consts: 3.0
tactic failed
trying again...
[[x + y > 0]]
'''

Z3Py还提供了If(p, t1, t2)的combinator(tactical)，它是:OrElse(Then(FailIf(Not(p)), t1), t2)的缩写；When(p, t) 是If(p, t, 'skip')的缩写。策略skip只返回输入目标. 下面的例子演示了如何使用If连接符。

x, y, z = Reals('x y z')
g = Goal()
g.add(x**2 - y**2 >= 0)p = Probe('num-consts')
t = If(p > 2, 'simplify', 'factor')print(t(g))g = Goal()
g.add(x + x + y + z >= 0, x**2 - y**2 >= 0)print(t(g))
'''
[[(y + -1*x)*(y + x) <= 0]]
[[2*x + y + z >= 0, x**2 + -1*y**2 >= 0]]
'''

z3 strategies相关推荐

mark点Z3学习资料整理
文章目录 Anything is Nothing Less is More SMT z3 classes logic programming Reasoning符号推理策略strategies Fix ...
Tools and Strategies for Long-Read Sequencing and De Novo Assembly of Plant Genomes
Tools and Strategies for Long-Read Sequencing and De Novo Assembly of Plant Genomes 用于植物基因组长读测序和从头组装 ...
Windows下安装Z3的Python3版
文章目录 Windows下安装Z3的Python3版 pip 安装(不推荐,很慢) 使用微软官方构建好的DLL(推荐,快速) Windows下安装Z3的Python3版 GitHub官方仓库地址:Z3 ...
SAP RETAIL WA01创建分配表报错- No allocation rule allowed for allocation strategies or variants-
SAP RETAIL WA01创建分配表报错- No allocation rule allowed for allocation strategies or variants- 1,执行事务代码WA ...
SharePoint 2007 Backup Strategies
SharePoint 2007 Backup Strategies from http://www.sharepointkicks.com/ 转载于:https://www.cnblogs.com/i ...
CTF Re-Python z3库的使用
一安装: z3是由微软公司开发的一个优秀的SMT求解器(也就定理证明器),它能够检查逻辑表达式的可满足性. 我是在windows下pyCharm 里面自己添加包包名为z3-slover(不是z3) ...
boost::geometry模块测试地理策略Testing geographic strategies的测试程序
boost::geometry模块测试地理策略Testing geographic strategies的测试程序实现功能 C++实现代码实现功能 boost::geometry模块测试地理策略T ...
C语言学习之两个乒乓球队进行比赛,各出3人。甲队为A,B,C3人,乙队为X,Y,Z3人。已抽签决定比赛名单。
两个乒乓球队进行比赛,各出3人.甲队为A,B,C3人,乙队为X,Y,Z3人.已抽签决定比赛名单.有人向队员打听比赛的名单,A说他不和X比,C说他不和X,Z比,请编程序找出3对赛手的名单. #inclu ...
python解释器下安装z3_再次：在Windows上安装Z3 Python
earlier question中指出的安装问题仍然存在. 我曾尝试在Windows XP SP3 32位和Windows 7 64位下安装Z3 4.3.0和4.1.这些组合都不起作用!我可以执行&q ...

z3 strategies

simplify 和 solve-eqs

split-clause

describe_tactics()

遍历子目标

solver()

With和aig

smt

整数运算

`Tactics`与`solvers`结合

Probes

z3 strategies相关推荐

最新文章

热门文章

z3 strategies

simplify 和 solve-eqs

split-clause

describe_tactics()

遍历子目标

solver()

With和aig

smt

整数运算

Tactics与solvers结合

Probes

z3 strategies相关推荐

最新文章

热门文章

`Tactics`与`solvers`结合