python - 在 z3 中声明有限排序

Question

让我们假设我有一个有限集{e1, e2, e3}。我希望能够区分传递约束，以便处理这种行为:

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

我发现解决它的唯一方法是用这个改变最后一个约束:

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

这是建模的方式吗？有可用的有限排序吗？我是否需要添加声明元素彼此不同的所有约束？

一些说明: Maybe 不是我需要的变量，因为 {x == y, y == z, x == z } 显然是 sat，但我想要建模的行为更像是这样的 {x == 1, 2 == z, x == z } 显然是不满足的(假设某种有限排序，如 {1,2,3,4})。

Answer 1

我要找的是 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