X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FBackend%2Fsatfuncopencoder.cc;h=3f85fec3700ac5a7e7905f1f627f7f183b320931;hb=77f32c79afdf12f29c040d511cd84f15d703ceb9;hp=8e66c9b16b06ab040abd616f04865c6506f1da25;hpb=71b1f3df40acb5b54bbb06c2c55c97af1a62521b;p=satune.git

diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc
index 8e66c9b..3f85fec 100644
--- a/src/Backend/satfuncopencoder.cc
+++ b/src/Backend/satfuncopencoder.cc
@@ -9,31 +9,30 @@
 #include "set.h"
 #include "element.h"
 #include "common.h"
-#include "satfuncopencoder.h"
 
-Edge encodeOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+Edge SATEncoder::encodeOperatorPredicateSATEncoder(BooleanPredicate *constraint) {
 	switch (constraint->encoding.type) {
 	case ENUMERATEIMPLICATIONS:
-		return encodeEnumOperatorPredicateSATEncoder(This, constraint);
+		return encodeEnumOperatorPredicateSATEncoder(constraint);
 	case CIRCUIT:
-		return encodeCircuitOperatorPredicateEncoder(This, constraint);
+		return encodeCircuitOperatorPredicateEncoder(constraint);
 	default:
 		ASSERT(0);
 	}
 	exit(-1);
 }
 
-Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constraint) {
 	PredicateOperator *predicate = (PredicateOperator *)constraint->predicate;
-	uint numDomains = getSizeArraySet(&predicate->domains);
+	uint numDomains = predicate->domains.getSize();
 
 	FunctionEncodingType encType = constraint->encoding.type;
 	bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
 
 	/* Call base encoders for children */
 	for (uint i = 0; i < numDomains; i++) {
-		Element *elem = getArrayElement( &constraint->inputs, i);
-		encodeElementSATEncoder(This, elem);
+		Element *elem = constraint->inputs.get(i);
+		encodeElementSATEncoder(elem);
 	}
 	VectorEdge *clauses = allocDefVectorEdge();	// Setup array of clauses
 
@@ -42,36 +41,36 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *c
 
 	uint64_t vals[numDomains];//setup value array
 	for (uint i = 0; i < numDomains; i++) {
-		Set *set = getArraySet(&predicate->domains, i);
-		vals[i] = getSetElement(set, indices[i]);
+		Set *set = predicate->domains.get(i);
+		vals[i] = set->getElement(indices[i]);
 	}
 
 	bool notfinished = true;
 	while (notfinished) {
 		Edge carray[numDomains];
 
-		if (evalPredicateOperator(predicate, vals) ^ generateNegation) {
+		if (predicate->evalPredicateOperator(vals) != generateNegation) {
 			//Include this in the set of terms
 			for (uint i = 0; i < numDomains; i++) {
-				Element *elem = getArrayElement(&constraint->inputs, i);
-				carray[i] = getElementValueConstraint(This, elem, vals[i]);
+				Element *elem = constraint->inputs.get(i);
+				carray[i] = getElementValueConstraint(elem, vals[i]);
 			}
-			Edge term = constraintAND(This->cnf, numDomains, carray);
+			Edge term = constraintAND(cnf, numDomains, carray);
 			pushVectorEdge(clauses, term);
 		}
 
 		notfinished = false;
 		for (uint i = 0; i < numDomains; i++) {
 			uint index = ++indices[i];
-			Set *set = getArraySet(&predicate->domains, i);
+			Set *set = predicate->domains.get(i);
 
-			if (index < getSetSize(set)) {
-				vals[i] = getSetElement(set, index);
+			if (index < set->getSize()) {
+				vals[i] = set->getElement(index);
 				notfinished = true;
 				break;
 			} else {
 				indices[i] = 0;
-				vals[i] = getSetElement(set, 0);
+				vals[i] = set->getElement(0);
 			}
 		}
 	}
@@ -79,23 +78,23 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *c
 		deleteVectorEdge(clauses);
 		return E_False;
 	}
-	Edge cor = constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+	Edge cor = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
 	deleteVectorEdge(clauses);
 	return generateNegation ? constraintNegate(cor) : cor;
 }
 
 
-void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction *func) {
+void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func) {
 #ifdef TRACE_DEBUG
 	model_print("Operator Function ...\n");
 #endif
-	FunctionOperator *function = (FunctionOperator *) func->function;
-	uint numDomains = getSizeArrayElement(&func->inputs);
+	FunctionOperator *function = (FunctionOperator *) func->getFunction();
+	uint numDomains = func->inputs.getSize();
 
 	/* Call base encoders for children */
 	for (uint i = 0; i < numDomains; i++) {
-		Element *elem = getArrayElement( &func->inputs, i);
-		encodeElementSATEncoder(This, elem);
+		Element *elem = func->inputs.get(i);
+		encodeElementSATEncoder(elem);
 	}
 
 	VectorEdge *clauses = allocDefVectorEdge();	// Setup array of clauses
@@ -105,58 +104,58 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction *
 
 	uint64_t vals[numDomains];//setup value array
 	for (uint i = 0; i < numDomains; i++) {
-		Set *set = getElementSet(getArrayElement(&func->inputs, i));
-		vals[i] = getSetElement(set, indices[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 = applyFunctionOperator(function, numDomains, vals);
-		bool isInRange = isInRangeFunction((FunctionOperator *)func->function, result);
+		uint64_t result = function->applyFunctionOperator(numDomains, vals);
+		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;
 		}
 
 		if (needClause) {
 			//Include this in the set of terms
 			for (uint i = 0; i < numDomains; i++) {
-				Element *elem = getArrayElement(&func->inputs, i);
-				carray[i] = getElementValueConstraint(This, elem, vals[i]);
+				Element *elem = func->inputs.get(i);
+				carray[i] = getElementValueConstraint(elem, vals[i]);
 			}
 			if (isInRange) {
-				carray[numDomains] = getElementValueConstraint(This, func, result);
+				carray[numDomains] = getElementValueConstraint(func, result);
 			}
 
 			Edge clause;
 			switch (function->overflowbehavior) {
-			case IGNORE:
-			case NOOVERFLOW:
-			case WRAPAROUND: {
-				clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
+			case SATC_IGNORE:
+			case SATC_NOOVERFLOW:
+			case SATC_WRAPAROUND: {
+				clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
 				break;
 			}
-			case FLAGFORCESOVERFLOW: {
-				clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
+			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(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
+					clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
 				} else {
-					clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
+					clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), overFlowConstraint);
 				}
 				break;
 			}
-			case FLAGIFFOVERFLOW: {
+			case SATC_FLAGIFFOVERFLOW: {
 				if (isInRange) {
-					clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
+					clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
 				} else {
-					clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
+					clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), overFlowConstraint);
 				}
 				break;
 			}
@@ -174,15 +173,15 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction *
 		notfinished = false;
 		for (uint i = 0; i < numDomains; i++) {
 			uint index = ++indices[i];
-			Set *set = getElementSet(getArrayElement(&func->inputs, i));
+			Set *set = func->inputs.get(i)->getRange();
 
-			if (index < getSetSize(set)) {
-				vals[i] = getSetElement(set, index);
+			if (index < set->getSize()) {
+				vals[i] = set->getElement(index);
 				notfinished = true;
 				break;
 			} else {
 				indices[i] = 0;
-				vals[i] = getSetElement(set, 0);
+				vals[i] = set->getElement(0);
 			}
 		}
 	}
@@ -190,31 +189,30 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction *
 		deleteVectorEdge(clauses);
 		return;
 	}
-	Edge cor = constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
-	addConstraintCNF(This->cnf, cor);
+	Edge cor = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+	addConstraintCNF(cnf, cor);
 	deleteVectorEdge(clauses);
 }
 
-Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+Edge SATEncoder::encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constraint) {
 	PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
-	ASSERT(getSizeArraySet(&predicate->domains) == 2);
-	Element *elem0 = getArrayElement( &constraint->inputs, 0);
-	encodeElementSATEncoder(This, elem0);
-	Element *elem1 = getArrayElement( &constraint->inputs, 1);
-	encodeElementSATEncoder(This, elem1);
-	ElementEncoding *ee0 = getElementEncoding(elem0);
-	ElementEncoding *ee1 = getElementEncoding(elem1);
+	Element *elem0 = constraint->inputs.get(0);
+	encodeElementSATEncoder(elem0);
+	Element *elem1 = constraint->inputs.get(1);
+	encodeElementSATEncoder(elem1);
+	ElementEncoding *ee0 = elem0->getElementEncoding();
+	ElementEncoding *ee1 = elem1->getElementEncoding();
 	ASSERT(ee0->numVars == ee1->numVars);
 	uint numVars = ee0->numVars;
-	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);
+	switch (predicate->getOp()) {
+	case SATC_EQUALS:
+		return generateEquivNVConstraint(cnf, numVars, ee0->variables, ee1->variables);
+	case SATC_LT:
+		return generateLTConstraint(cnf, numVars, ee0->variables, ee1->variables);
+	case SATC_GT:
+		return generateLTConstraint(cnf, numVars, ee1->variables, ee0->variables);
+	default:
+		ASSERT(0);
 	}
 	exit(-1);
 }