Z3Py中transitivecloclose函数的问题

Question

我正在尝试与Z3建模图连接。具体来说，我正在划分一个图，并且需要子图保持连接。然而，TransitiveClosure不像我期望的那样工作。I用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)添加到模型中来设置它?为什么这与外汇的定义不冲突呢?

模型的输出/连接线很难理解，所以我不太确定发生了什么。

Answer 1

我也在使用t闭包，发现这很有帮助:https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-transitive-closure

也许你的第二个问题也有答案。