Declaring a finite sort in z3

user_4145074 0
Viewed 333

Let us assume I have a finite set {e1, e2, e3}. I want to be able to distinguish transitive constraints so I can handle this behavior:

from z3 import *

solver = Solver()
A = DeclareSort('A')
x = Const('x', A)
y = Const('y', A)
z = Const('z', A)
solver.add(x!=y)
solver.add(y!=z)
solver.add(x==z)

assert solver.check() != z3.sat

The only way I found to solve it is changing the last constraint with this one:

solver.add(ForAll([x,z],x==z))

Is this the way to model it? Is there any finite sort available? Should I need to add all the constraints declaring the elements different from each other?

Some clarification: Maybe is not a variable what I need, because {x == y, y == z, x == z } is clearly sat, but the behavior I want to model is more like this {x == 1, 2 == z, x == z } that is obviously unsat (assuming some finite sort like {1,2,3,4}).

z3 python
1 Answers

What I was looking for was the EnumSort:

from z3 import *

solver = Solver()
S, (a, b, c) = EnumSort('round', ['a','b','c'])

x = Const("x", S)
z = Const("z", S)
solver.add(x==a)
solver.add(z==b)
solver.add(x==z)

assert solver.check() != z3.sat
user_41450740
Related