Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constraint) {
PredicateOperator *predicate = (PredicateOperator *)constraint->predicate;
- uint numDomains = predicate->domains.getSize();
-
+ uint numDomains = constraint->inputs.getSize();
+ Polarity polarity = constraint->polarity;
FunctionEncodingType encType = constraint->encoding.type;
bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
+ if (generateNegation)
+ polarity = negatePolarity(polarity);
/* Call base encoders for children */
for (uint i = 0; i < numDomains; i++) {
uint64_t vals[numDomains];//setup value array
for (uint i = 0; i < numDomains; i++) {
- Set *set = predicate->domains.get(i);
+ Set *set = constraint->inputs.get(i)->getRange();
vals[i] = set->getElement(indices[i]);
}
bool notfinished = true;
+ Edge carray[numDomains];
while (notfinished) {
- Edge carray[numDomains];
-
if (predicate->evalPredicateOperator(vals) != generateNegation) {
//Include this in the set of terms
for (uint i = 0; i < numDomains; i++) {
Element *elem = constraint->inputs.get(i);
- carray[i] = getElementValueConstraint(elem, vals[i]);
+ carray[i] = getElementValueConstraint(elem, polarity, vals[i]);
}
Edge term = constraintAND(cnf, numDomains, carray);
pushVectorEdge(clauses, term);
+ ASSERT(getSizeVectorEdge(clauses) > 0);
}
notfinished = false;
for (uint i = 0; i < numDomains; i++) {
uint index = ++indices[i];
- Set *set = predicate->domains.get(i);
+ Set *set = constraint->inputs.get(i)->getRange();
if (index < set->getSize()) {
vals[i] = set->getElement(index);
}
}
if (getSizeVectorEdge(clauses) == 0) {
- clearVectorEdge(clauses);
return E_False;
}
Edge cor = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
vals[i] = set->getElement(indices[i]);
}
- Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
-
bool notfinished = true;
+ Edge carray[numDomains + 1];
while (notfinished) {
- Edge carray[numDomains + 1];
-
uint64_t result = function->applyFunctionOperator(numDomains, vals);
bool isInRange = ((FunctionOperator *)func->getFunction())->isInRangeFunction(result);
bool needClause = isInRange;
//Include this in the set of terms
for (uint i = 0; i < numDomains; i++) {
Element *elem = func->inputs.get(i);
- carray[i] = getElementValueConstraint(elem, vals[i]);
+ carray[i] = getElementValueConstraint(elem, P_FALSE, vals[i]);
}
if (isInRange) {
- carray[numDomains] = getElementValueConstraint(func, result);
+ carray[numDomains] = getElementValueConstraint(func, P_TRUE, result);
}
Edge clause;
break;
}
case SATC_FLAGFORCESOVERFLOW: {
+ Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
break;
}
if (isInRange) {
clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
} else {
+ Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), overFlowConstraint);
}
break;
}
case SATC_FLAGIFFOVERFLOW: {
+ Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
if (isInRange) {
clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
} else {
deleteVectorEdge(clauses);
return;
}
- Edge cor = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
- addConstraintCNF(cnf, cor);
+ Edge cand = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+ addConstraintCNF(cnf, cand);
deleteVectorEdge(clauses);
}