在z3中声明有限排序

问题描述 投票:1回答:1

让我们假设我有一个finite集{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))

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

一些澄清:也许不是我需要的变量,因为{x == y,y == z,x == z}很明显,但是我要建模的行为更像这样{x == 1,2 == z,x == z}显然是不饱和的(假设像{1,2,3,4}这样的有限排序)。

python z3
1个回答
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
© www.soinside.com 2019 - 2024. All rights reserved.