Array Model Output

[bdrodes]

I'm using the python api. I was previously on version 4.5.1.0.post2 and upgraded to version 4.8.6.0. The model output for arrays is drastically different, and I'm not sure how to interpret it. I'm used to seeing something of the form:

[a = [41 -> 100, else -> 100],
 k!0 = [41 -> 100, else -> 100]]

But now the output is:

In [6]: s.model()                                                                                                                                                                                                                           
Out[6]: [a = K(Int, 100)]

How do I get an output that has index/value pairs like the prior version?

[NikolajBjorner]

Models are now compressed. K(Int, 100) is a constant array with value 100. It is the same as [else -> 100]. Since 41 also results in 100, there is no need to list both 41 -> 100 and else -> 100.

[bdrodes]

Yea I can see that makes sense, but I wonder if there is a way to get a clean output for an array when more constraints are added.

For example

a = Array('a', IntSort(), IntSort())
b = Array('b', IntSort(), IntSort())
s.add(a[1] == IntVal(1))
s.add(b[1] == IntVal(2))
s.add(a[2] == IntVal(3))
s.add(ForAll(Int('z'), If(Int('z') == 1, b[Int('z')] == b[Int('z')], b[Int('z')] == a[Int('z')])))

In the older version getting a model for this yields, where I can easily see all elements and indices:

[b = [else -> k!1!4(k!2(Var(0)))],
 a = [else -> k!0!3(k!2(Var(0)))],
 k!0 = [else -> k!0!3(k!2(Var(0)))],
 k!0!3 = [1 -> 1, else -> 3],
 k!1 = [else -> k!1!4(k!2(Var(0)))],
 k!2 = [1 -> 1, else -> 2],
 k!1!4 = [1 -> 2, else -> 3]]

Whereas the new version yields:

[b = [else ->
      If(If(Var(0) == 1, 1, 2) == 1,
         2,
         If(If(Var(0) == 1, 1, 2) == 2, 3, 4))],
 a = [else ->
      If(If(Var(0) == 1, 1, 2) == 1,
         1,
         If(If(Var(0) == 1, 1, 2) == 2, 3, 0))],
 k!20 = [else ->
         If(If(Var(0) == 1, 1, 2) == 1,
            1,
            If(If(Var(0) == 1, 1, 2) == 2, 3, 0))],
 k!21 = [else ->
         If(If(Var(0) == 1, 1, 2) == 1,
            2,
            If(If(Var(0) == 1, 1, 2) == 2, 3, 4))],
 Ext = [(as-array, as-array) -> 1, else -> 0]]

Perhaps this is me being silly, but I find the earlier format easier to read and easily assess the state of my array, whereas the newer version requires more unpacking. Is there any way to getting a more easily readable string output, or do I basically need to make a custom parser to do that now? Thanks.

[NikolajBjorner]

The new model you display definitely looks convoluted.
If I do

from z3 import *
a = Array('a', IntSort(), IntSort())
b = Array('b', IntSort(), IntSort())
s = Solver()
s.add(a[1] == IntVal(1))
s.add(b[1] == IntVal(2))
s.add(a[2] == IntVal(3))
s.add(ForAll(Int('z'), If(Int('z') == 1, b[Int('z')] == b[Int('z')], b[Int('z')] == a[Int('z')])))

s.check()
mdl = s.model()
print(mdl)
print(mdl.sexpr())

I get the following output:

[b = Store(K(Int, 3), 1, 2),
 a = Store(K(Int, 3), 1, 1),
 k!0 = [1 -> 1, else -> 3],
 k!1 = [1 -> 2, else -> 3],
 Ext = [(as-array, as-array) -> 1, else -> 0]]
(define-fun b () (Array Int Int)
  (store ((as const (Array Int Int)) 3) 1 2))
(define-fun a () (Array Int Int)
  (store ((as const (Array Int Int)) 3) 1 1))
(define-fun k!0 ((x!0 Int)) Int
  (ite (= x!0 1) 1
    3))
(define-fun k!1 ((x!0 Int)) Int
  (ite (= x!0 1) 2
    3))

It isn't as convoluted, but you could argue that you prefer to untangle the store sequence into a lookup-table format.

[NikolajBjorner]

In another note, you can obtain uncompressed behavior by setting:

set_param("model.compact", False)
set_param("model_compress", False)

It is a design flaw that there are two aliases for the same effect.
The second parameter is set to True by default, the first is set to False by default.
I will try to address this, but it gives you a way to obtain the "old style".

[bdrodes]

That's awesome. I think this is exactly what I was looking for. Thanks

[NikolajBjorner]

This issue exposed that there are two parameters with overlapping functionality.
I have now removed model_compress.
The example now works with the following setting:

from z3 import *
a = Array('a', IntSort(), IntSort())
b = Array('b', IntSort(), IntSort())
s = Solver()
s.add(a[1] == IntVal(1))
s.add(b[1] == IntVal(2))
s.add(a[2] == IntVal(3))
s.add(ForAll(Int('z'), If(Int('z') == 1, b[Int('z')] == b[Int('z')], b[Int('z')] == a[Int('z')])))

s.set("model.compact", False)
s.check()
mdl = s.model()
print(mdl)
print(mdl.sexpr())