Enumerating models in Z3 over finite domains

Question

I am experimenting with FD in Z3 with Python.

I have the following code:

F = FiniteDomainSort('F', 3)
u=Const('u', F)
v=Const('v', F)
s = Solver()
s.add(u !=v )

So, variables {u,v} over the FD sort {1,2,3}, and they need to be distinct..

Goal: I want to enumerate all possible models.

I have first writing this code, to print the 'first' three models:

i = 0
while s.check()==CheckSatResult(Z3_L_TRUE) and i<3:
    m=s.model()
    print(m)
    s.add(Or(u != m.get_interp(u), v != m.get_interp(v)))
    print(s.sexpr())
    i = i+1

However, it doesn't seem to work. I always get the same model despite the new constraints being correctly added:

[v = 1, u = 0]
(declare-fun v () F)
(declare-fun u () F)
(assert (distinct u v))
(assert (or (distinct 0 u) (distinct 1 v)))
(rmodel->model-converter-wrapper
v -> 1
u -> 0
)

[v = 1, u = 0]
(declare-fun v () F)
(declare-fun u () F)
(assert (distinct u v))
(assert (or (distinct 0 u) (distinct 1 v)))
(assert (or (distinct 0 u) (distinct 1 v)))
(rmodel->model-converter-wrapper
v -> 1
u -> 0
)

[v = 1, u = 0]
(declare-fun v () F)
(declare-fun u () F)
(assert (distinct u v))
(assert (or (distinct 0 u) (distinct 1 v)))
(assert (or (distinct 0 u) (distinct 1 v)))
(assert (or (distinct 0 u) (distinct 1 v)))
(rmodel->model-converter-wrapper
v -> 1
u -> 0
)

I have found the following code from this answer:

def get_models(F, M):
    result = []
    s = Solver()
    s.add(F)
    while len(result) < M and s.check() == sat:
        m = s.model()
        result.append(m)
        # Create a new constraint the blocks the current model
        block = []
        for d in m:
            # d is a declaration
            if d.arity() > 0:
                raise Z3Exception("uninterpreted functions are not supported")
            # create a constant from declaration
            c = d()
            if is_array(c) or c.sort().kind() == Z3_UNINTERPRETED_SORT:
                raise Z3Exception("arrays and uninterpreted sorts are not supported")
            block.append(c != m[d])
        s.add(Or(block))
    return result

But it seems to hit the same problem of my code:

F = FiniteDomainSort('F', 3)
u=Const('u', F)
v=Const('v', F)
s = Solver()
F = [u!=v]
print(get_models(F,3))

[[v = 0, u = 1], [v = 0, u = 1], [v = 0, u = 1]]

QUESTION: What would be a working method for enumerating all models when working with finite domains?

THANKS

alias · Accepted Answer · 2022-02-02T20:48:13.517

1

Finite-domain sorts in z3 is only intended to be used by the Datalog engine. Other uses are invalid, and unsupported. Ideally, you'd expect z3 to catch such uses and reject them; alas it doesn't do that causing these sorts of confusions.

See https://github.com/Z3Prover/z3/issues/4842 for details.

As noted in the above ticket, the recommended solution is to use enumerations instead.

edited Feb 02 '22 at 20:48

answered Feb 02 '22 at 20:42

alias

28,120
2
23
40

thanks a lot! Solved my problems. In my tests so far, it looks like enumerations (say, from 1... k) runs much faster than Int type, with added constratints 1<= x <= k. Good to know! thanks! – makkiato Feb 03 '22 at 16:21
1

Yeah, if you don't need arithmetic, enumerations are definitely the way to go. – alias Feb 03 '22 at 17:01

Enumerating models in Z3 over finite domains

1 Answers1