Z3py:将值添加到计算结果并进行另一次检查

Question

我想用Z3:解决以下示例

input = 0
if input < 5:
var v1 = 5
input += v1
input *= v1
if input > 5:
return True
else:
return False

如何将此逻辑转换为Z3？这就是我到目前为止所拥有的。

input = Int("input")
v1 = Int("v1")
solver = Solver()
solver.add(v1 == 5)
solver.add(input < 5)
solver.check()
model = solver.model()
for d in model.decls():
# prints:
#   "input = 4"
#   "v1 = 5"
print ("%s = %s" % (d.name(), model[d]))

如何将5添加到输入，并将多个输入与5相加，以便稍后检查是否大于5？

Answer 1

建模此类命令式程序的标准技术是将其转换为SSA(静态单赋值(形式，本质上是通过在每个位置复制每个赋值变量。有关详细信息，请参阅：https://en.wikipedia.org/wiki/Static_single_assignment_form

基于这个想法，我将为您的程序建模如下：

from z3 import *
v1 = Int('v1')
input0, input1, input2 = Ints('input0 input1 input2')
solver = Solver()
solver.add(input0 == 0)
solver.add(Implies(input0 < 5, v1 == 5))
solver.add(input1 == If(input0 < 5, input0 + v1, input0))
solver.add(input2 == If(input0 < 5, input1 * v1, input1))
result = Bool('result')
solver.add(result == (input2 > 5))
print(solver.check())
m = solver.model()
print ("input  = %s" % m[input2])
print ("v1     = %s" % m[v1])
print ("result = %s" % m[result])

运行时，将打印：

sat
input  = 25
v1     = 5
result = True

它显示了所涉及的变量的最终值和返回的值。