Adding circuit-based encoding for LT and GT

diff --git a/src/Backend/constraint.c b/src/Backend/constraint.c
index 62c3c81b6c603b8534a4e11d565f72f0f8658e17..3e0d0a8165916b2e536860a4a2f33dda38acb77d 100644 (file)
--- a/src/Backend/constraint.c
+++ b/src/Backend/constraint.c
@@ -847,7 +847,7 @@ Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
 }
 
 /** Generates a constraint to ensure that all encodings are less than value */
-Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
+Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
        Edge orarray[numvars];
        Edge andarray[numvars];
        uint andi = 0;
@@ -880,3 +880,15 @@ Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
        }
        return constraintAND(cnf, numvars, array);
 }
+
+Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2){
+       if(numvars == 0 )
+               return E_True;
+       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]);
+               Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result); 
+               result = constraintOR2(cnf, lt, eq); 
+       }
+       return result;
+}
\ No newline at end of file

diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h
index b2488178134bc82bc50ee5680dd9622154dca1ad..772f6c8dafe88bdd312c845d32e676baa1a24278 100644 (file)
--- a/src/Backend/constraint.h
+++ b/src/Backend/constraint.h
@@ -209,8 +209,9 @@ Literal introProxy(CNF *cnf, Edge e, CNFExpr *exp, bool isNeg);
 void outputCNF(CNF *cnf, CNFExpr *expr);
 
 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
-Edge generateLTConstraint(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);
 
 extern Edge E_True;
 extern Edge E_False;

diff --git a/src/Backend/satfuncopencoder.c b/src/Backend/satfuncopencoder.c
index b8a814d54d46f43f3c33191cbc6818c70c274c54..8dd753258a0b8a185706eaf2687eb51615336898 100644 (file)
--- a/src/Backend/satfuncopencoder.c
+++ b/src/Backend/satfuncopencoder.c
@@ -197,19 +197,6 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction *
 
 Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate *constraint) {
        PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
-
-       switch (predicate->op) {
-       case EQUALS: {
-               return encodeCircuitEquals(This, constraint);
-       }
-       default:
-               ASSERT(0);
-       }
-       exit(-1);
-}
-
-Edge encodeCircuitEquals(SATEncoder *This, BooleanPredicate *constraint) {
-       PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
        ASSERT(getSizeArraySet(&predicate->domains) == 2);
        Element *elem0 = getArrayElement( &constraint->inputs, 0);
        encodeElementSATEncoder(This, elem0);
@@ -219,10 +206,16 @@ Edge encodeCircuitEquals(SATEncoder *This, BooleanPredicate *constraint) {
        ElementEncoding *ee1 = getElementEncoding(elem1);
        ASSERT(ee0->numVars == ee1->numVars);
        uint numVars = ee0->numVars;
-       ASSERT(numVars != 0);
-       Edge carray[numVars];
-       for (uint i = 0; i < numVars; i++) {
-               carray[i] = constraintIFF(This->cnf, ee0->variables[i], ee1->variables[i]);
+       switch (predicate->op) {
+               case EQUALS:
+                       return generateEquivNVConstraint(This->cnf, numVars, ee0->variables, ee1->variables);
+               case LT:
+                       return generateLTConstraint(This->cnf, numVars, ee0->variables, ee1->variables);
+               case GT:
+                       return generateLTConstraint(This->cnf, numVars, ee1->variables, ee0->variables);
+               default:
+                       ASSERT(0);
        }
-       return constraintAND(This->cnf, numVars, carray);
+       exit(-1);
 }
+

diff --git a/src/Backend/satfuncopencoder.h b/src/Backend/satfuncopencoder.h
index 8b39194026bdcba11fa6767e15fee70d228fa44b..a9d0663133da92e399cc5ea6b4194e1bade976a7 100644 (file)
--- a/src/Backend/satfuncopencoder.h
+++ b/src/Backend/satfuncopencoder.h
@@ -5,6 +5,5 @@ Edge encodeOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *const
 Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint);
 void encodeOperatorElementFunctionSATEncoder(SATEncoder *encoder,ElementFunction *This);
 Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate *constraint);
-Edge encodeCircuitEquals(SATEncoder *This, BooleanPredicate *constraint);
 
 #endif