#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();
getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
if (encoding->element->anyValue) {
uint setSize = encoding->element->getRange()->getSize();
- uint encArraySize = encoding->encArraySize;
- if (setSize < encArraySize * (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex) / 10) {
+ int maxIndex = getMaximumUsedIndex(encoding);
+// model_print("maxIndex=%d\tsetSize=%u\tmetric=%f\n", maxIndex, setSize, (maxIndex - setSize) == 0? -1.0 : (setSize*1.0/(maxIndex-setSize)) );
+ if (maxIndex != -1 && (maxIndex - setSize) != 0 && (setSize * 1.0 / (maxIndex - setSize)) < pow(1.9, (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex) - 4)) {
generateAnyValueBinaryIndexEncodingPositive(encoding);
} else {
generateAnyValueBinaryIndexEncoding(encoding);
}
}
-void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding) {
- if (encoding->numVars == 0)
- return;
+int SATEncoder::getMaximumUsedIndex(ElementEncoding *encoding) {
int index = -1;
for (uint i = encoding->encArraySize - 1; i >= 0; i--) {
if (encoding->isinUseElement(i)) {
break;
}
}
+ return index;
+}
+
+void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding) {
+ if (encoding->numVars == 0)
+ return;
+ int index = getMaximumUsedIndex(encoding);
if ( index != -1 ) {
addConstraintCNF(cnf, generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, index));
}