X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FBackend%2Fsatfuncopencoder.cc;h=f4eda5240d69c401d2a47ec0cd0474199103c837;hp=d416a15a48113f6c3cc7b5d95ed5ed224b77de01;hb=f60d35f0d239c6423cbe443a0b86ab5b335173e5;hpb=852184b398d1e4c1e70b3d997bd18ba2b96490a5

diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc
index d416a15..f4eda52 100644
--- a/src/Backend/satfuncopencoder.cc
+++ b/src/Backend/satfuncopencoder.cc
@@ -34,7 +34,7 @@ Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constra
 		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);
@@ -75,11 +75,11 @@ Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constra
 		}
 	}
 	if (getSizeVectorEdge(clauses) == 0) {
-		deleteVectorEdge(clauses);
+		clearVectorEdge(clauses);
 		return E_False;
 	}
 	Edge cor = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
-	deleteVectorEdge(clauses);
+	clearVectorEdge(clauses);
 	return generateNegation ? constraintNegate(cor) : cor;
 }
 
@@ -88,7 +88,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,20 +104,20 @@ 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;
+	Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
 
 	bool notfinished = true;
 	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 == OVERFLOWSETSFLAG || function->overflowbehavior == FLAGIFFOVERFLOW) {
+		if (function->overflowbehavior == SATC_OVERFLOWSETSFLAG || function->overflowbehavior == SATC_FLAGIFFOVERFLOW) {
 			needClause = true;
 		}
 
@@ -133,17 +133,17 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
 
 			Edge clause;
 			switch (function->overflowbehavior) {
-			case IGNORE:
-			case NOOVERFLOW:
-			case WRAPAROUND: {
+			case SATC_IGNORE:
+			case SATC_NOOVERFLOW:
+			case SATC_WRAPAROUND: {
 				clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
 				break;
 			}
-			case FLAGFORCESOVERFLOW: {
+			case SATC_FLAGFORCESOVERFLOW: {
 				clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
 				break;
 			}
-			case OVERFLOWSETSFLAG: {
+			case SATC_OVERFLOWSETSFLAG: {
 				if (isInRange) {
 					clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
 				} else {
@@ -151,7 +151,7 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
 				}
 				break;
 			}
-			case FLAGIFFOVERFLOW: {
+			case SATC_FLAGIFFOVERFLOW: {
 				if (isInRange) {
 					clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
 				} else {
@@ -173,7 +173,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);
@@ -200,16 +200,16 @@ 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) {
-	case EQUALS:
+	switch (predicate->getOp()) {
+	case SATC_EQUALS:
 		return generateEquivNVConstraint(cnf, numVars, ee0->variables, ee1->variables);
-	case LT:
+	case SATC_LT:
 		return generateLTConstraint(cnf, numVars, ee0->variables, ee1->variables);
-	case GT:
+	case SATC_GT:
 		return generateLTConstraint(cnf, numVars, ee1->variables, ee0->variables);
 	default:
 		ASSERT(0);