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

diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc
index d416a15..7372c95 100644
--- a/src/Backend/satfuncopencoder.cc
+++ b/src/Backend/satfuncopencoder.cc
@@ -22,47 +22,195 @@ Edge SATEncoder::encodeOperatorPredicateSATEncoder(BooleanPredicate *constraint)
 	exit(-1);
 }
 
-Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constraint) {
+Edge SATEncoder::encodeEnumEqualsPredicateSATEncoder(BooleanPredicate *constraint) {
+	Polarity polarity = constraint->polarity;
+
+	/* Call base encoders for children */
+	for (uint i = 0; i < 2; i++) {
+		Element *elem = constraint->inputs.get(i);
+		encodeElementSATEncoder(elem);
+	}
+	VectorEdge *clauses = vector;
+
+	Set *set0 = constraint->inputs.get(0)->getRange();
+	uint size0 = set0->getSize();
+
+	Set *set1 = constraint->inputs.get(1)->getRange();
+	uint size1 = set1->getSize();
+
+	uint64_t val0 = set0->getElement(0);
+	uint64_t val1 = set1->getElement(0);
+	if (size0 != 0 && size1 != 0)
+		for (uint i = 0, j = 0; true; ) {
+			if (val0 == val1) {
+				Edge carray[2];
+				carray[0] = getElementValueConstraint(constraint->inputs.get(0), polarity, val0);
+				carray[1] = getElementValueConstraint(constraint->inputs.get(1), polarity, val0);
+				Edge term = constraintAND(cnf, 2, carray);
+				pushVectorEdge(clauses, term);
+				i++; j++;
+				if (i < size0)
+					val0 = set0->getElement(i);
+				else
+					break;
+				if (j < size1)
+					val1 = set1->getElement(j);
+				else
+					break;
+			} else if (val0 < val1) {
+				i++;
+				if (i < size0)
+					val0 = set0->getElement(i);
+				else
+					break;
+			} else {
+				j++;
+				if (j < size1)
+					val1 = set1->getElement(j);
+				else
+					break;
+			}
+		}
+	if (getSizeVectorEdge(clauses) == 0) {
+		return E_False;
+	}
+	Edge cor = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+	clearVectorEdge(clauses);
+	return cor;
+}
+
+Edge SATEncoder::encodeUnaryPredicateSATEncoder(BooleanPredicate *constraint) {
+	Polarity polarity = constraint->polarity;
 	PredicateOperator *predicate = (PredicateOperator *)constraint->predicate;
-	uint numDomains = predicate->domains.getSize();
+	CompOp op = predicate->getOp();
+
+	/* Call base encoders for children */
+	for (uint i = 0; i < 2; i++) {
+		Element *elem = constraint->inputs.get(i);
+		encodeElementSATEncoder(elem);
+	}
+	VectorEdge *clauses = vector;
+
+	Element *elem0 = constraint->inputs.get(0);
+	Element *elem1 = constraint->inputs.get(1);
 
+	//Eliminate symmetric cases
+	if (op == SATC_GT) {
+		op = SATC_LT;
+		Element *tmp = elem0;
+		elem0 = elem1;
+		elem1 = elem0;
+	} else if (op == SATC_GTE) {
+		op = SATC_LTE;
+		Element *tmp = elem0;
+		elem0 = elem1;
+		elem1 = elem0;
+	}
+
+	Set *set0 = elem0->getRange();
+	uint size0 = set0->getSize();
+	Edge *vars0 = elem0->getElementEncoding()->variables;
+
+	Set *set1 = elem1->getRange();
+	uint size1 = set1->getSize();
+	Edge *vars1 = elem1->getElementEncoding()->variables;
+
+
+	uint64_t val0 = set0->getElement(0);
+	uint64_t val1 = set1->getElement(0);
+	if (size0 != 0 && size1 != 0) {
+		for (uint i = 0, j = 0; true; ) {
+			if (val0 > val1 || (op == SATC_LT && val0 == val1)) {
+				j++;
+				if (j == size1) {
+					//need to assert val0 isn't this big
+					if (i == 0)
+						return E_False;//Can't satisfy this constraint
+					pushVectorEdge(clauses, constraintNegate(vars0[i - 1]));
+					break;
+				}
+				val1 = set1->getElement(j);
+			} else {
+				if (i == 0) {
+					if (j != 0) {
+						pushVectorEdge(clauses, vars1[j - 1]);
+					}
+				} else {
+					if (j != 0) {
+						Edge term = constraintIMPLIES(cnf, vars0[i - 1], vars1[j - 1]);
+						pushVectorEdge(clauses, term);
+					}
+				}
+				i++;
+				if (i == size0)
+					break;
+				val0 = set0->getElement(i);
+			}
+		}
+	}
+	//Trivially true constraint
+	if (getSizeVectorEdge(clauses) == 0)
+		return E_True;
+
+	Edge cand = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+	clearVectorEdge(clauses);
+	return cand;
+}
+
+Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constraint) {
+	PredicateOperator *predicate = (PredicateOperator *)constraint->predicate;
+	uint numDomains = constraint->inputs.getSize();
+	Polarity polarity = constraint->polarity;
 	FunctionEncodingType encType = constraint->encoding.type;
 	bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
+	if (generateNegation)
+		polarity = negatePolarity(polarity);
+
+	CompOp op = predicate->getOp();
+	if (!generateNegation && op == SATC_EQUALS)
+		return encodeEnumEqualsPredicateSATEncoder(constraint);
+
+	if (!generateNegation && numDomains == 2 &&
+			(op == SATC_LT || op == SATC_GT || op == SATC_LTE || op == SATC_GTE) &&
+			constraint->inputs.get(0)->encoding.type == UNARY &&
+			constraint->inputs.get(1)->encoding.type == UNARY) {
+		return encodeUnaryPredicateSATEncoder(constraint);
+	}
 
 	/* 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);
 
 	uint64_t vals[numDomains];//setup value array
 	for (uint i = 0; i < numDomains; i++) {
-		Set *set = predicate->domains.get(i);
+		Set *set = constraint->inputs.get(i)->getRange();
 		vals[i] = set->getElement(indices[i]);
 	}
 
 	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;
 		for (uint i = 0; i < numDomains; i++) {
 			uint index = ++indices[i];
-			Set *set = predicate->domains.get(i);
+			Set *set = constraint->inputs.get(i)->getRange();
 
 			if (index < set->getSize()) {
 				vals[i] = set->getElement(index);
@@ -75,11 +223,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 +235,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 +251,17 @@ 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 == OVERFLOWSETSFLAG || function->overflowbehavior == FLAGIFFOVERFLOW) {
+		if (function->overflowbehavior == SATC_OVERFLOWSETSFLAG || function->overflowbehavior == SATC_FLAGIFFOVERFLOW) {
 			needClause = true;
 		}
 
@@ -125,33 +269,36 @@ 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;
 			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: {
+				Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
 				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 {
+					Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
 					clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), overFlowConstraint);
 				}
 				break;
 			}
-			case FLAGIFFOVERFLOW: {
+			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 +320,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 +336,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,16 +347,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);