在z3中迭代添加

Question

我想检查a，b，c的值，如果值'a'等于1，则'x'加1。我们继续执行值“ b”和“ c”的过程。因此，如果a = 1，b = 1，c = 1，则x的结果应为3。如果a = 1，b = 1，c = 0，则x的结果应为2。在z3中要实现什么方法？源代码如下：

from z3 import *

a, b, c = Ints('a b c')
x, y = Ints('x y')
s = Solver()
s.add(If(a==1, x=x + 1, y = y-1))
s.add(If(b==1, x=x + 1, y = y-1))
s.add(If(c==1, x=x + 1, y = y-1))
s.check()
print s.model()

关于我能做什么的任何建议？

Answer 1

这种“迭代”处理通常通过展开分配并创建所谓的SSA表单来建模。 （静态单次分配。）在这种格式下，每个变量只分配一次，但是可以多次使用。通常这是由一些基础工具完成的，因为它相当繁琐，但是您也可以手动完成。应用于您的问题，它看起来像：

from z3 import *

s = Solver()

a, b, c = Ints('a b c')

x0, x1, x2, x3 = Ints('x0 x1 x2 x3')

s.add(x0 == 0)
s.add(x1 == If(a == 1, x0+1, x0))
s.add(x2 == If(b == 1, x1+1, x1))
s.add(x3 == If(c == 1, x2+1, x2))

# Following asserts are not part of your problem, but
# they make the output interesting
s.add(b == 1)
s.add(c == 0)

# Find the model
if s.check() == sat:
   m = s.model()
   print("a=%d, b=%d, c=%d, x=%d" % (m[a].as_long(), m[b].as_long(), m[c].as_long(), m[x3].as_long()))

else:
    print "no solution"

SSA转换应用于变量x，创建了为分配建模所需的尽可能多的实例。运行时，此程序将产生：

a=0, b=1, c=0, x=1

希望有帮助！