adding different handlers for predicatetable

diff --git a/src/Backend/satfunctableencoder.c b/src/Backend/satfunctableencoder.c
index 64b5efb6f2b3a0d4bcdcbfc4bc60e55737567b54..a9ba7b17e2d9f41be44cf1141503a5d02798431b 100644 (file)
--- a/src/Backend/satfunctableencoder.c
+++ b/src/Backend/satfunctableencoder.c
@@ -11,14 +11,13 @@
 #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];
@@ -35,15 +34,123 @@ Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder * This, BooleanPredica
                        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){
@@ -127,49 +234,44 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* el
                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++) {