Combining models

[norhh]

Consider the following example:

> s.add(And(a>10, a<20))
> s.check()
> saved_model = s.model()

We can use the solution saved_model to solve something like And(a > 10, a < 20, b > 10) as follows

> new_constraint = saved_model.eval(And(a > 10, a < 20, b > 10))
> new_solver = Solver()
> new_solver.add(new_constraint)
> new_solver.check()
> secondary_model = new_solver.model()

Is there a way to combine these two models saved_model and secondary_model?
I need something like total_model = saved_model + secondary_model

[nunoplopes]

Not sure I understand the question.
The two models may not even be compatible. One may have a=1 and the other a=2. How do you combine them? Can you give an example of what you want to do?

[norhh]

One may have a=1 and the other a=2. How do you combine them?
Yes, there are cases where two models may not be combinable, but in the cases where the variables in model_1 are not in model_2 and vice versa, we can directly combine them. I want to know any way to combine such models into a new model using z3-py. I am currently maintaining two models to handle such scenarios.

In symbolic execution, In most cases, you can use some previously solved constraint's model to solve the existing constraint partially (as there are cases where a new condition is added to a new variable). A way of combining models with independent variables might help.

[nunoplopes]

I don't think Z3 has support for that. You've to do it yourself manually.

BTW, your 'eval()' call is a bit strange. Print new_contraint to see if what you're obtaining is what you expect. The new_solver is likely under constrained.

[norhh]

I get something like Not(b <= 10) using model.eval(), which is fed to the new solver