X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FBackend%2Fsatfuncopencoder.cc;h=1fea1a58f41ebf23391bba824a6744bc84662ae8;hp=41b687ec17aa2d6cac9d10511c91ea33c9af52c9;hb=c0c4f17e45f0e5b7881a9f041a4cd5e09f3276ba;hpb=bb49b371775e60638e71a99febce2bc4a21e075e

diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc
index 41b687e..1fea1a5 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;
 }
 
@@ -88,7 +89,7 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
 #ifdef TRACE_DEBUG
 	model_print("Operator Function ...\n");
 #endif
-	FunctionOperator *function = (FunctionOperator *) func->function;
+	FunctionOperator *function = (FunctionOperator *) func->getFunction();
 	uint numDomains = func->inputs.getSize();
 
 	/* Call base encoders for children */
@@ -104,18 +105,15 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
 
 	uint64_t vals[numDomains];//setup value array
 	for (uint i = 0; i < numDomains; i++) {
-		Set *set = getElementSet(func->inputs.get(i));
+		Set *set = func->inputs.get(i)->getRange();
 		vals[i] = set->getElement(indices[i]);
 	}
 
-	Edge overFlowConstraint = ((BooleanVar *) func->overflowstatus)->var;
-
 	bool notfinished = true;
+        Edge carray[numDomains + 1];
 	while (notfinished) {
-		Edge carray[numDomains + 1];
-
 		uint64_t result = function->applyFunctionOperator(numDomains, vals);
-		bool isInRange = ((FunctionOperator *)func->function)->isInRangeFunction(result);
+		bool isInRange = ((FunctionOperator *)func->getFunction())->isInRangeFunction(result);
 		bool needClause = isInRange;
 		if (function->overflowbehavior == SATC_OVERFLOWSETSFLAG || function->overflowbehavior == SATC_FLAGIFFOVERFLOW) {
 			needClause = true;
@@ -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 {
@@ -173,7 +174,7 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
 		notfinished = false;
 		for (uint i = 0; i < numDomains; i++) {
 			uint index = ++indices[i];
-			Set *set = getElementSet(func->inputs.get(i));
+			Set *set = func->inputs.get(i)->getRange();
 
 			if (index < set->getSize()) {
 				vals[i] = set->getElement(index);
@@ -189,8 +190,8 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
 		deleteVectorEdge(clauses);
 		return;
 	}
-	Edge cor = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
-	addConstraintCNF(cnf, cor);
+	Edge cand = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+	addConstraintCNF(cnf, cand);
 	deleteVectorEdge(clauses);
 }
 
@@ -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: