Z3 python model compareson

0
votes

Having a set of formulas and using z3py to create two model old_model = solver.model() and new_model. How can a list of variable names be obtain that have different assignments in the two models?

A general solution is needed that consider all free variables in the set of formulas. If possible there are case where a variable is defined by var = Int('varname')m and used only in a formula ForAll(var, ...), that variable var need not be considered when the models are begin compared.

The idea is to use the comparison during debugging and to see if there exist any unexpected variables that define differences between the models, or the variable should not appear in the model.

1
pythonz3z3py

1 Answers

1
votes

It's not clear what you are asking; but when z3 gives you a model, it's simply a dictionary mapping variables to their values. You can easily hold on to them in Python:

from z3 import *

s = Solver()

x, y, z = Ints('x y z')

s.add(x + y > 5)

s.add(ForAll([z], z > z-1))

s.check()
m = s.model()

print m

# get the variables:
for v in m:
  print v

This prints:

[y = 0, x = 6]
y
x

As you see, y and x are there, and z isn't; as you wanted I think. If you have multiple models, you can simply query them separately and look for differences and do whatever programming you wish. Is this what you're looking for?