#include "set.h"
#include "element.h"
#include "common.h"
-#include "satfuncopencoder.h"
-Edge encodeOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+Edge SATEncoder::encodeOperatorPredicateSATEncoder(BooleanPredicate *constraint) {
switch (constraint->encoding.type) {
case ENUMERATEIMPLICATIONS:
- return encodeEnumOperatorPredicateSATEncoder(This, constraint);
+ return encodeEnumOperatorPredicateSATEncoder(constraint);
case CIRCUIT:
- return encodeCircuitOperatorPredicateEncoder(This, constraint);
+ return encodeCircuitOperatorPredicateEncoder(constraint);
default:
ASSERT(0);
}
exit(-1);
}
-Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constraint) {
PredicateOperator *predicate = (PredicateOperator *)constraint->predicate;
- uint numDomains = getSizeArraySet(&predicate->domains);
-
+ uint numDomains = predicate->domains.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++) {
- Element *elem = getArrayElement( &constraint->inputs, i);
- encodeElementSATEncoder(This, elem);
+ Element *elem = constraint->inputs.get(i);
+ encodeElementSATEncoder(elem);
}
- VectorEdge *clauses = allocDefVectorEdge(); // Setup array of clauses
+ VectorEdge *clauses = vector;
uint indices[numDomains]; //setup indices
bzero(indices, sizeof(uint) * numDomains);
uint64_t vals[numDomains];//setup value array
for (uint i = 0; i < numDomains; i++) {
- Set *set = getArraySet(&predicate->domains, i);
- vals[i] = getSetElement(set, indices[i]);
+ Set *set = predicate->domains.get(i);
+ vals[i] = set->getElement(indices[i]);
}
bool notfinished = true;
+ Edge carray[numDomains];
while (notfinished) {
- Edge carray[numDomains];
-
- if (evalPredicateOperator(predicate, vals) ^ generateNegation) {
+ if (predicate->evalPredicateOperator(vals) != generateNegation) {
//Include this in the set of terms
for (uint i = 0; i < numDomains; i++) {
- Element *elem = getArrayElement(&constraint->inputs, i);
- carray[i] = getElementValueConstraint(This, elem, vals[i]);
+ Element *elem = constraint->inputs.get(i);
+ carray[i] = getElementValueConstraint(elem, polarity, vals[i]);
}
- Edge term = constraintAND(This->cnf, numDomains, carray);
+ 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 = getArraySet(&predicate->domains, i);
+ Set *set = predicate->domains.get(i);
- if (index < getSetSize(set)) {
- vals[i] = getSetElement(set, index);
+ if (index < set->getSize()) {
+ vals[i] = set->getElement(index);
notfinished = true;
break;
} else {
indices[i] = 0;
- vals[i] = getSetElement(set, 0);
+ vals[i] = set->getElement(0);
}
}
}
if (getSizeVectorEdge(clauses) == 0) {
- deleteVectorEdge(clauses);
return E_False;
}
- Edge cor = constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
- deleteVectorEdge(clauses);
+ Edge cor = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+ clearVectorEdge(clauses);
return generateNegation ? constraintNegate(cor) : cor;
}
-void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction *func) {
+void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func) {
#ifdef TRACE_DEBUG
model_print("Operator Function ...\n");
#endif
- FunctionOperator *function = (FunctionOperator *) func->function;
- uint numDomains = getSizeArrayElement(&func->inputs);
+ FunctionOperator *function = (FunctionOperator *) func->getFunction();
+ uint numDomains = func->inputs.getSize();
/* Call base encoders for children */
for (uint i = 0; i < numDomains; i++) {
- Element *elem = getArrayElement( &func->inputs, i);
- encodeElementSATEncoder(This, elem);
+ Element *elem = func->inputs.get(i);
+ encodeElementSATEncoder(elem);
}
VectorEdge *clauses = allocDefVectorEdge(); // Setup array of clauses
uint64_t vals[numDomains];//setup value array
for (uint i = 0; i < numDomains; i++) {
- Set *set = getElementSet(getArrayElement(&func->inputs, i));
- vals[i] = getSetElement(set, indices[i]);
+ Set *set = func->inputs.get(i)->getRange();
+ vals[i] = set->getElement(indices[i]);
}
- Edge overFlowConstraint = ((BooleanVar *) func->overflowstatus)->var;
-
bool notfinished = true;
+ Edge carray[numDomains + 1];
while (notfinished) {
- Edge carray[numDomains + 1];
-
- uint64_t result = applyFunctionOperator(function, numDomains, vals);
- bool isInRange = isInRangeFunction((FunctionOperator *)func->function, result);
+ uint64_t result = function->applyFunctionOperator(numDomains, vals);
+ bool isInRange = ((FunctionOperator *)func->getFunction())->isInRangeFunction(result);
bool needClause = isInRange;
- if (function->overflowbehavior == OVERFLOWSETSFLAG || function->overflowbehavior == FLAGIFFOVERFLOW) {
+ if (function->overflowbehavior == SATC_OVERFLOWSETSFLAG || function->overflowbehavior == SATC_FLAGIFFOVERFLOW) {
needClause = true;
}
if (needClause) {
//Include this in the set of terms
for (uint i = 0; i < numDomains; i++) {
- Element *elem = getArrayElement(&func->inputs, i);
- carray[i] = getElementValueConstraint(This, elem, vals[i]);
+ Element *elem = func->inputs.get(i);
+ carray[i] = getElementValueConstraint(elem, P_FALSE, vals[i]);
}
if (isInRange) {
- carray[numDomains] = getElementValueConstraint(This, &func->base, result);
+ carray[numDomains] = getElementValueConstraint(func, P_TRUE, result);
}
Edge clause;
switch (function->overflowbehavior) {
- case IGNORE:
- case NOOVERFLOW:
- case WRAPAROUND: {
- clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
+ case SATC_IGNORE:
+ case SATC_NOOVERFLOW:
+ case SATC_WRAPAROUND: {
+ clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
break;
}
- case FLAGFORCESOVERFLOW: {
- clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
+ case SATC_FLAGFORCESOVERFLOW: {
+ Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
+ clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
break;
}
- case OVERFLOWSETSFLAG: {
+ case SATC_OVERFLOWSETSFLAG: {
if (isInRange) {
- clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
+ clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
} else {
- clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
+ Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
+ clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), overFlowConstraint);
}
break;
}
- case FLAGIFFOVERFLOW: {
+ case SATC_FLAGIFFOVERFLOW: {
+ Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
if (isInRange) {
- clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
+ clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
} else {
- clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
+ clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), overFlowConstraint);
}
break;
}
notfinished = false;
for (uint i = 0; i < numDomains; i++) {
uint index = ++indices[i];
- Set *set = getElementSet(getArrayElement(&func->inputs, i));
+ Set *set = func->inputs.get(i)->getRange();
- if (index < getSetSize(set)) {
- vals[i] = getSetElement(set, index);
+ if (index < set->getSize()) {
+ vals[i] = set->getElement(index);
notfinished = true;
break;
} else {
indices[i] = 0;
- vals[i] = getSetElement(set, 0);
+ vals[i] = set->getElement(0);
}
}
}
deleteVectorEdge(clauses);
return;
}
- Edge cor = constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
- addConstraintCNF(This->cnf, cor);
+ Edge cand = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+ addConstraintCNF(cnf, cand);
deleteVectorEdge(clauses);
}
-Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+Edge SATEncoder::encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constraint) {
PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
- ASSERT(getSizeArraySet(&predicate->domains) == 2);
- Element *elem0 = getArrayElement( &constraint->inputs, 0);
- encodeElementSATEncoder(This, elem0);
- Element *elem1 = getArrayElement( &constraint->inputs, 1);
- encodeElementSATEncoder(This, elem1);
- ElementEncoding *ee0 = getElementEncoding(elem0);
- ElementEncoding *ee1 = getElementEncoding(elem1);
+ Element *elem0 = constraint->inputs.get(0);
+ encodeElementSATEncoder(elem0);
+ Element *elem1 = constraint->inputs.get(1);
+ encodeElementSATEncoder(elem1);
+ ElementEncoding *ee0 = elem0->getElementEncoding();
+ ElementEncoding *ee1 = elem1->getElementEncoding();
ASSERT(ee0->numVars == ee1->numVars);
uint numVars = ee0->numVars;
- switch (predicate->op) {
- case EQUALS:
- return generateEquivNVConstraint(This->cnf, numVars, ee0->variables, ee1->variables);
- case LT:
- return generateLTConstraint(This->cnf, numVars, ee0->variables, ee1->variables);
- case GT:
- return generateLTConstraint(This->cnf, numVars, ee1->variables, ee0->variables);
- default:
- ASSERT(0);
+ switch (predicate->getOp()) {
+ case SATC_EQUALS:
+ return generateEquivNVConstraint(cnf, numVars, ee0->variables, ee1->variables);
+ case SATC_LT:
+ return generateLTConstraint(cnf, numVars, ee0->variables, ee1->variables);
+ case SATC_GT:
+ return generateLTConstraint(cnf, numVars, ee1->variables, ee0->variables);
+ default:
+ ASSERT(0);
}
exit(-1);
}
projects / satune.git / blobdiff