Fixing the anyvalue heuristic for binaryIndex

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

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index 8f06eecad991e3d68d9b83e5d5b47f3bba3a4f6b..3cd2c1c70b9385e032d7cf4ba99e446f2829f212 100644 (file)
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -7,6 +7,7 @@
 #include "predicate.h"
 #include "csolver.h"
 #include "tunable.h"
+#include <cmath>
 
 void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool &memo) {
        uint numParents = elem->parents.getSize();
@@ -223,10 +224,11 @@ 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;
-               if(setSize < encArraySize * (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex)/10){
+               double metric = encArraySize == setSize?setSize:setSize/(encArraySize-setSize);
+               if ( log(metric) <  pow(1.9, (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex) - 4)) {
                        generateAnyValueBinaryIndexEncodingPositive(encoding);
                } else {
                        generateAnyValueBinaryIndexEncoding(encoding);