Add LTE function for completeness and fix bug in LT

diff --git a/src/Backend/constraint.c b/src/Backend/constraint.c
index 3e0d0a8165916b2e536860a4a2f33dda38acb77d..c7cac9867f47afb9d736bee81ffa9314298cc2f0 100644 (file)
--- a/src/Backend/constraint.c
+++ b/src/Backend/constraint.c
@@ -883,7 +883,7 @@ Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
 
 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2){
        if(numvars == 0 )
-               return E_True;
+               return E_False;
        Edge result =constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
        for (uint i = 1; i < numvars; i++) {
                Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
@@ -891,4 +891,16 @@ Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2){
                result = constraintOR2(cnf, lt, eq); 
        }
        return result;
-}
\ No newline at end of file
+}
+
+Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2){
+       if(numvars == 0 )
+               return E_True;
+       Edge result =constraintIMPLIES(cnf, var1[0], var2[0]);
+       for (uint i = 1; i < numvars; i++) {
+               Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
+               Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result); 
+               result = constraintOR2(cnf, lt, eq); 
+       }
+       return result;
+}

diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h
index 772f6c8dafe88bdd312c845d32e676baa1a24278..02fe3da617731c300e8d6a9adbb4f4cd009ab229 100644 (file)
--- a/src/Backend/constraint.h
+++ b/src/Backend/constraint.h
@@ -212,6 +212,7 @@ Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);
 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);
+Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);
 
 extern Edge E_True;
 extern Edge E_False;