Checking all solutions for array (as-array) in Z3PY

Question

My problem is that I have to get all possible models for an array of the form as-array. The code I have done for this is the following:

s = Solver()
check = s.check()
while (str(check) == "sat"):
      mod = s.model()
      block = []
      for var in mod.decls():
         block.append(var() != mod[var])
      s.add(Or(block))
      check = s.check()

var can take values of type as-array among others and when I run the line s.add(Or(block)), the next time I run the line check = s.check it returns unknown

Is there any other way to do it?

------- Edit -------

I have found a way to get all possible models for an array of the form as-array that was the previous problem, the way I have done it is to create a variable that represents the size of the array and from i = 0 to i = n (where n is the size), make a[i]!= x being "a" the array and "x" the value that takes "a[i]".

My problem now is that I have a datatype of the form "mk-pair" whose first argument is an array of the form as-array and an Integer that indicates the size of the array.

When I get a model I have it in the form mk-pair(as-array, 30) (for example), being 30 the size of the array.

The problem is that I can't find a way to obtain all the possible models, since if I deny the type of data (a != x, assuming that "a" is the datatype and "x" its value), it returns me unknown and if I do the first (as-array[0] != x), what I am really denying is as-array, not the variable "a"(which is of the form mk-pair(as-array, Int) ) and when I ask for models several times I get duplicate results.

Any way to do this?

score 0 · Answer 1 · answered Feb 05 '20 at 19:05

0

This is a frequent request. Your blocking clause will have to be modified to account for the possibility of arrays. It should also watch out for data-types, functions, floats, ... Definitely doable, and the code to this answer will get you started: (Z3Py) checking all solutions for equation

Note that you can't in general "block" functions. Arrays can also be problematic as you will not be able to "recast" them as a blocker if they have an infinite support. (That is, think of an array that maps i'th element to value i. There's no finite representation of this that you can easily write in SMTLib without quantifiers.) Aside from those considerations, I believe the trick in the above answer can get you far enough, handling most cases.

answered Feb 05 '20 at 19:05

alias

28,120
2
23
40

I have edited with a possible solution that I found for my previous problem and with a new one. – alecille Feb 17 '20 at 17:27
In general, arrays and functions cannot be handled in `all-sat` scenarios if they have infinite support. (There would be no way to add a "blocking" clause.) But if they're over finite domains with finitely many elements defined in the model, you can work around by adding a blocking cause for those elements only. Your question is hard to follow though, please post a new one with sample code that people can actually run to replicate. You'll get better answers that way. – alias Feb 18 '20 at 16:49

Checking all solutions for array (as-array) in Z3PY

1 Answers1