X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FBackend%2Fsatelemencoder.cc;h=84880fff21574f387accacf7afcf2138defcb1f1;hp=ad0722b2d262bf4a89a792fa220c2d1b8a554013;hb=31d8e919360f167a7a3317d7e9482e3bd9f70b8e;hpb=8caa8c3d3d523566be88803ac9a12eb2e0b14db6

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index ad0722b..84880ff 100644
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -5,7 +5,8 @@
 #include "element.h"
 #include "set.h"
 #include "predicate.h"
-
+#include "csolver.h"
+#include "tunable.h"
 
 void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool &memo) {
 	uint numParents = elem->parents.getSize();
@@ -222,8 +223,16 @@ void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
 	ASSERT(encoding->type == BINARYINDEX);
 	allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1));
 	getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
-	if (encoding->element->anyValue)
+	if (encoding->element->anyValue){
+		uint setSize = encoding->element->getRange()->getSize();
+		uint encArraySize = encoding->encArraySize;
+		model_print("setSize=%u\tencArraySize=%u\n", setSize, encArraySize);
+		if(setSize < encArraySize * (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex)/10){
+			generateAnyValueBinaryIndexEncodingPositive(encoding);
+		} else {
 		generateAnyValueBinaryIndexEncoding(encoding);
+		}
+	}
 }
 
 void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) {
@@ -293,6 +302,20 @@ void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding)
 	}
 }
 
+void SATEncoder::generateAnyValueBinaryIndexEncodingPositive(ElementEncoding *encoding) {
+	if (encoding->numVars == 0)
+		return;
+	Edge carray[encoding->encArraySize];
+	uint size = 0;
+	for (uint i = 0; i < encoding->encArraySize; i++) {
+		if (encoding->isinUseElement(i)) {
+			carray[size] = generateBinaryConstraint(cnf, encoding->numVars, encoding->variables, i);
+			size++;
+		}
+	}
+	addConstraintCNF(cnf, constraintOR(cnf, size, carray));
+}
+
 void SATEncoder::generateAnyValueBinaryValueEncoding(ElementEncoding *encoding) {
 	uint64_t minvalueminusoffset = encoding->low - encoding->offset;
 	uint64_t maxvalueminusoffset = encoding->high - encoding->offset;