z3 - Trouble with TransitiveClosure function in Z3Py

Question

I am trying to model graph connectivity with Z3. Specifically I am partitioning a graph and need the subgraphs to remain connected. However TransitiveClosure doesn't work as I expect. I model edges with F

Here's a 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))

This is apparently SAT, which doesn't make much sense to me. If I change s.add(FX(A,C)) to s.add(Not(FX(A,C))).

Why is this? C should not be a member of FX. Am I somehow setting FX(A,C) == True) by adding it to the model? Why doesn't that conflict with the definition of FX.

The output/connection lines of the model are hard to understand so I'm not quite sure what's going on.

question from:https://stackoverflow.com/questions/65936759/trouble-with-transitiveclosure-function-in-z3py

Answer 1

I am working with tclosures as well and found this helpful: https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-transitive-closure

Maybe there is an answer to your 2nd question as well.