#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();
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){
+ 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);
+ generateAnyValueBinaryIndexEncoding(encoding);
}
}
}