Являются ли кэши Z3 аддитивными?

Question

Мне известно, что в Z3 есть кэширование на основе стека, где можно добавлять и кэшировать дополнительные формулы.Существует ли встроенный способ или расширение, позволяющее объединять два кэша Z3?

Пример (Z3 py)

from z3 import Solver

solver = Solver()
solver.push()
solver2 = Solver()
# solver.combine(solver2) ?

Answer 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]

Вы можете использовать этот трюк для создания своих собственных комбинаций, я полагаю.