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的建议去做。请记住，这是一个很大的 hack 并且不安全，因为该文件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 带字符串表达式