1

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.

Patrick Trentin
  • 7,126
  • 3
  • 23
  • 40
adrianX
  • 619
  • 7
  • 21

1 Answers1

0

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
Nikolaj Bjorner
  • 8,229
  • 14
  • 15
  • for pysmt, does not seem like i can do that, but in any case, i can move away from pysmt if need be. if i do the calls as you mentioned, do i get significant performance improvement? – adrianX Mar 18 '17 at 14:12
  • 1
    pysmt does not seem to support any such feature yet, but they provide a way to access functionality that is not wrapped by their library, see here: http://pysmt.readthedocs.io/en/latest/tutorials.html#how-to-access-functionalities-of-solvers-not-currently-wrapped-by-pysmt – Christoph Wintersteiger Mar 23 '17 at 19:05
  • hello Christoph, yes that helps! should had read the docs more thoroughly. thank you! – adrianX Mar 24 '17 at 00:40