【发布时间】：2021-01-28 12:03:16
【问题描述】：
我正在尝试使用 Z3 对图形连接进行建模。具体来说，我正在对图进行分区，并且需要子图保持连接。然而TransitiveClosure 并没有像我预期的那样工作。我用 F 建模边缘
这是一个 MWE：
s = Solver()
N = DeclareSort('N')
a,b,c = Consts('a b c', N)
F = Function(N,N,BoolSort())
s.add(F(A,B) == True)
s.add(F(B,A) == True)
s.add(F(B,C) == False)
s.add(F(C,B) == False)
s.add(F(A,C) == False)
s.add(F(C,A) == False)
s.add(A != B, B != C, C != A)
FX = TransitiveClosure(F)
s.add(FX(A,C))
这显然是 SAT，对我来说没有多大意义。如果我将s.add(FX(A,C)) 更改为s.add(Not(FX(A,C)))。
这是为什么？ C 不应该是 FX 的成员。我是否通过将FX(A,C) == True) 添加到模型中来设置它？为什么这和 FX 的定义不冲突。
模型的输出/连接线很难理解，所以我不太确定发生了什么。
【问题讨论】：
-
我不确定
TransitiveClosure是否应该在IntSort()等任意/无限域上工作。我怀疑它可能仅在底层排序是新的排序声明时才有效。但是，文档对此并不清楚，因此您可能想在github.com/Z3Prover/z3/issues 询问以获得更明确的答案。如果您这样做，请发布更新！ -
好吧，这是有道理的。我将它切换为一个未解释的排序，每个顶点有一个常数。如果我对这种新类型做同样的事情，我仍然会在不应该的情况下获得 SAT。如果我将所有其他边缘函数设置为 false，为什么我会断言存在两个断开连接的传递闭包？回家后我会更新上面的代码。