#include "element.h"
#include "common.h"
-Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
- ASSERT(GETPREDICATETYPE(constraint->predicate) == TABLEPRED);
+Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *constraint) {
+ ASSERT(constraint->predicate->type == TABLEPRED);
UndefinedBehavior undefStatus = ((PredicateTable *)constraint->predicate)->undefinedbehavior;
- ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
+ ASSERT(undefStatus == SATC_IGNOREBEHAVIOR || undefStatus == SATC_FLAGFORCEUNDEFINED);
Table *table = ((PredicateTable *)constraint->predicate)->table;
FunctionEncodingType encType = constraint->encoding.type;
- Array<Element*> * inputs = &constraint->inputs;
+ Array<Element *> *inputs = &constraint->inputs;
uint inputNum = inputs->getSize();
- uint size = getSizeHashSetTableEntry(table->entries);
+ uint size = table->getSize();
bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
Edge constraints[size];
- Edge undefConst = encodeConstraintSATEncoder(This, constraint->undefStatus);
+ Edge undefConst = encodeConstraintSATEncoder(constraint->undefStatus);
printCNF(undefConst);
model_print("**\n");
- HSIteratorTableEntry *iterator = iteratorTableEntry(table->entries);
+ SetIteratorTableEntry *iterator = table->getEntries();
uint i = 0;
- while (hasNextTableEntry(iterator)) {
- TableEntry *entry = nextTableEntry(iterator);
- if (generateNegation == (entry->output != 0) && undefStatus == IGNOREBEHAVIOR) {
+ while (iterator->hasNext()) {
+ TableEntry *entry = iterator->next();
+ if (generateNegation == (entry->output != 0) && undefStatus == SATC_IGNOREBEHAVIOR) {
//Skip the irrelevant entries
continue;
}
Edge carray[inputNum];
for (uint j = 0; j < inputNum; j++) {
Element *el = inputs->get(j);
- carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
+ carray[j] = getElementValueConstraint(el, entry->inputs[j]);
printCNF(carray[j]);
model_print("\n");
}
Edge row;
switch (undefStatus) {
- case IGNOREBEHAVIOR:
- row = constraintAND(This->cnf, inputNum, carray);
+ case SATC_IGNOREBEHAVIOR:
+ row = constraintAND(cnf, inputNum, carray);
break;
- case FLAGFORCEUNDEFINED: {
- addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintNegate(undefConst)));
+ case SATC_FLAGFORCEUNDEFINED: {
+ addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintNegate(undefConst)));
if (generateNegation == (entry->output != 0)) {
continue;
}
- row = constraintAND(This->cnf, inputNum, carray);
+ row = constraintAND(cnf, inputNum, carray);
break;
}
default:
model_print("\n\n");
}
- deleteIterTableEntry(iterator);
+ delete iterator;
ASSERT(i != 0);
- Edge result = generateNegation ? constraintNegate(constraintOR(This->cnf, i, constraints))
- : constraintOR(This->cnf, i, constraints);
+ Edge result = generateNegation ? constraintNegate(constraintOR(cnf, i, constraints))
+ : constraintOR(cnf, i, constraints);
printCNF(result);
return result;
}
-Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint) {
#ifdef TRACE_DEBUG
model_print("Enumeration Table Predicate ...\n");
#endif
- ASSERT(GETPREDICATETYPE(constraint->predicate) == TABLEPRED);
+ ASSERT(constraint->predicate->type == TABLEPRED);
//First encode children
Array<Element *> *inputs = &constraint->inputs;
uint inputNum = inputs->getSize();
//Encode all the inputs first ...
for (uint i = 0; i < inputNum; i++) {
- encodeElementSATEncoder(This, inputs->get(i));
+ encodeElementSATEncoder(inputs->get(i));
}
PredicateTable *predicate = (PredicateTable *)constraint->predicate;
switch (predicate->undefinedbehavior) {
- case IGNOREBEHAVIOR:
- case FLAGFORCEUNDEFINED:
- return encodeEnumEntriesTablePredicateSATEncoder(This, constraint);
+ case SATC_IGNOREBEHAVIOR:
+ case SATC_FLAGFORCEUNDEFINED:
+ return encodeEnumEntriesTablePredicateSATEncoder(constraint);
default:
break;
}
bool generateNegation = constraint->encoding.type == ENUMERATEIMPLICATIONSNEGATE;
- uint numDomains = predicate->table->domains.getSize();
-
+ uint numDomains = predicate->table->numDomains();
+ ASSERT(numDomains != 0);
VectorEdge *clauses = allocDefVectorEdge();
uint indices[numDomains]; //setup indices
uint64_t vals[numDomains];//setup value array
for (uint i = 0; i < numDomains; i++) {
- Set *set = predicate->table->domains.get(i);
+ Set *set = predicate->table->getDomain(i);
vals[i] = set->getElement(indices[i]);
}
bool hasOverflow = false;
- Edge undefConstraint = encodeConstraintSATEncoder (This, constraint->undefStatus);
+ Edge undefConstraint = encodeConstraintSATEncoder(constraint->undefStatus);
printCNF(undefConstraint);
bool notfinished = true;
while (notfinished) {
Edge clause;
for (uint i = 0; i < numDomains; i++) {
Element *elem = constraint->inputs.get(i);
- carray[i] = getElementValueConstraint(This, elem, vals[i]);
+ carray[i] = getElementValueConstraint(elem, vals[i]);
}
switch (predicate->undefinedbehavior) {
- case UNDEFINEDSETSFLAG:
+ case SATC_UNDEFINEDSETSFLAG:
if (isInRange) {
- clause = constraintAND(This->cnf, numDomains, carray);
+ clause = constraintAND(cnf, numDomains, carray);
} else {
- addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint) );
+ addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), undefConstraint) );
}
break;
- case FLAGIFFUNDEFINED:
+ case SATC_FLAGIFFUNDEFINED:
if (isInRange) {
- clause = constraintAND(This->cnf, numDomains, carray);
- addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintNegate(undefConstraint)));
+ clause = constraintAND(cnf, numDomains, carray);
+ addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintNegate(undefConstraint)));
} else {
- addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint) );
+ addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint) );
}
break;
notfinished = false;
for (uint i = 0; i < numDomains; i++) {
uint index = ++indices[i];
- Set *set = predicate->table->domains.get(i);
+ Set *set = predicate->table->getDomain(i);
if (index < set->getSize()) {
vals[i] = set->getElement(index);
}
Edge result = E_NULL;
ASSERT(getSizeVectorEdge(clauses) != 0);
- result = constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+ result = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
if (hasOverflow) {
- result = constraintOR2(This->cnf, result, undefConstraint);
+ result = constraintOR2(cnf, result, undefConstraint);
}
if (generateNegation) {
ASSERT(!hasOverflow);
return result;
}
-void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder *This, ElementFunction *func) {
- UndefinedBehavior undefStatus = ((FunctionTable *) func->function)->undefBehavior;
- ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
+void SATEncoder::encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *func) {
+ UndefinedBehavior undefStatus = ((FunctionTable *) func->getFunction())->undefBehavior;
+ ASSERT(undefStatus == SATC_IGNOREBEHAVIOR || undefStatus == SATC_FLAGFORCEUNDEFINED);
Array<Element *> *elements = &func->inputs;
- Table *table = ((FunctionTable *) (func->function))->table;
- uint size = getSizeHashSetTableEntry(table->entries);
+ Table *table = ((FunctionTable *) (func->getFunction()))->table;
+ uint size = table->getSize();
Edge constraints[size];
- HSIteratorTableEntry *iterator = iteratorTableEntry(table->entries);
+ SetIteratorTableEntry *iterator = table->getEntries();
uint i = 0;
- while (hasNextTableEntry(iterator)) {
- TableEntry *entry = nextTableEntry(iterator);
+ while (iterator->hasNext()) {
+ TableEntry *entry = iterator->next();
ASSERT(entry != NULL);
uint inputNum = elements->getSize();
Edge carray[inputNum];
for (uint j = 0; j < inputNum; j++) {
Element *el = elements->get(j);
- carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
+ carray[j] = getElementValueConstraint(el, entry->inputs[j]);
}
- Edge output = getElementValueConstraint(This, (Element *)func, entry->output);
+ Edge output = getElementValueConstraint(func, entry->output);
Edge row;
switch (undefStatus ) {
- case IGNOREBEHAVIOR: {
- row = constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), output);
+ case SATC_IGNOREBEHAVIOR: {
+ row = constraintIMPLIES(cnf,constraintAND(cnf, inputNum, carray), output);
break;
}
- case FLAGFORCEUNDEFINED: {
- Edge undefConst = encodeConstraintSATEncoder(This, func->overflowstatus);
- row = constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintAND2(This->cnf, output, constraintNegate(undefConst)));
+ case SATC_FLAGFORCEUNDEFINED: {
+ Edge undefConst = encodeConstraintSATEncoder(func->overflowstatus);
+ row = constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintAND2(cnf, output, constraintNegate(undefConst)));
break;
}
default:
}
constraints[i++] = row;
}
- deleteIterTableEntry(iterator);
- addConstraintCNF(This->cnf, constraintAND(This->cnf, size, constraints));
+ delete iterator;
+ addConstraintCNF(cnf, constraintAND(cnf, size, constraints));
}
-void encodeEnumTableElemFunctionSATEncoder(SATEncoder *This, ElementFunction *elemFunc) {
+void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc) {
#ifdef TRACE_DEBUG
model_print("Enumeration Table functions ...\n");
#endif
- ASSERT(GETFUNCTIONTYPE(elemFunc->function) == TABLEFUNC);
+ ASSERT(elemFunc->getFunction()->type == TABLEFUNC);
//First encode children
Array<Element *> *elements = &elemFunc->inputs;
for (uint i = 0; i < elements->getSize(); i++) {
Element *elem = elements->get(i);
- encodeElementSATEncoder(This, elem);
+ encodeElementSATEncoder(elem);
}
- FunctionTable *function = (FunctionTable *)elemFunc->function;
+ FunctionTable *function = (FunctionTable *)elemFunc->getFunction();
switch (function->undefBehavior) {
- case IGNOREBEHAVIOR:
- case FLAGFORCEUNDEFINED:
- return encodeEnumEntriesTableElemFuncSATEncoder(This, elemFunc);
+ case SATC_IGNOREBEHAVIOR:
+ case SATC_FLAGFORCEUNDEFINED:
+ return encodeEnumEntriesTableElemFuncSATEncoder(elemFunc);
default:
break;
}
- uint numDomains = function->table->domains.getSize();
+ uint numDomains = function->table->numDomains();
VectorEdge *clauses = allocDefVectorEdge(); // Setup array of clauses
uint64_t vals[numDomains];//setup value array
for (uint i = 0; i < numDomains; i++) {
- Set *set = function->table->domains.get(i);
+ Set *set = function->table->getDomain(i);
vals[i] = set->getElement(indices[i]);
}
- Edge undefConstraint = encodeConstraintSATEncoder(This, elemFunc->overflowstatus);
+ Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus);
bool notfinished = true;
while (notfinished) {
Edge carray[numDomains + 1];
TableEntry *tableEntry = function->table->getTableEntry(vals, numDomains);
bool isInRange = tableEntry != NULL;
- ASSERT(function->undefBehavior == UNDEFINEDSETSFLAG || function->undefBehavior == FLAGIFFUNDEFINED);
+ ASSERT(function->undefBehavior == SATC_UNDEFINEDSETSFLAG || function->undefBehavior == SATC_FLAGIFFUNDEFINED);
for (uint i = 0; i < numDomains; i++) {
Element *elem = elemFunc->inputs.get(i);
- carray[i] = getElementValueConstraint(This, elem, vals[i]);
+ carray[i] = getElementValueConstraint(elem, vals[i]);
}
if (isInRange) {
- carray[numDomains] = getElementValueConstraint(This, (Element *)elemFunc, tableEntry->output);
+ carray[numDomains] = getElementValueConstraint(elemFunc, tableEntry->output);
}
Edge clause;
switch (function->undefBehavior) {
- case UNDEFINEDSETSFLAG: {
+ case SATC_UNDEFINEDSETSFLAG: {
if (isInRange) {
- //FIXME: Talk to Brian, It should be IFF not only IMPLY. --HG
- clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
+ clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
} else {
- addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint));
+ addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
}
break;
}
- case FLAGIFFUNDEFINED: {
+ case SATC_FLAGIFFUNDEFINED: {
if (isInRange) {
- clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
- addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf, constraintAND(This->cnf, numDomains, carray), constraintNegate(undefConstraint) ));
+ clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
+ addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintNegate(undefConstraint) ));
} else {
- addConstraintCNF(This->cnf,constraintIMPLIES(This->cnf, constraintAND(This->cnf, numDomains, carray), undefConstraint));
+ addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
}
break;
}
notfinished = false;
for (uint i = 0; i < numDomains; i++) {
uint index = ++indices[i];
- Set *set = function->table->domains.get(i);
+ Set *set = function->table->getDomain(i);
if (index < set->getSize()) {
vals[i] = set->getElement(index);
deleteVectorEdge(clauses);
return;
}
- Edge cor = constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
- addConstraintCNF(This->cnf, cor);
+ Edge cor = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+ addConstraintCNF(cnf, cor);
deleteVectorEdge(clauses);
-
}
projects / satune.git / blobdiff