python - z3 smt 求解器采用什么形式的输入？如何使用文件读取需要求解的方程？

Question

from z3 import *
x = Int('x')
y = Int('y')
s = Solver()
try:
    f = open("read.txt","r")
    try:
        str = f.read()
        length = len(str)
        s.add(str)
    finally:
        f.close()
except IOError:
    pass

我写了上面的代码，但它不起作用。它不接受字符串作为输入，我无法找到它接受哪种输入。

Answer 1

我们基本上可以按照 martineau 的建议进行操作。请记住，这是一个很大的黑客行为并且不安全，因为文件 read.txt 可能包含任意 Python 命令。无论如何，下面的代码将评估输入文件的每一行，并将结果对象添加到求解器 s 中。如果文件 read.txt 包含 x + y == 2，则输出将为:

sat
[y = 0, x = 2]

这是更新后的代码:

from z3 import *
x = Int('x')
y = Int('y')
s = Solver()
try:
    f = open("read.txt","r")
    try:
        for l in f:
            s.add(eval(l))
    finally:
        f.close()
except IOError:
    pass
print s.check()
print s.model()

另一个解决方案是创建 SMT-LIB 2.0 格式的文件，并使用以下帖子中描述的方法:

• Z3 4.0 Z3_parse_smtlib2_string

• Z3 with string expressions