X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FBackend%2Fsatencoder.cc;h=1d6b4f4e7dc91c65d1643e92e62333ffba08125d;hp=a7513d6120eb9180c8b33f127742b4f625e21597;hb=d46ee65a6767e2016cab629220a60c3e39b366f1;hpb=c25ce5e80da20bb0eac14f371900bbf79bebb9b2

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index a7513d6..1d6b4f4 100644
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -11,12 +11,8 @@
 #include "order.h"
 #include "predicate.h"
 #include "set.h"
-#include "satfuncopencoder.h"
 
-//TODO: Should handle sharing of AST Nodes without recoding them a second time
-
-SATEncoder::SATEncoder(CSolver * _solver) :
-	varcount(1),
+SATEncoder::SATEncoder(CSolver *_solver) :
 	cnf(createCNF()),
 	solver(_solver) {
 }
@@ -25,90 +21,105 @@ SATEncoder::~SATEncoder() {
 	deleteCNF(cnf);
 }
 
+int SATEncoder::solve() {
+	return solveCNF(cnf);
+}
+
 void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
-	HSIteratorBoolean *iterator = csolver->getConstraints();
+	SetIteratorBoolean *iterator = csolver->getConstraints();
 	while (iterator->hasNext()) {
 		Boolean *constraint = iterator->next();
-		model_print("Encoding All ...\n\n");
 		Edge c = encodeConstraintSATEncoder(constraint);
-		model_print("Returned Constraint in EncodingAll:\n");
-		ASSERT( !equalsEdge(c, E_BOGUS));
 		addConstraintCNF(cnf, c);
 	}
 	delete iterator;
 }
 
 Edge SATEncoder::encodeConstraintSATEncoder(Boolean *constraint) {
-	switch (GETBOOLEANTYPE(constraint)) {
+	Edge result;
+	if (booledgeMap.contains(constraint)) {
+		Edge e = {(Node *) booledgeMap.get(constraint)};
+		return e;
+	}
+
+	switch (constraint->type) {
 	case ORDERCONST:
-		return encodeOrderSATEncoder(this, (BooleanOrder *) constraint);
+		result = encodeOrderSATEncoder((BooleanOrder *) constraint);
+		break;
 	case BOOLEANVAR:
-		return encodeVarSATEncoder(this, (BooleanVar *) constraint);
+		result = encodeVarSATEncoder((BooleanVar *) constraint);
+		break;
 	case LOGICOP:
-		return encodeLogicSATEncoder(this, (BooleanLogic *) constraint);
+		result = encodeLogicSATEncoder((BooleanLogic *) constraint);
+		break;
 	case PREDICATEOP:
-		return encodePredicateSATEncoder(this, (BooleanPredicate *) constraint);
+		result = encodePredicateSATEncoder((BooleanPredicate *) constraint);
+		break;
 	default:
-		model_print("Unhandled case in encodeConstraintSATEncoder %u", GETBOOLEANTYPE(constraint));
+		model_print("Unhandled case in encodeConstraintSATEncoder %u", constraint->type);
 		exit(-1);
 	}
+	booledgeMap.put(constraint, result.node_ptr);
+	return result;
 }
 
-void getArrayNewVarsSATEncoder(SATEncoder *encoder, uint num, Edge *carray) {
+void SATEncoder::getArrayNewVarsSATEncoder(uint num, Edge *carray) {
 	for (uint i = 0; i < num; i++)
-		carray[i] = getNewVarSATEncoder(encoder);
+		carray[i] = getNewVarSATEncoder();
 }
 
-Edge getNewVarSATEncoder(SATEncoder *This) {
-	return constraintNewVar(This->cnf);
+Edge SATEncoder::getNewVarSATEncoder() {
+	return constraintNewVar(cnf);
 }
 
-Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar *constraint) {
+Edge SATEncoder::encodeVarSATEncoder(BooleanVar *constraint) {
 	if (edgeIsNull(constraint->var)) {
-		constraint->var = getNewVarSATEncoder(This);
+		constraint->var = getNewVarSATEncoder();
 	}
 	return constraint->var;
 }
 
-Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic *constraint) {
+Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
 	Edge array[constraint->inputs.getSize()];
 	for (uint i = 0; i < constraint->inputs.getSize(); i++)
-		array[i] = This->encodeConstraintSATEncoder(constraint->inputs.get(i));
+		array[i] = encodeConstraintSATEncoder(constraint->inputs.get(i));
 
 	switch (constraint->op) {
-	case L_AND:
-		return constraintAND(This->cnf, constraint->inputs.getSize(), array);
-	case L_OR:
-		return constraintOR(This->cnf, constraint->inputs.getSize(), array);
-	case L_NOT:
+	case SATC_AND:
+		return constraintAND(cnf, constraint->inputs.getSize(), array);
+	case SATC_OR:
+		return constraintOR(cnf, constraint->inputs.getSize(), array);
+	case SATC_NOT:
 		return constraintNegate(array[0]);
-	case L_XOR:
-		return constraintXOR(This->cnf, array[0], array[1]);
-	case L_IMPLIES:
-		return constraintIMPLIES(This->cnf, array[0], array[1]);
+	case SATC_XOR:
+		return constraintXOR(cnf, array[0], array[1]);
+	case SATC_IFF:
+		return constraintIFF(cnf, array[0], array[1]);
+	case SATC_IMPLIES:
+		return constraintIMPLIES(cnf, array[0], array[1]);
 	default:
 		model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
 		exit(-1);
 	}
 }
 
-Edge encodePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
-	switch (GETPREDICATETYPE(constraint->predicate) ) {
+Edge SATEncoder::encodePredicateSATEncoder(BooleanPredicate *constraint) {
+	switch (constraint->predicate->type) {
 	case TABLEPRED:
-		return encodeTablePredicateSATEncoder(This, constraint);
+		return encodeTablePredicateSATEncoder(constraint);
 	case OPERATORPRED:
-		return encodeOperatorPredicateSATEncoder(This, constraint);
+		return encodeOperatorPredicateSATEncoder(constraint);
 	default:
 		ASSERT(0);
 	}
 	return E_BOGUS;
 }
 
-Edge encodeTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+Edge SATEncoder::encodeTablePredicateSATEncoder(BooleanPredicate *constraint) {
 	switch (constraint->encoding.type) {
 	case ENUMERATEIMPLICATIONS:
 	case ENUMERATEIMPLICATIONSNEGATE:
-		return encodeEnumTablePredicateSATEncoder(This, constraint);
+		return encodeEnumTablePredicateSATEncoder(constraint);
 	case CIRCUIT:
 		ASSERT(0);
 		break;
@@ -118,14 +129,19 @@ Edge encodeTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constrai
 	return E_BOGUS;
 }
 
-void encodeElementSATEncoder(SATEncoder *encoder, Element *This) {
-	switch ( GETELEMENTTYPE(This) ) {
+void SATEncoder::encodeElementSATEncoder(Element *element) {
+	/* Check to see if we have already encoded this element. */
+	if (getElementEncoding(element)->variables != NULL)
+		return;
+
+	/* Need to encode. */
+	switch ( element->type) {
 	case ELEMFUNCRETURN:
-		generateElementEncoding(encoder, This);
-		encodeElementFunctionSATEncoder(encoder, (ElementFunction *) This);
+		generateElementEncoding(element);
+		encodeElementFunctionSATEncoder((ElementFunction *) element);
 		break;
 	case ELEMSET:
-		generateElementEncoding(encoder, This);
+		generateElementEncoding(element);
 		return;
 	case ELEMCONST:
 		return;
@@ -134,23 +150,23 @@ void encodeElementSATEncoder(SATEncoder *encoder, Element *This) {
 	}
 }
 
-void encodeElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This) {
-	switch (GETFUNCTIONTYPE(This->function)) {
+void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
+	switch (function->function->type) {
 	case TABLEFUNC:
-		encodeTableElementFunctionSATEncoder(encoder, This);
+		encodeTableElementFunctionSATEncoder(function);
 		break;
 	case OPERATORFUNC:
-		encodeOperatorElementFunctionSATEncoder(encoder, This);
+		encodeOperatorElementFunctionSATEncoder(function);
 		break;
 	default:
 		ASSERT(0);
 	}
 }
 
-void encodeTableElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This) {
-	switch (getElementFunctionEncoding(This)->type) {
+void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {
+	switch (getElementFunctionEncoding(function)->type) {
 	case ENUMERATEIMPLICATIONS:
-		encodeEnumTableElemFunctionSATEncoder(encoder, This);
+		encodeEnumTableElemFunctionSATEncoder(function);
 		break;
 	case CIRCUIT:
 		ASSERT(0);