how to duplicate solvers in pysmt for divergent incremental solving?

Skip to first unread message

Ming Yang Koh

Mar 19, 2017, 10:23:13 PM3/19/17
to pySMT

i am using pySMT (and only using Z3 through pySMT for now). 

my script's purpose requires me to add many assertions (e.g. assertions a, b, c) and at many points in time, the assertions that needs to be added diverges (e.g. assertion x and assertion y). 
At the moment, i create multiple solver instances and re-add the assertions from scratch and then solve them independently. for example, the first solver will have assertion a, b, c and x, and the second solver will have assertion a, b, c, and y. i think that performance can be improved if i can 

a) duplicate the solvers, and also 
b) if i can incrementally solve and bring forward this context when i duplicate the solver.  

for (b), i think Z3 supports something like in the form of context:

may i seek your advise on the best way for (a) and (b) can be done using pySMT?

thank you and regards!

Andrea Micheli

Mar 20, 2017, 5:09:49 AM3/20/17
to Ming Yang Koh, pySMT

Currently PySMT does not support this feature: the main reason is that not all the SMT solvers we use support it. 

However, you can try using a single solver instance using solving under assumptions.
You can add all the non-common assertions as implications of fresh Boolean variables and the you ask for a solution assuming a subset of these Boolean variables. 

For example:

with Solver(...) as s:
   s.add_assertion(phi) # a fixed assertion, common to all the "instances"
   x_ctrl = FreshSymbol(typing.BOOL)
   y_ctrl = FreshSymbol(typing.BOOL)
   s.add_assertion(Implies(x_ctrl, x)) # ading assertion x as an implication 
   s.add_assertion(Implies(y_ctrl, y)) # ading assertion y as an implication

   s.solve() # solving for psi only
   s.solve([x_ctrl]) # solving for psi & x
   s.solve([y_ctrl]) # solving for psi & y
   s.solve([x_ctrl, y_ctrl]) # solving for psi & x & y



You received this message because you are subscribed to the Google Groups "pySMT" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
To post to this group, send email to
To view this discussion on the web visit
For more options, visit

Ming Yang Koh

Mar 23, 2017, 8:32:07 PM3/23/17
to pySMT
hello Andrea! 

that helps! thank you!
To unsubscribe from this group and stop receiving emails from it, send an email to
Reply all
Reply to author
0 new messages