From 510efd1d0ee344fb5bbf4fe8ac94940d7a806402 Mon Sep 17 00:00:00 2001
From: Hamed <hamed.gorjiara@gmail.com>
Date: Tue, 22 Aug 2017 08:50:27 -0700
Subject: [PATCH] Adding circuit-based encoding for LT and GT

---
 src/Backend/constraint.c       | 14 +++++++++++++-
 src/Backend/constraint.h       |  3 ++-
 src/Backend/satfuncopencoder.c | 29 +++++++++++------------------
 src/Backend/satfuncopencoder.h |  1 -
 4 files changed, 26 insertions(+), 21 deletions(-)

diff --git a/src/Backend/constraint.c b/src/Backend/constraint.c
index 62c3c81..3e0d0a8 100644
--- 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 b248817..772f6c8 100644
--- 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 b8a814d..8dd7532 100644
--- 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 8b39194..a9d0663 100644
--- 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
-- 
2.34.1