CODEWITHSUNDEEP
pythonz3pysmt
adrianX
adrianX

Reputation: 627

how to duplicate a solver created in pysmt?

in pysmt, assuming that i have created a solver and added many assertions. now, i want to make a copy of the solver instance because i need to add different assertions to the solver. how do i do so? i need to do so in order to improve the performance of of code.

i tried to do things like copy(), clone() and deepcopy() but they all do not work. so my current workaround now is to keep track of all the assertions and create new solver instances and build it up from scratch everytime.

Upvotes: 1

Views: 163

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

For your scenario, the easiest seems to be as follows:

You can retrieve all assertions from a solver using the "assertions()" method.

from z3 import *
x, y = Ints('x y')
s1 = Solver()
s1.add(x <= y)
print s1
s2 = Solver()
s2.add(s1.assertions())
print s2

Upvotes: 0

Related Questions