0

I'm using Z3 with the ml interface. I had created a formula f(x_i) that is satisfiable, according to the solver Solver.mk_simple_solver ctxr.

The problem is: I can get a model, but he find me values only for some variables of the formula, and not all (some of my Model.get_const_interp_er end with a type None)

How can it be possible that the model can give me only a part of the x_ir? In my understanding, if the model work for one of the values, it means that the formula was satisfiable (in my case, it is) and so all the values can be given...

I don't understand something.. Thanks for reading me!

Andreas Rossberg
  • 34,518
  • 3
  • 61
  • 72
user8622655
  • 41
  • 3

1 Answers1

0

You should always post full examples so people can help with actual coding issues; without seeing your actual code, it's impossible to know what might be the actual reason.

Having said that, this sounds very much like the following question: Why Z3Py does not provide all possible solutions So, perhaps the answer given there will help you.

Long story short: Z3 models will only contain values for variables that matter for the model. For anything that is not explicitly assigned, any value will do. There are ways to get "full" models as explained in that answer of course; which I'm sure is also possible from the ML interface.

alias
  • 28,120
  • 2
  • 23
  • 40