Adding a directed search based config for the tuner

[satune.git] / src / Backend / satelemencoder.cc

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index ad0722b2d262bf4a89a792fa220c2d1b8a554013..8f06eecad991e3d68d9b83e5d5b47f3bba3a4f6b 100644 (file)
--- 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,15 @@ void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
        ASSERT(encoding->type == BINARYINDEX);
        allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1));
        getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
-       if (encoding->element->anyValue)
-               generateAnyValueBinaryIndexEncoding(encoding);
+       if (encoding->element->anyValue){
+               uint setSize = encoding->element->getRange()->getSize();
+               uint encArraySize = encoding->encArraySize;
+               if(setSize < encArraySize * (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex)/10){
+                       generateAnyValueBinaryIndexEncodingPositive(encoding);
+               } else {
+                       generateAnyValueBinaryIndexEncoding(encoding);
+               }
+       }
 }
 
 void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) {
@@ -293,6 +301,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;