CODEWITHSUNDEEP
pythonz3z3py
Johan
Johan

Reputation: 615

Z3 python model compareson

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.

Upvotes: 0

Views: 342

Answers (1)

alias
alias

Reputation: 30418

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?

Upvotes: 1

Related Questions