Какую форму ввода принимает решатель z3 smt? Как использовать файл для чтения уравнения, которое необходимо решить?

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

Я написал приведенный выше код, но он не работает. Он не принимает строку в качестве ввода, и я не могу найти, какой ввод он принимает.


python z3 z3py
person user2534232    schedule 29.06.2013    source источник
comment
Как выглядит содержимое read.txt? Вы пытались выяснить, можете ли вы загружать утверждения в формате SMTLib2?   -  person Malte Schwerhoff    schedule 29.06.2013
comment
Попробуйте сделать что-то вроде eval('s.add({})'.format(str.strip())). Кстати, str — это имя встроенной функции, и его не следует использовать в качестве имени переменной.   -  person martineau    schedule 29.06.2013
comment
read.txt содержит уравнение вида x + y == 2   -  person user2534232    schedule 29.06.2013

Ответы (1)


arrow_upward
2
arrow_downward

По сути, мы можем сделать то, что предложил 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 и использовать подход, описанный в следующих сообщениях:

person Leonardo de Moura    schedule 09.07.2013