Z3py:将值添加到计算结果并进行另一次检查 [英] Z3py: Add value to computed result and make another check

问题描述

我想用 Z3 解决下面的例子:

输入 = 0如果输入<5:无功 v1 = 5输入 += v1输入 *= v1如果输入>5:返回真别的:返回错误

如何将这个逻辑转换为 Z3?这是我目前所拥有的.

input = Int(输入")v1 = Int(v1")求解器 = 求解器()solver.add(v1 == 5)solver.add(输入<5)求解器检查()模型 =solver.model()对于 model.decls() 中的 d:# 印刷:# "输入 = 4";# "v1 = 5";打印 ("%s = %s" % (d.name(), model[d]))

如何将 5 添加到输入中，并将多个输入添加到 5，以便稍后检查它是否大于 5?

解决方案

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

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

from z3 import *v1 = Int('v1')input0, input1, input2 = Ints('input0 input1 input2')求解器 = 求解器()solver.add(input0 == 0)solver.add(暗示(input0 <5, v1 == 5))solver.add(input1 == If(input0 <5, input0 + v1, input0))solver.add(input2 == If(input0 <5, input1 * v1, input1))结果 = Bool('结果')solver.add(result == (input2 > 5))打印(求解器.检查())m =solver.model()打印(输入 = %s"% m[input2])打印(v1 = %s"% m[v1])打印(结果 = %s"% m[结果])

运行时，打印:

sat输入 = 25v1 = 5结果 = 真

显示所涉及变量的最终值和返回值.

I want to solve the following example with Z3:

input = 0
if input < 5:
    var v1 = 5
    input += v1
    input *= v1

if input > 5:
    return True
else:
    return False

How do I turn this logic into Z3? This is what I have so far.

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]))

How do I add 5 to input and multiple input with 5 that I can later check if it's greater than 5?

解决方案

The standard technique for modeling such imperative programs is to convert it to SSA (static single assignment) form, essentially by duplicating each assigned variable at each position. For details, see: https://en.wikipedia.org/wiki/Static_single_assignment_form

Based on this idea, I'd model your program as follows:

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])

When run, this prints:

sat
input  = 25
v1     = 5
result = True

which shows the final values of the variables involved and the returned value.

这篇关于Z3py:将值添加到计算结果并进行另一次检查的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！