how to duplicate solvers in pysmt for divergent incremental solving?

[Ming Yang Koh]

Hello!

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:

http://stackoverflow.com/questions/36364214/how-to-quick-copy-pyz3-solvers

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

thank you and regards!

damon

[Andrea Micheli]

Hello!

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

HTH

Andrea

--
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 pysmt+unsubscribe@googlegroups.com.
To post to this group, send email to py...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/pysmt/1952f2d1-22f1-41c1-893d-ce4ffc43c448%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Ming Yang Koh]

hello Andrea! 

that helps! thank you!

To unsubscribe from this group and stop receiving emails from it, send an email to pysmt+un...@googlegroups.com.