#include "common.h"
Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+ ASSERT(GETPREDICATETYPE(constraint->predicate) == TABLEPRED);
+ UndefinedBehavior undefStatus = ((PredicateTable*)constraint->predicate)->undefinedbehavior;
+ ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
Table* table = ((PredicateTable*)constraint->predicate)->table;
FunctionEncodingType encType = constraint->encoding.type;
ArrayElement* inputs = &constraint->inputs;
uint inputNum =getSizeArrayElement(inputs);
- //Encode all the inputs first ...
- for(uint i=0; i<inputNum; i++){
- encodeElementSATEncoder(This, getArrayElement(inputs, i));
- }
uint size = getSizeHashSetTableEntry(table->entries);
bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
Edge constraints[size];
Element* el = getArrayElement(inputs, j);
carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
}
- constraints[i++]=constraintAND(This->cnf, inputNum, carray);
+ Edge row;
+ switch(undefStatus){
+ case IGNOREBEHAVIOR:
+ row=constraintAND(This->cnf, inputNum, carray);
+ break;
+ case FLAGFORCEUNDEFINED:{
+ Edge undefConst = ((BooleanVar*)constraint->undefStatus)->var;
+ row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintNegate(undefConst));
+ break;
+ }
+ default:
+ ASSERT(0);
+ }
+ constraints[i++] = row;
+
}
Edge result=constraintOR(This->cnf, size, constraints);
return generateNegation ? constraintNegate(result) : result;
}
Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
- //FIXME
- return E_NULL;
+#ifdef TRACE_DEBUG
+ model_print("Enumeration Table Predicate ...\n");
+#endif
+ ASSERT(GETPREDICATETYPE(constraint->predicate) == TABLEPRED);
+ //First encode children
+ ArrayElement* inputs = &constraint->inputs;
+ uint inputNum =getSizeArrayElement(inputs);
+ //Encode all the inputs first ...
+ for(uint i=0; i<inputNum; i++){
+ encodeElementSATEncoder(This, getArrayElement(inputs, i));
+ }
+ PredicateTable* predicate = (PredicateTable*)constraint->predicate;
+ switch(predicate->undefinedbehavior){
+ case IGNOREBEHAVIOR:
+ case FLAGFORCEUNDEFINED:
+ return encodeEnumEntriesTablePredicateSATEncoder(This, constraint);
+ default:
+ break;
+ }
+ bool generateNegation = constraint->encoding.type == ENUMERATEIMPLICATIONSNEGATE;
+ uint numDomains=getSizeArraySet(&predicate->table->domains);
+
+ VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses
+
+ 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->table->domains, i);
+ vals[i]=getSetElement(set, indices[i]);
+ }
+
+ Edge undefConstraint = ((BooleanVar*) constraint->undefStatus)->var;
+
+ bool notfinished=true;
+ while(notfinished) {
+ Edge carray[numDomains];
+ TableEntry* tableEntry = getTableEntryFromTable(predicate->table, vals, numDomains);
+ bool isInRange = tableEntry!=NULL;
+ bool ignoreEntry = generateNegation == tableEntry->output;
+ ASSERT(predicate->undefinedbehavior == UNDEFINEDSETSFLAG || predicate->undefinedbehavior == FLAGIFFUNDEFINED);
+ //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]);
+ }
+
+ Edge clause;
+ switch(predicate->undefinedbehavior) {
+ case UNDEFINEDSETSFLAG: {
+ if (isInRange && !ignoreEntry) {
+ clause=constraintAND(This->cnf, numDomains, carray);
+ } else if(!isInRange) {
+ clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
+ }
+ break;
+ }
+ case FLAGIFFUNDEFINED: {
+ if (isInRange && !ignoreEntry) {
+ clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(undefConstraint)));
+ } else if(!isInRange) {
+ clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
+ }
+ break;
+ }
+ default:
+ ASSERT(0);
+ }
+#ifdef TRACE_DEBUG
+ model_print("added clause in predicate table enumeration ...\n");
+ printCNF(clause);
+ model_print("\n");
+#endif
+ pushVectorEdge(clauses, clause);
+
+
+ notfinished=false;
+ for(uint i=0;i<numDomains; i++) {
+ uint index=++indices[i];
+ Set * set=getArraySet(&predicate->table->domains, i);
+
+ if (index < getSetSize(set)) {
+ vals[i]=getSetElement(set, index);
+ notfinished=true;
+ break;
+ } else {
+ indices[i]=0;
+ vals[i]=getSetElement(set, 0);
+ }
+ }
+ }
+
+ Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+ deleteVectorEdge(clauses);
+ return generateNegation ? constraintNegate(cor) : cor;
}
void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder* This, ElementFunction* func){
Edge carray[numDomains+1];
TableEntry* tableEntry = getTableEntryFromTable(function->table, vals, numDomains);
bool isInRange = tableEntry!=NULL;
- bool needClause = isInRange;
- if (function->undefBehavior == UNDEFINEDSETSFLAG || function->undefBehavior == FLAGIFFUNDEFINED) {
- needClause=true;
+ ASSERT(function->undefBehavior == UNDEFINEDSETSFLAG || function->undefBehavior == FLAGIFFUNDEFINED);
+ //Include this in the set of terms
+ for(uint i=0;i<numDomains;i++) {
+ Element * elem = getArrayElement(&elemFunc->inputs, i);
+ carray[i] = getElementValueConstraint(This, elem, vals[i]);
+ }
+ if (isInRange) {
+ carray[numDomains] = getElementValueConstraint(This, (Element*)elemFunc, tableEntry->output);
}
-
- if (needClause) {
- //Include this in the set of terms
- for(uint i=0;i<numDomains;i++) {
- Element * elem = getArrayElement(&elemFunc->inputs, i);
- carray[i] = getElementValueConstraint(This, elem, vals[i]);
- }
- if (isInRange) {
- carray[numDomains] = getElementValueConstraint(This, (Element*)elemFunc, tableEntry->output);
- }
- Edge clause;
- switch(function->undefBehavior) {
- case UNDEFINEDSETSFLAG: {
- if (isInRange) {
- clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
- } else {
- clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
- }
- break;
+ Edge clause;
+ switch(function->undefBehavior) {
+ case UNDEFINEDSETSFLAG: {
+ if (isInRange) {
+ clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
+ } else {
+ clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
}
- case FLAGIFFUNDEFINED: {
- if (isInRange) {
- clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(undefConstraint)));
- } else {
- clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
- }
- break;
+ break;
+ }
+ case FLAGIFFUNDEFINED: {
+ if (isInRange) {
+ clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(undefConstraint)));
+ } else {
+ clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
}
- default:
- ASSERT(0);
+ break;
}
+ default:
+ ASSERT(0);
+ }
#ifdef TRACE_DEBUG
- model_print("added clause in table enumeration ...\n");
- printCNF(clause);
- model_print("\n");
+ model_print("added clause in function table enumeration ...\n");
+ printCNF(clause);
+ model_print("\n");
#endif
- pushVectorEdge(clauses, clause);
- }
+ pushVectorEdge(clauses, clause);
+
notfinished=false;
for(uint i=0;i<numDomains; i++) {