X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FBackend%2Fsatfuncopencoder.cc;h=79b13033ebdc40f4ffd82963ac83885d936f3cdc;hp=7e6a67d239def78348bb3d4443b1a683735e4354;hb=f9f7d7f9830b7ca2b85c56bdeaff4ceae29f2128;hpb=cb887a9e8e6cc23c2e09638a1f7bceed4ce1868a

diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc
index 7e6a67d..79b1303 100644
--- a/src/Backend/satfuncopencoder.cc
+++ b/src/Backend/satfuncopencoder.cc
@@ -25,16 +25,18 @@ Edge SATEncoder::encodeOperatorPredicateSATEncoder(BooleanPredicate *constraint)
 Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constraint) {
 	PredicateOperator *predicate = (PredicateOperator *)constraint->predicate;
 	uint numDomains = predicate->domains.getSize();
-
+	Polarity polarity = constraint->polarity;
 	FunctionEncodingType encType = constraint->encoding.type;
 	bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
+	if (generateNegation)
+		polarity = negatePolarity(polarity);
 
 	/* Call base encoders for children */
 	for (uint i = 0; i < numDomains; i++) {
 		Element *elem = constraint->inputs.get(i);
 		encodeElementSATEncoder(elem);
 	}
-	VectorEdge *clauses = allocDefVectorEdge();	// Setup array of clauses
+	VectorEdge *clauses = vector;
 
 	uint indices[numDomains];	//setup indices
 	bzero(indices, sizeof(uint) * numDomains);
@@ -46,17 +48,17 @@ Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constra
 	}
 
 	bool notfinished = true;
+        Edge carray[numDomains];
 	while (notfinished) {
-		Edge carray[numDomains];
-
 		if (predicate->evalPredicateOperator(vals) != generateNegation) {
 			//Include this in the set of terms
 			for (uint i = 0; i < numDomains; i++) {
 				Element *elem = constraint->inputs.get(i);
-				carray[i] = getElementValueConstraint(elem, vals[i]);
+				carray[i] = getElementValueConstraint(elem, polarity, vals[i]);
 			}
 			Edge term = constraintAND(cnf, numDomains, carray);
 			pushVectorEdge(clauses, term);
+			ASSERT(getSizeVectorEdge(clauses) > 0);
 		}
 
 		notfinished = false;
@@ -75,11 +77,10 @@ Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constra
 		}
 	}
 	if (getSizeVectorEdge(clauses) == 0) {
-		deleteVectorEdge(clauses);
 		return E_False;
 	}
 	Edge cor = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
-	deleteVectorEdge(clauses);
+	clearVectorEdge(clauses);
 	return generateNegation ? constraintNegate(cor) : cor;
 }
 
@@ -108,12 +109,9 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
 		vals[i] = set->getElement(indices[i]);
 	}
 
-	Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
-
 	bool notfinished = true;
+        Edge carray[numDomains + 1];
 	while (notfinished) {
-		Edge carray[numDomains + 1];
-
 		uint64_t result = function->applyFunctionOperator(numDomains, vals);
 		bool isInRange = ((FunctionOperator *)func->getFunction())->isInRangeFunction(result);
 		bool needClause = isInRange;
@@ -125,10 +123,10 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
 			//Include this in the set of terms
 			for (uint i = 0; i < numDomains; i++) {
 				Element *elem = func->inputs.get(i);
-				carray[i] = getElementValueConstraint(elem, vals[i]);
+				carray[i] = getElementValueConstraint(elem, P_FALSE, vals[i]);
 			}
 			if (isInRange) {
-				carray[numDomains] = getElementValueConstraint(func, result);
+				carray[numDomains] = getElementValueConstraint(func, P_TRUE, result);
 			}
 
 			Edge clause;
@@ -140,6 +138,7 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
 				break;
 			}
 			case SATC_FLAGFORCESOVERFLOW: {
+				Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
 				clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
 				break;
 			}
@@ -147,11 +146,13 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
 				if (isInRange) {
 					clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
 				} else {
+					Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
 					clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), overFlowConstraint);
 				}
 				break;
 			}
 			case SATC_FLAGIFFOVERFLOW: {
+				Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
 				if (isInRange) {
 					clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
 				} else {
@@ -200,11 +201,11 @@ Edge SATEncoder::encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constra
 	encodeElementSATEncoder(elem0);
 	Element *elem1 = constraint->inputs.get(1);
 	encodeElementSATEncoder(elem1);
-	ElementEncoding *ee0 = getElementEncoding(elem0);
-	ElementEncoding *ee1 = getElementEncoding(elem1);
+	ElementEncoding *ee0 = elem0->getElementEncoding();
+	ElementEncoding *ee1 = elem1->getElementEncoding();
 	ASSERT(ee0->numVars == ee1->numVars);
 	uint numVars = ee0->numVars;
-	switch (predicate->op) {
+	switch (predicate->getOp()) {
 	case SATC_EQUALS:
 		return generateEquivNVConstraint(cnf, numVars, ee0->variables, ee1->variables);
 	case SATC_LT: