src/Backend/satfunctableencoder.c

   1 #include "satencoder.h"
   2 #include "common.h"
   3 #include "function.h"
   4 #include "ops.h"
   5 #include "predicate.h"
   6 #include "boolean.h"
   7 #include "table.h"
   8 #include "tableentry.h"
   9 #include "set.h"
  10 #include "element.h"
  11 #include "common.h"
  12
  13 Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
  14         Table* table = ((PredicateTable*)constraint->predicate)->table;
  15         FunctionEncodingType encType = constraint->encoding.type;
  16         ArrayElement* inputs = &constraint->inputs;
  17         uint inputNum =getSizeArrayElement(inputs);
  18         //Encode all the inputs first ...
  19         for(uint i=0; i<inputNum; i++){
  20                 encodeElementSATEncoder(This, getArrayElement(inputs, i));
  21         }
  22         uint size = getSizeHashSetTableEntry(table->entries);
  23         bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
  24         Edge constraints[size];
  25         HSIteratorTableEntry* iterator = iteratorTableEntry(table->entries);
  26         uint i=0;
  27         while(hasNextTableEntry(iterator)){
  28                 TableEntry* entry = nextTableEntry(iterator);
  29                 if(generateNegation == entry->output) {
  30                         //Skip the irrelevant entries
  31                         continue;
  32                 }
  33                 Edge carray[inputNum];
  34                 for(uint j=0; j<inputNum; j++){
  35                         Element* el = getArrayElement(inputs, j);
  36                         carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
  37                 }
  38                 constraints[i++]=constraintAND(This->cnf, inputNum, carray);
  39         }
  40         Edge result=constraintOR(This->cnf, size, constraints);
  41
  42         return generateNegation ? constraintNegate(result) : result;
  43 }
  44 Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
  45         //FIXME
  46         return E_NULL;
  47 }
  48
  49 void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder* This, ElementFunction* func){
  50         UndefinedBehavior undefStatus = ((FunctionTable*) func->function)->undefBehavior;
  51         ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
  52         ArrayElement* elements= &func->inputs;
  53         Table* table = ((FunctionTable*) (func->function))->table;
  54         uint size = getSizeHashSetTableEntry(table->entries);
  55         Edge constraints[size];
  56         HSIteratorTableEntry* iterator = iteratorTableEntry(table->entries);
  57         uint i=0;
  58         while(hasNextTableEntry(iterator)) {
  59                 TableEntry* entry = nextTableEntry(iterator);
  60                 ASSERT(entry!=NULL);
  61                 uint inputNum = getSizeArrayElement(elements);
  62                 Edge carray[inputNum];
  63                 for(uint j=0; j<inputNum; j++){
  64                         Element* el= getArrayElement(elements, j);
  65                         carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
  66                 }
  67                 Edge output = getElementValueConstraint(This, (Element*)func, entry->output);
  68                 Edge row;
  69                 switch(undefStatus ){
  70                         case IGNOREBEHAVIOR: {
  71                                 row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), output);
  72                                 break;
  73                         }
  74                         case FLAGFORCEUNDEFINED: {
  75                                 Edge undefConst = ((BooleanVar*)func->overflowstatus)->var;
  76                                 row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintAND2(This->cnf, output, constraintNegate(undefConst)));
  77                                 break;
  78                         }
  79                         default:
  80                                 ASSERT(0);
  81
  82                 }
  83                 constraints[i++]=row;
  84         }
  85         deleteIterTableEntry(iterator);
  86         addConstraintCNF(This->cnf, constraintAND(This->cnf, size, constraints));
  87 }
  88
  89 void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* elemFunc){
  90 #ifdef TRACE_DEBUG
  91         model_print("Enumeration Table functions ...\n");
  92 #endif
  93         ASSERT(GETFUNCTIONTYPE(elemFunc->function)==TABLEFUNC);
  94         //First encode children
  95         ArrayElement* elements= &elemFunc->inputs;
  96         for(uint i=0; i<getSizeArrayElement(elements); i++){
  97                 Element *elem = getArrayElement( elements, i);
  98                 encodeElementSATEncoder(This, elem);
  99         }
 100
 101         FunctionTable* function =(FunctionTable*)elemFunc;
 102         switch(function->undefBehavior){
 103                 case IGNOREBEHAVIOR:
 104                 case FLAGFORCEUNDEFINED:
 105                         return encodeEnumEntriesTableElemFuncSATEncoder(This, elemFunc);
 106                 default:
 107                         break;
 108         }
 109
 110         uint numDomains=getSizeArraySet(&function->table->domains);
 111
 112         VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses
 113
 114         uint indices[numDomains]; //setup indices
 115         bzero(indices, sizeof(uint)*numDomains);
 116
 117         uint64_t vals[numDomains]; //setup value array
 118         for(uint i=0;i<numDomains; i++) {
 119                 Set * set=getArraySet(&function->table->domains, i);
 120                 vals[i]=getSetElement(set, indices[i]);
 121         }
 122
 123         Edge undefConstraint = ((BooleanVar*) elemFunc->overflowstatus)->var;
 124
 125         bool notfinished=true;
 126         while(notfinished) {
 127                 Edge carray[numDomains+1];
 128                 TableEntry* tableEntry = getTableEntryFromTable(function->table, vals, numDomains);
 129                 bool isInRange = tableEntry!=NULL;
 130                 bool needClause = isInRange;
 131                 if (function->undefBehavior == UNDEFINEDSETSFLAG || function->undefBehavior == FLAGIFFUNDEFINED) {
 132                         needClause=true;
 133                 }
 134
 135                 if (needClause) {
 136                         //Include this in the set of terms
 137                         for(uint i=0;i<numDomains;i++) {
 138                                 Element * elem = getArrayElement(&elemFunc->inputs, i);
 139                                 carray[i] = getElementValueConstraint(This, elem, vals[i]);
 140                         }
 141                         if (isInRange) {
 142                                 carray[numDomains] = getElementValueConstraint(This, (Element*)elemFunc, tableEntry->output);
 143                         }
 144
 145                         Edge clause;
 146                         switch(function->undefBehavior) {
 147                                 case UNDEFINEDSETSFLAG: {
 148                                         if (isInRange) {
 149                                                 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
 150                                         } else {
 151                                                 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
 152                                         }
 153                                         break;
 154                                 }
 155                                 case FLAGIFFUNDEFINED: {
 156                                         if (isInRange) {
 157                                                 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(undefConstraint)));
 158                                         } else {
 159                                                 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
 160                                         }
 161                                         break;
 162                                 }
 163                                 default:
 164                                         ASSERT(0);
 165                         }
 166 #ifdef TRACE_DEBUG
 167                         model_print("added clause in table enumeration ...\n");
 168                         printCNF(clause);
 169                         model_print("\n");
 170 #endif
 171                         pushVectorEdge(clauses, clause);
 172                 }
 173
 174                 notfinished=false;
 175                 for(uint i=0;i<numDomains; i++) {
 176                         uint index=++indices[i];
 177                         Set * set=getArraySet(&function->table->domains, i);
 178
 179                         if (index < getSetSize(set)) {
 180                                 vals[i]=getSetElement(set, index);
 181                                 notfinished=true;
 182                                 break;
 183                         } else {
 184                                 indices[i]=0;
 185                                 vals[i]=getSetElement(set, 0);
 186                         }
 187                 }
 188         }
 189
 190         Edge cor=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
 191         addConstraintCNF(This->cnf, cor);
 192         deleteVectorEdge(clauses);
 193
 194 }