3

我正在使用 z3 的 python API 来解决查看一组约束是否可以满足。我将条件作为字符串，我想尽可能直接将它们传递给 z3，只是为了节省转码的处理时间。如果约束是像 a = b 这样的赋值，那么输入它的最佳方式是什么。我想要类似的东西

    str1 = "a = b"
    a = BitVec('a', 3)
    b = BitVec('b', 3)
    s = Solver()
    s.push()
    s.add(str1)

该程序给出的错误为“预期为真、假或 Z3 布尔表达式”
请让我知道最好的方法。

4

1 回答 1

4

您需要将 Z3 表达式传递给大多数 API 函数（如Solver.add(expr)），而不是字符串。对于您的示例（z3py 链接：http ://rise4fun.com/Z3Py/iu0 ）：

str1 = "a = b"
a = BitVec('a', 3)
b = BitVec('b', 3)
constraint1 = a == b # sets constraint1 to be the z3 expression a == b
s = Solver()
s.push()
# s.add(str1) # error: 'True, False or Z3 Boolean expression expected'
s.add(constraint1)
print constraint1

如果您想传递以中缀表示法编码的字符串（例如“a = b”），您应该能够使用 Python 的eval，尽管这可能无法完全通用，因此您可能必须编写一个解析器，并且您不能使用evalon由于消毒剂，rise4fun：

constraint2 = eval(str1)

以下是有关使用的更多详细信息eval：z3python：将字符串转换为表达式

如果您有以 SMT-LIB 标准编码的字符串（使用前缀表示法，例如“(= ab)”），则可以使用parse_smt2_stringAPI 函数。下面是一个从上面继续的例子：

cstr1 = "(assert (= a b))"
ds = { 'a' : a, 'b' : b }
constraint3 = parse_smt2_string(cstr1, decls=ds)
print constraint3
prove(constraint1 == constraint3)

这是 API 文档parse_smt2_string：http ://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html#-parse_smt2_string

另请参阅有关使用中缀输出 Z3 表达式的相关问题和答案：如何将 z3 表达式转换为中缀表达式？

于 2013-05-10T04:13:06.387 回答