What form of input does z3 smt solver take? How to use a file to read the equation required to be solved?

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

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.

Answer 1

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