X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FEncoders%2Fnaiveencoder.cc;h=17b9914c80bfe9ccbfe1e004d9089689300dd331;hb=31d8e919360f167a7a3317d7e9482e3bd9f70b8e;hp=ef677adf77671389a279bc736537f195a83cd36e;hpb=b03787cd7584eea5b44ae5303576295e52b01289;p=satune.git

diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc
index ef677ad..17b9914 100644
--- a/src/Encoders/naiveencoder.cc
+++ b/src/Encoders/naiveencoder.cc
@@ -11,32 +11,34 @@
 #include "table.h"
 #include "tableentry.h"
 #include "order.h"
+#include "tunable.h"
 #include <strings.h>
 
 void naiveEncodingDecision(CSolver *This) {
-	HSIteratorBoolean *iterator = This->getConstraints();
+	SetIteratorBooleanEdge *iterator = This->getConstraints();
 	while (iterator->hasNext()) {
-		Boolean *boolean = iterator->next();
-		naiveEncodingConstraint(boolean);
+		BooleanEdge b = iterator->next();
+		naiveEncodingConstraint(This, b.getBoolean());
 	}
 	delete iterator;
 }
 
-void naiveEncodingConstraint(Boolean *This) {
+void naiveEncodingConstraint(CSolver *csolver, Boolean *This) {
 	switch (This->type) {
 	case BOOLEANVAR: {
 		return;
 	}
 	case ORDERCONST: {
-		((BooleanOrder *) This)->order->setOrderEncodingType(PAIRWISE);
+		if (((BooleanOrder *) This)->order->encoding.type == ORDER_UNASSIGNED)
+			((BooleanOrder *) This)->order->setOrderEncodingType(PAIRWISE);
 		return;
 	}
 	case LOGICOP: {
-		naiveEncodingLogicOp((BooleanLogic *) This);
+		naiveEncodingLogicOp(csolver, (BooleanLogic *) This);
 		return;
 	}
 	case PREDICATEOP: {
-		naiveEncodingPredicate((BooleanPredicate *) This);
+		naiveEncodingPredicate(csolver, (BooleanPredicate *) This);
 		return;
 	}
 	default:
@@ -44,27 +46,30 @@ void naiveEncodingConstraint(Boolean *This) {
 	}
 }
 
-void naiveEncodingLogicOp(BooleanLogic *This) {
+void naiveEncodingLogicOp(CSolver *csolver, BooleanLogic *This) {
 	for (uint i = 0; i < This->inputs.getSize(); i++) {
-		naiveEncodingConstraint(This->inputs.get(i));
+		naiveEncodingConstraint(csolver, This->inputs.get(i).getBoolean());
 	}
 }
 
-void naiveEncodingPredicate(BooleanPredicate *This) {
+void naiveEncodingPredicate(CSolver *csolver, BooleanPredicate *This) {
 	FunctionEncoding *encoding = This->getFunctionEncoding();
 	if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)
 		This->getFunctionEncoding()->setFunctionEncodingType(ENUMERATEIMPLICATIONS);
 
 	for (uint i = 0; i < This->inputs.getSize(); i++) {
 		Element *element = This->inputs.get(i);
-		naiveEncodingElement(element);
+		naiveEncodingElement(csolver, element);
 	}
 }
 
-void naiveEncodingElement(Element *This) {
-	ElementEncoding *encoding = getElementEncoding(This);
+void naiveEncodingElement(CSolver *csolver, Element *This) {
+	ElementEncoding *encoding = This->getElementEncoding();
 	if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
-		encoding->setElementEncodingType(BINARYINDEX);
+		if(This->type != ELEMCONST){
+			model_print("INFO: naive encoder is making the decision about element %p....\n", This);
+		}
+		encoding->setElementEncodingType((ElementEncodingType)csolver->getTuner()->getVarTunable(This->getRange()->getType(), NAIVEENCODER, &NaiveEncodingDesc));
 		encoding->encodingArrayInitialization();
 	}
 
@@ -72,11 +77,11 @@ void naiveEncodingElement(Element *This) {
 		ElementFunction *function = (ElementFunction *) This;
 		for (uint i = 0; i < function->inputs.getSize(); i++) {
 			Element *element = function->inputs.get(i);
-			naiveEncodingElement(element);
+			naiveEncodingElement(csolver, element);
 		}
-		FunctionEncoding *encoding = getElementFunctionEncoding(function);
+		FunctionEncoding *encoding = function->getElementFunctionEncoding();
 		if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)
-			getElementFunctionEncoding(function)->setFunctionEncodingType(ENUMERATEIMPLICATIONS);
+			function->getElementFunctionEncoding()->setFunctionEncodingType(ENUMERATEIMPLICATIONS);
 	}
 }