问题描述:

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

I wrote the above code but it is not working. It is not taking a string as an input, and I am unable to find what kind of input it accepts. Please help.

网友答案:

We can essentially do what was suggested by martineau. Keep in mind this is a big hack and insecure because the file read.txt may contain arbitrary Python commands. Anyway, the following piece of code, will evaluate each line of the input file, and add the resultant object into the solver s. If the file read.txt contains x + y == 2, then the output will be:

sat
[y = 0, x = 2]

Here is the updated code:

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()

Another solution is to create files in SMT-LIB 2.0 format, and use the approach described in the following posts:

  • Z3 4.0 Z3_parse_smtlib2_string

  • Z3 with string expressions

相关阅读:
Top