From: Hamed <hamed.gorjiara@gmail.com>
Date: Tue, 11 Jul 2017 20:19:37 +0000 (-0700)
Subject: Fixing bugs + renaming ...
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=2b9b871ad30b632b8abfd31e5014d373f742317d;p=satune.git

Fixing bugs + renaming ...
---

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 4b7d447..d51e251 100644
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -356,8 +356,7 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate *
 void encodeElementSATEncoder(SATEncoder* encoder, Element *This){
 	switch( GETELEMENTTYPE(This) ){
 		case ELEMFUNCRETURN:
-			Edge c = encodeFunctionElementSATEncoder(This, (ElementFunction*) This);
-			addConstraint(encoder->cnf, c);
+			addConstraintCNF(encoder->cnf, encodeElementFunctionSATEncoder(encoder, (ElementFunction*) This));
 			break;
 		case ELEMSET:
 			return;
@@ -366,7 +365,7 @@ void encodeElementSATEncoder(SATEncoder* encoder, Element *This){
 	}
 }
 
-Edge encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){
+Edge encodeElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction *This){
 	switch(GETFUNCTIONTYPE(This->function)){
 		case TABLEFUNC:
 			return encodeTableElementFunctionSATEncoder(encoder, This);
@@ -465,12 +464,7 @@ Edge encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunctio
 			}
 		}
 	}
-	Edge result = constraintAND(encoder->cnf, size, carray); 
-	if (!edgeIsNull(elemc1))
-		result = constraintAND2(encoder->cnf, result, elemc1);
-	if (!edgeIsNull(elemc2))
-		result = constraintAND2(encoder->cnf, result, elemc2);
-	return result;
+	return constraintAND(encoder->cnf, size, carray); 
 }
 
 Edge encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 22b1b2e..dfcb886 100644
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -34,8 +34,8 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate *
 Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* element, uint64_t value);
 Edge getElementValueConstraint(SATEncoder* encoder, Element* This, uint64_t value);
 
-Edge encodeElementSATEncoder(SATEncoder* encoder, Element *This);
-Edge encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This);
+void encodeElementSATEncoder(SATEncoder* encoder, Element *This);
+Edge encodeElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction *This);
 Edge encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
 Edge encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
 Edge encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder,ElementFunction* This);