#caching #z3 #z3py
#кэширование #z3 #z3py
Вопрос:
Я знаю, что Z3 имеет кэширование на основе стека, где дополнительные формулы могут быть добавлены и кэшированы. Существует ли встроенный способ или расширение, позволяющее объединять два кэша Z3?
Пример (Z3 py)
from z3 import Solver
solver = Solver()
solver.push()
solver2 = Solver()
# solver.combine(solver2) ?
Ответ №1:
Не совсем понятно, что вы подразумеваете под «объединением». Но вы можете получить утверждения из одного и добавить их к другому:
from z3 import *
i = Int('x')
s1 = Solver()
s1.add(i == 3)
s1.push()
s2 = Solver()
s2.add(s1.assertions())
print s2.check()
print s2.model()
Это выводит:
sat
[x = 3]
Я полагаю, вы можете использовать этот трюк для создания своих собственных комбинаций.
Комментарии:
1. Привет, под объединением я подразумеваю повторное использование производных как части обоих решателей. Объединение утверждений в этом случае не дает никаких преимуществ в производительности.
2. Я не думаю, что вы можете поделиться «знаниями» каким-либо значимым образом. Обратите внимание, что z3py ‘Solver’ представляет собой тонкую оболочку поверх базового контекста решателя, и, насколько я знаю, нет никакого способа объединить их каким-либо образом. Возможно, вы захотите спросить на их сайте проблем, возможно ли это. (Хотя имейте в виду, что даже если это возможно на базовом уровне, это не означает, что он будет доступен пользователю через Python API.)