CODEWITHSUNDEEP
z3z3py
makkiato
makkiato

Reputation: 67

Enumerating models in Z3 over finite domains

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

Upvotes: 0

Views: 296

Answers (1)

alias
alias

Reputation: 30460

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.

Upvotes: 1

Related Questions