Z3:如何在 Z3 python 中编码 If-the-else? [英] Z3: how to encode If-the-else in Z3 python?

问题描述

我想在 Z3 python 中对 If-the-else 进行编码，但找不到有关如何执行此操作的任何文档或示例.

我有一个如下所示的示例代码.

F = 真tmp = BitVec('tmp', 1)tmp1 = BitVec('tmp1', 8)

现在我如何将此条件编码为 F:

如果 tmp == 1，则 tmp1 == 100.否则，tmp1 == 0

非常感谢.

解决方案

你需要Z3的If函数:

<块引用>

def z3py.If ( a,乙，C，ctx = 无)

创建 Z3 if-then-else 表达式.

<预><代码>>>>x = Int('x')>>>y = Int('y')>>>最大值 = 如果(x > y, x, y)>>>最大限度如果(x > y, x, y)>>>简化(最大)如果(x <= y, y, x)

(来自此处)

I want to encode If-the-else in Z3 python, but cannot find any docs or sample on how to do that.

I have a sample code like below.

F = True
tmp = BitVec('tmp', 1)
tmp1 = BitVec('tmp1', 8)

Now how can I encode this condition into F:

if tmp == 1, then tmp1 == 100. otherwise, tmp1 == 0 

Thanks so much.

解决方案

You'll need Z3's If function:

def z3py.If   (       a,
          b,
          c,
          ctx = None 
  )   

Create a Z3 if-then-else expression.

>>> x = Int('x')
>>> y = Int('y')
>>> max = If(x > y, x, y)
>>> max
If(x > y, x, y)
>>> simplify(max)
If(x <= y, y, x)

(from here)

这篇关于Z3:如何在 Z3 python 中编码 If-the-else?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！