getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
if (encoding->element->anyValue) {
uint setSize = encoding->element->getRange()->getSize();
getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
if (encoding->element->anyValue) {
uint setSize = encoding->element->getRange()->getSize();
- int maxIndex = getMaximumUsedIndex(encoding);
- maxIndex = maxIndex == -1? (int)encoding->encArraySize : maxIndex;
- if(setSize == encoding->encArraySize && maxIndex == (int)setSize){
+ int maxIndex = getMaximumUsedSize(encoding);
+ if (setSize == encoding->encArraySize && maxIndex == (int)setSize) {
// model_print("encArraySize=%u\tmaxIndex=%d\tsetSize=%u\tmetric=%f\tnumBits=%u\n", encoding->encArraySize, maxIndex, setSize, ratio, encoding->numVars);
if ( ratio < pow(2, (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex) - 3)) {
generateAnyValueBinaryIndexEncodingPositive(encoding);
// model_print("encArraySize=%u\tmaxIndex=%d\tsetSize=%u\tmetric=%f\tnumBits=%u\n", encoding->encArraySize, maxIndex, setSize, ratio, encoding->numVars);
if ( ratio < pow(2, (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex) - 3)) {
generateAnyValueBinaryIndexEncodingPositive(encoding);
-int SATEncoder::getMaximumUsedIndex(ElementEncoding *encoding) {
- int index = -1;
- for (uint i = encoding->encArraySize - 1; i >= 0; i--) {
- if (encoding->isinUseElement(i)) {
- if (i + 1 < encoding->encArraySize) {
- index = i + 1;
- }
- break;
- }
+int SATEncoder::getMaximumUsedSize(ElementEncoding *encoding) {
+ for (int i = encoding->encArraySize - 1; i >= 0; i--) {
+ if (encoding->isinUseElement(i))
+ return i + 1;
}
void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding) {
if (encoding->numVars == 0)
return;
}
void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding) {
if (encoding->numVars == 0)
return;
addConstraintCNF(cnf, generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, index));
}
addConstraintCNF(cnf, generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, index));
}
if (!encoding->isinUseElement(i)) {
addConstraintCNF(cnf, constraintNegate( generateBinaryConstraint(cnf, encoding->numVars, encoding->variables, i)));
}
if (!encoding->isinUseElement(i)) {
addConstraintCNF(cnf, constraintNegate( generateBinaryConstraint(cnf, encoding->numVars, encoding->variables, i)));
}