title: Residual constraints with reification in clpfd
body: <p>I defined reified variants of the 
  <a href="http://www.swi-prolog.org/man/clpfd.html" rel="nofollow">clpfd</a> constraints <code>(#&lt;)/2</code>, <code>(#=&lt;)/2</code>, <code>(#&gt;=)/2</code> and <code>(#&gt;)/2</code>:</p>
  
  <pre><code>:- use_module(library(clpfd)).
  
  ltA(X,Y,Truth)  :- X #&lt;  Y #&lt;==&gt; B, bool01_truth(B,Truth).
  ltB(X,Y, true)  :- X #&lt;  Y.
  ltB(X,Y,false)  :- X #&gt;= Y.
  
  lteA(X,Y,Truth) :- X #=&lt; Y #&lt;==&gt; B, bool01_truth(B,Truth).
  lteB(X,Y, true) :- X #=&lt; Y.
  lteB(X,Y,false) :- X #&gt;  Y.
  
  gteA(X,Y,Truth) :- X #&gt;= Y #&lt;==&gt; B, bool01_truth(B,Truth).
  gteB(X,Y, true) :- X #&gt;= Y.
  gteB(X,Y,false) :- X #&lt;  Y.
  
  gtA(X,Y,Truth)  :- X #&gt;  Y #&lt;==&gt; B, bool01_truth(B,Truth).
  gtB(X,Y, true)  :- X #&gt;  Y.
  gtB(X,Y,false)  :- X #=&lt; Y.
  </code></pre>
  
  <p>Of course, <code>ltA/3</code> and <code>ltB/3</code> are <strong>logically equivalent</strong>, as are
  <code>lteA/3</code> and <code>lteB/3</code>, <code>gteA/3</code> and <code>gteB/3</code>, and <code>gtA/3</code> and <code>gtB/3</code>.</p>
  
  <p>The answers I get using these predicates, however, differ regarding size and readability. I ran the following queries with SWI-Prolog 7.1.37:</p>
  
  <p><strong>Good news, first!</strong></p>
  
  <pre><code>?- lteA(X,Y,Truth).
  Truth = false, Y#=&lt;X+ -1 ;
  Truth = true,  Y#&gt;=X.
  ?- lteB(X,Y,Truth).
  Truth = true,  Y#&gt;=X ;
  Truth = false, Y#=&lt;X+ -1.
  
  ?- gteA(X,Y,Truth).
  Truth = false, X#=&lt;Y+ -1 ;
  Truth = true,  X#&gt;=Y.
  ?- gteB(X,Y,Truth).
  Truth = true,  X#&gt;=Y ;
  Truth = false, X#=&lt;Y+ -1.
  </code></pre>
  
  <p><strong>Ok!</strong> But what about the other two?</p>
  
  <pre><code>?- ltA(X,Y,Truth).
  Truth = false, X+1#=_G968, Y#=&lt;_G968+ -1 ;
  Truth = true,  X+1#=_G912, Y#&gt;=_G912.
  ?- ltB(X,Y,Truth).
  Truth = true,  X#=&lt;Y+ -1 ;
  Truth = false, X#&gt;=Y.
  
  ?- gtA(X,Y,Truth).
  Truth = false, X#=&lt;_G1301+ -1, Y+1#=_G1301 ;
  Truth = true,  X#&gt;=_G1243,     Y+1#=_G1243.
  ?- gtB(X,Y,Truth).
  Truth = true,  Y#=&lt;X+ -1 ;
  Truth = false, Y#&gt;=X.
  </code></pre>
  
  <p><strong>Not quite!</strong> </p>
  
  <p>How do I get compact answers with <code>ltA/3</code> and <code>gtA/3</code>---just like with <code>lteA/3</code> and <code>gteA/3</code>?</p>