Special Relations

[philzook58]

I was interesting in the method behind https://microsoft.github.io/z3guide/docs/theories/Special%20Relations. It states that the decision procedure is using "Ford-Fulkerson push relabeling graphs". After thinking about it a bit, it isn't obvious to me how this problem maps into maximum flow and was curious to hear any elaboration or references you might have.
Looking at what I think is the implementation https://github.com/Z3Prover/z3/blob/master/src/smt/theory_special_relations.cpp it seems to rely on the difference logic module for a lot but not all of the functionality. Does the difference logic module implement the maximum flow push relabelling? I was under the impression that difference logic solvers were based on Bellman-Ford or Floyd-Warshall shortest path algorithms.

Thanks!

[NikolajBjorner]

so Bellman-Ford. Doc bug?