Сохраните и перезагрузите ограничения решателя z3py - PullRequest
Новая
       17

Сохраните и перезагрузите ограничения решателя z3py

2 голосов
/ 11 марта 2019

Можно ли сохранить созданные мною ограничения для решателя z3, а затем перезагрузить их, чтобы продолжить поиск других решений?

Я узнал, что для таких вещей существует формат SMT-LIB2, а z3 и z3py имеютAPI для сохранения и загрузки в этом формате.К сожалению, я не могу заставить это работать.

Вот мой пример программы, которая бессмысленно сохраняет и перезагружает: 

import z3

filename = 'z3test.smt'

# Make a solver with some arbitrary useless constraint
solver = z3.Solver()
solver.add(True)

# Save to file
smt2 = solver.sexpr()
with open(filename, mode='w', encoding='ascii') as f: # overwrite
    f.write(smt2)
    f.close()

# Load from file
solver.reset()
solver.from_file(filename)

Сбой: 

Exception has occurred: ctypes.ArgumentError
argument 3: <class 'TypeError'>: wrong type
  File "C:\Users\Marian Aldenhövel\Desktop\FridgeIQ\z3\z3-4.8.4.d6df51951f4c-x64-win\bin\python\z3\z3core.py", line 3449, in Z3_solver_from_file
    _elems.f(a0, a1, _to_ascii(a2))
  File "C:\Users\Marian Aldenhövel\Desktop\FridgeIQ\z3\z3-4.8.4.d6df51951f4c-x64-win\bin\python\z3\z3.py", line 6670, in from_file
    _handle_parse_error(e, self.ctx)
  File "C:\Users\Marian Aldenhövel\Desktop\FridgeIQ\src\z3test.py", line 17, in <module>
    solver.from_file(filename)

Это проблема с моим пониманием или моим кодом?Можно ли это сделать так?Являются ли sexpr() и from_file() правильной парой вызовов API?

Я использую z3 и z3py 4.8.4 из https://github.com/z3prover/z3/releases в Windows 10 64bit.

Более подробная информация, если требуется:

Я играю с z3 в Python, чтобы найти решения для большой головоломки.

Чтобы найти все решения, которые я звоню solver.check().Когда он возвращает вердикт sat, я интерпретирую модель как образ моего решения головоломки.Затем я добавляю блокирующее предложение, исключающее это конкретное решение, и снова вызываю solver.check().

Это работает нормально, и я в восторге.

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

Я могу легко воссоздать начальные ограничения, которые и составляют весь смысл программы.Но предложения о блокировке являются продуктом времени выполнения и функцией того, как далеко мы продвинулись.

Я думал, что смогу сохранить состояние решателя, и если во время выполнения я найду такой файл, перезапустите его, загрузив его с блокировкойпункты без изменений и продолжают находить больше решений вместо того, чтобы начинать заново.

Спасибо, что уделили время на чтение и размышления.

Мариан

1 Ответ

1 голос
/ 11 марта 2019

С z3 4.4.1 и z3 4.8.5 я бы сбросил (и перезагрузил) ограничения в формате smt2 следующим образом: 

import z3

filename = "z3test.smt2"

x1 = z3.Real("x1")
x2 = z3.Real("x2")

solver = z3.Solver()
solver.add(x1 != x2)

#
# STORE
#

with open(filename, mode='w') as f:
    f.write(solver.to_smt2())

#
# RELOAD
#

solver.reset()

constraints = z3.parse_smt2_file(filename, sorts={}, decls={})
solver.add(constraints)
print(solver)

вывод: 

~$ python t.py 
[And(x1 != x2, True)]

файлz3test.smt2: 

(set-info :status unknown)
(declare-fun x2 () Real)
(declare-fun x1 () Real)
(assert
 (and (distinct x1 x2) true))
(check-sat)

Понятия не имею, изменился ли API в используемой вами версии.Обратная связь приветствуется.

...