Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *constraint) {
ASSERT(constraint->predicate->type == TABLEPRED);
UndefinedBehavior undefStatus = ((PredicateTable *)constraint->predicate)->undefinedbehavior;
- ASSERT(undefStatus == SATC_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;
uint inputNum = inputs->getSize();
- uint size = table->entries->getSize();
+ uint size = table->getSize();
+ Polarity polarity = constraint->polarity;
bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
+ if (generateNegation)
+ polarity = negatePolarity(polarity);
+ if (undefStatus ==SATC_FLAGFORCEUNDEFINED)
+ polarity = P_BOTHTRUEFALSE;
+
Edge constraints[size];
- Edge undefConst = encodeConstraintSATEncoder(constraint->undefStatus);
- printCNF(undefConst);
- model_print("**\n");
- HSIteratorTableEntry *iterator = table->entries->iterator();
+
+ SetIteratorTableEntry *iterator = table->getEntries();
uint i = 0;
while (iterator->hasNext()) {
TableEntry *entry = iterator->next();
Edge carray[inputNum];
for (uint j = 0; j < inputNum; j++) {
Element *el = inputs->get(j);
- carray[j] = getElementValueConstraint(el, entry->inputs[j]);
- printCNF(carray[j]);
- model_print("\n");
+ carray[j] = getElementValueConstraint(el, polarity, entry->inputs[j]);
}
Edge row;
switch (undefStatus) {
case SATC_IGNOREBEHAVIOR:
row = constraintAND(cnf, inputNum, carray);
break;
- case FLAGFORCEUNDEFINED: {
- addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintNegate(undefConst)));
+ case SATC_FLAGFORCEUNDEFINED: {
+ Edge proxy = constraintNewVar(cnf);
+ generateProxy(cnf, constraintAND(cnf, inputNum, carray), proxy, P_BOTHTRUEFALSE);
+ Edge undefConst = encodeConstraintSATEncoder(constraint->undefStatus);
+ addConstraintCNF(cnf, constraintIMPLIES(cnf, proxy, constraintNegate(undefConst)));
if (generateNegation == (entry->output != 0)) {
continue;
}
- row = constraintAND(cnf, inputNum, carray);
+ row = proxy;
break;
}
default:
ASSERT(0);
}
constraints[i++] = row;
- printCNF(row);
-
- model_print("\n\n");
}
delete iterator;
ASSERT(i != 0);
Edge result = generateNegation ? constraintNegate(constraintOR(cnf, i, constraints))
: constraintOR(cnf, i, constraints);
- printCNF(result);
return result;
}
+
Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint) {
#ifdef TRACE_DEBUG
model_print("Enumeration Table Predicate ...\n");
#endif
ASSERT(constraint->predicate->type == TABLEPRED);
+ Polarity polarity = constraint->polarity;
+
//First encode children
Array<Element *> *inputs = &constraint->inputs;
uint inputNum = inputs->getSize();
PredicateTable *predicate = (PredicateTable *)constraint->predicate;
switch (predicate->undefinedbehavior) {
case SATC_IGNOREBEHAVIOR:
- case FLAGFORCEUNDEFINED:
+ 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();
+ if (generateNegation)
+ polarity = negatePolarity(polarity);
+
+ 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(constraint->undefStatus);
- printCNF(undefConstraint);
+
bool notfinished = true;
while (notfinished) {
Edge carray[numDomains];
Edge clause;
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]);
}
switch (predicate->undefinedbehavior) {
- case UNDEFINEDSETSFLAG:
+ case SATC_UNDEFINEDSETSFLAG:
if (isInRange) {
clause = constraintAND(cnf, numDomains, carray);
} else {
+ Edge undefConstraint = encodeConstraintSATEncoder(constraint->undefStatus);
addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), undefConstraint) );
}
break;
- case FLAGIFFUNDEFINED:
+ case SATC_FLAGIFFUNDEFINED: {
+ Edge undefConstraint = encodeConstraintSATEncoder(constraint->undefStatus);
if (isInRange) {
clause = constraintAND(cnf, numDomains, carray);
addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintNegate(undefConstraint)));
addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint) );
}
break;
-
+ }
default:
ASSERT(0);
}
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);
ASSERT(getSizeVectorEdge(clauses) != 0);
result = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
if (hasOverflow) {
+ Edge undefConstraint = encodeConstraintSATEncoder(constraint->undefStatus);
result = constraintOR2(cnf, result, undefConstraint);
}
if (generateNegation) {
}
void SATEncoder::encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *func) {
- UndefinedBehavior undefStatus = ((FunctionTable *) func->function)->undefBehavior;
- ASSERT(undefStatus == SATC_IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
+ 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 = table->entries->getSize();
+
+ Table *table = ((FunctionTable *) (func->getFunction()))->table;
+ uint size = table->getSize();
Edge constraints[size];
- HSIteratorTableEntry *iterator = table->entries->iterator();
+ SetIteratorTableEntry *iterator = table->getEntries();
uint i = 0;
while (iterator->hasNext()) {
TableEntry *entry = iterator->next();
Edge carray[inputNum];
for (uint j = 0; j < inputNum; j++) {
Element *el = elements->get(j);
- carray[j] = getElementValueConstraint(el, entry->inputs[j]);
+ carray[j] = getElementValueConstraint(el, P_FALSE, entry->inputs[j]);
}
- Edge output = getElementValueConstraint(func, entry->output);
- Edge row;
+ Edge output = getElementValueConstraint(func, P_TRUE, entry->output);
switch (undefStatus ) {
case SATC_IGNOREBEHAVIOR: {
- row = constraintIMPLIES(cnf,constraintAND(cnf, inputNum, carray), output);
+ if(inputNum == 0){
+ addConstraintCNF(cnf, output);
+ }else{
+ addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, inputNum, carray), output));
+ }
break;
}
- case FLAGFORCEUNDEFINED: {
+ case SATC_FLAGFORCEUNDEFINED: {
Edge undefConst = encodeConstraintSATEncoder(func->overflowstatus);
- row = constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintAND2(cnf, output, constraintNegate(undefConst)));
+ if(inputNum ==0){
+ addConstraintCNF(cnf, constraintAND2(cnf, output, constraintNegate(undefConst)));
+ }else{
+ addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintAND2(cnf, output, constraintNegate(undefConst))));
+ }
break;
}
default:
ASSERT(0);
}
- constraints[i++] = row;
}
delete iterator;
- addConstraintCNF(cnf, constraintAND(cnf, size, constraints));
}
void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc) {
#ifdef TRACE_DEBUG
model_print("Enumeration Table functions ...\n");
#endif
- ASSERT(elemFunc->function->type == TABLEFUNC);
+ ASSERT(elemFunc->getFunction()->type == TABLEFUNC);
+
//First encode children
Array<Element *> *elements = &elemFunc->inputs;
for (uint i = 0; i < elements->getSize(); i++) {
encodeElementSATEncoder(elem);
}
- FunctionTable *function = (FunctionTable *)elemFunc->function;
+ FunctionTable *function = (FunctionTable *)elemFunc->getFunction();
switch (function->undefBehavior) {
case SATC_IGNOREBEHAVIOR:
- case FLAGFORCEUNDEFINED:
+ case SATC_FLAGFORCEUNDEFINED:
return encodeEnumEntriesTableElemFuncSATEncoder(elemFunc);
default:
break;
}
- uint numDomains = function->table->domains.getSize();
-
- VectorEdge *clauses = allocDefVectorEdge(); // Setup array of clauses
+ uint numDomains = function->table->numDomains();
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 = function->table->domains.get(i);
+ Set *set = function->table->getDomain(i);
vals[i] = set->getElement(indices[i]);
}
- 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(elem, vals[i]);
+ carray[i] = getElementValueConstraint(elem, P_FALSE, vals[i]);
}
if (isInRange) {
- carray[numDomains] = getElementValueConstraint(elemFunc, tableEntry->output);
+ carray[numDomains] = getElementValueConstraint(elemFunc, P_TRUE, 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(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
+ if(numDomains == 0){
+ addConstraintCNF(cnf,carray[numDomains]);
+ }else{
+ addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]));
+ }
} else {
+ Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus);
addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
}
break;
}
- case FLAGIFFUNDEFINED: {
+ case SATC_FLAGIFFUNDEFINED: {
+ Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus);
if (isInRange) {
- clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
- addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintNegate(undefConstraint) ));
+ if(numDomains == 0){
+ addConstraintCNF(cnf, constraintAND2(cnf,carray[numDomains], constraintNegate(undefConstraint)) );
+ }else{
+ Edge freshvar = constraintNewVar(cnf);
+ addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), freshvar ));
+ addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, constraintNegate(undefConstraint) ));
+ addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, carray[numDomains]));
+ }
+
} else {
addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
}
printCNF(clause);
model_print("\n");
#endif
- pushVectorEdge(clauses, clause);
}
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);
}
}
}
- if (getSizeVectorEdge(clauses) == 0) {
- deleteVectorEdge(clauses);
- return;
- }
- Edge cor = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
- addConstraintCNF(cnf, cor);
- deleteVectorEdge(clauses);
}
projects / satune.git / blobdiff