Newer versions of Z3 no longer keep/print all function instances

Viewed 35

Notice in the new versions of Z3, the model only prints the arguments to the function that have a value other than the default. Is there a way to return to the old method of receiving all instances, including those that map to the default value?

Code:

import z3

config_init = z3.Function('config_init', z3.IntSort(), z3.IntSort(), z3.IntSort(), z3.IntSort())


def fooY(W, X, Y, Z):
    return config_init(W, X, Y) == Z


s = z3.Solver()
s.add(fooY(1, 2, 3, 4))
s.add(fooY(2, 3, 4, 5))
s.add(fooY(1, 2, 8, 4))
s.add(fooY(2, 3, 9, 5))

print("Z3 Version", z3.get_version())
if s.check() == z3.sat:
    mod = s.model()
    print(mod)
else:
    print('failed')
    print(s.unsat_core())

Old Z3 Output

('Z3 Version', (4L, 5L, 1L, 0L))
[config_init = [(1, 2, 3) -> 4,
                (2, 3, 4) -> 5,
                (1, 2, 8) -> 4,
                (2, 3, 9) -> 5,
                else -> 4]]

New Z3 Output

Z3 Version (4, 8, 7, 0)
[config_init = [(2, 3, 4) -> 5, (2, 3, 9) -> 5, else -> 4]]
0 Answers
Related