Verifying consistency of strict and non-strict partial orders constraints I am building a set of constraints of the kind $x &lt; y$ and $x \leq y$, where $&lt;$ is a strict order and $\leq$ is a non-strict order on the same set, and $x$ and $y$ are abstract variables representing elements of the set.  The laws that relate the two orderings are the same as $&lt;$ and $\leq$ for integers.  I need to make sure that each constraint that I add does not make the set inconsistent (e.g. adding $x &lt; y$ and then $y &lt; x$ I'd get an error).

Now, if I had only the $&lt;$ constraints I could get away with generating a graph and then doing a topological sort, or with disjoint-sets.  The problem is that I'm not sure how to handle the additional $\leq$ constraints.

One idea is to express $x \leq y$ as $\neg (x &gt; y)$, and to keep two graphs:  one for the actual $&lt;$ relations and one for the negated ones.  Then we'd need to check, at each new constraints, whether there are overlapping paths between the two graphs, in which case we'd have a problem.  However this seems rather costly since it seems to me that we'd need to analyze all the pairs each time.

Another idea would be to 'collapse' $\leq$ relations to equalities or $&lt;$ when needed, but again I'm quite uncertain on the details.

Is this problem described somewhere?  As a bonus, I'd like the data structures involved to be purely functional.
You may find it helpful to think of your problem in terms of equalities and strict inequalities. 

In the case of the constraints being equalities or disequalities there is a simple saturation procedure based on transitivity of equality.  Strict inequalities can be represented by directed edges in a graph. You can then compute strongly connected components to reason about dependencies between sets of variables. If you have uninterpreted functions, you can use congruence closure.

I would imagine that the first results date to the 50s or at least the 70s, but I do not have a good reference for you. Recent literature in which these ideas occur is the paper below.


  An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions, Georg Weissenbacher.