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

里面显示了涉及到的变量的最终值和返回值。

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

Z3py: Add value to computed result and make another check

z3

z3py