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         ASSERT(GETPREDICATETYPE(constraint->predicate) == TABLEPRED);
  15         UndefinedBehavior undefStatus = ((PredicateTable*)constraint->predicate)->undefinedbehavior;
  16         ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
  17         Table* table = ((PredicateTable*)constraint->predicate)->table;
  18         FunctionEncodingType encType = constraint->encoding.type;
  19         ArrayElement* inputs = &constraint->inputs;
  20         uint inputNum =getSizeArrayElement(inputs);
  21         uint size = getSizeHashSetTableEntry(table->entries);
  22         bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
  23         Edge constraints[size];
  24         HSIteratorTableEntry* iterator = iteratorTableEntry(table->entries);
  25         uint i=0;
  26         while(hasNextTableEntry(iterator)){
  27                 TableEntry* entry = nextTableEntry(iterator);
  28                 if(generateNegation == entry->output) {
  29                         //Skip the irrelevant entries
  30                         continue;
  31                 }
  32                 Edge carray[inputNum];
  33                 for(uint j=0; j<inputNum; j++){
  34                         Element* el = getArrayElement(inputs, j);
  35                         carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
  36                 }
  37                 Edge row;
  38                 switch(undefStatus){
  39                         case IGNOREBEHAVIOR:
  40                                 row=constraintAND(This->cnf, inputNum, carray);
  41                                 break;
  42                         case FLAGFORCEUNDEFINED:{
  43                                 Edge undefConst = ((BooleanVar*)constraint->undefStatus)->var;
  44                                 row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray),  constraintNegate(undefConst));
  45                                 break;
  46                         }
  47                         default:
  48                                 ASSERT(0);
  49                 }
  50                 constraints[i++] = row;
  51
  52         }
  53         Edge result=constraintOR(This->cnf, size, constraints);
  54
  55         return generateNegation ? constraintNegate(result) : result;
  56 }
  57 Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
  58 #ifdef TRACE_DEBUG
  59         model_print("Enumeration Table Predicate ...\n");
  60 #endif
  61         ASSERT(GETPREDICATETYPE(constraint->predicate) == TABLEPRED);
  62         //First encode children
  63         ArrayElement* inputs = &constraint->inputs;
  64         uint inputNum =getSizeArrayElement(inputs);
  65         //Encode all the inputs first ...
  66         for(uint i=0; i<inputNum; i++){
  67                 encodeElementSATEncoder(This, getArrayElement(inputs, i));
  68         }
  69         PredicateTable* predicate = (PredicateTable*)constraint->predicate;
  70         switch(predicate->undefinedbehavior){
  71                 case IGNOREBEHAVIOR:
  72                 case FLAGFORCEUNDEFINED:
  73                         return encodeEnumEntriesTablePredicateSATEncoder(This, constraint);
  74                 default:
  75                         break;
  76         }
  77         bool generateNegation = constraint->encoding.type == ENUMERATEIMPLICATIONSNEGATE;
  78         uint numDomains=getSizeArraySet(&predicate->table->domains);
  79
  80         VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses
  81
  82         uint indices[numDomains]; //setup indices
  83         bzero(indices, sizeof(uint)*numDomains);
  84
  85         uint64_t vals[numDomains]; //setup value array
  86         for(uint i=0;i<numDomains; i++) {
  87                 Set * set=getArraySet(&predicate->table->domains, i);
  88                 vals[i]=getSetElement(set, indices[i]);
  89         }
  90
  91         Edge undefConstraint = ((BooleanVar*) constraint->undefStatus)->var;
  92
  93         bool notfinished=true;
  94         while(notfinished) {
  95                 Edge carray[numDomains];
  96                 TableEntry* tableEntry = getTableEntryFromTable(predicate->table, vals, numDomains);
  97                 bool isInRange = tableEntry!=NULL;
  98                 bool ignoreEntry = generateNegation == tableEntry->output;
  99                 ASSERT(predicate->undefinedbehavior == UNDEFINEDSETSFLAG || predicate->undefinedbehavior == FLAGIFFUNDEFINED);
 100                 //Include this in the set of terms
 101                 for(uint i=0;i<numDomains;i++) {
 102                         Element * elem = getArrayElement(&constraint->inputs, i);
 103                         carray[i] = getElementValueConstraint(This, elem, vals[i]);
 104                 }
 105
 106                 Edge clause;
 107                 switch(predicate->undefinedbehavior) {
 108                         case UNDEFINEDSETSFLAG: {
 109                                 if (isInRange && !ignoreEntry) {
 110                                         clause=constraintAND(This->cnf, numDomains, carray);
 111                                 } else if(!isInRange) {
 112                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
 113                                 }
 114                                 break;
 115                         }
 116                         case FLAGIFFUNDEFINED: {
 117                                 if (isInRange && !ignoreEntry) {
 118                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(undefConstraint)));
 119                                 } else if(!isInRange) {
 120                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
 121                                 }
 122                                 break;
 123                         }
 124                         default:
 125                                 ASSERT(0);
 126                 }
 127 #ifdef TRACE_DEBUG
 128                 model_print("added clause in predicate table enumeration ...\n");
 129                 printCNF(clause);
 130                 model_print("\n");
 131 #endif
 132                 pushVectorEdge(clauses, clause);
 133
 134
 135                 notfinished=false;
 136                 for(uint i=0;i<numDomains; i++) {
 137                         uint index=++indices[i];
 138                         Set * set=getArraySet(&predicate->table->domains, i);
 139
 140                         if (index < getSetSize(set)) {
 141                                 vals[i]=getSetElement(set, index);
 142                                 notfinished=true;
 143                                 break;
 144                         } else {
 145                                 indices[i]=0;
 146                                 vals[i]=getSetElement(set, 0);
 147                         }
 148                 }
 149         }
 150
 151         Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
 152         deleteVectorEdge(clauses);
 153         return generateNegation ? constraintNegate(cor) : cor;
 154 }
 155
 156 void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder* This, ElementFunction* func){
 157         UndefinedBehavior undefStatus = ((FunctionTable*) func->function)->undefBehavior;
 158         ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
 159         ArrayElement* elements= &func->inputs;
 160         Table* table = ((FunctionTable*) (func->function))->table;
 161         uint size = getSizeHashSetTableEntry(table->entries);
 162         Edge constraints[size];
 163         HSIteratorTableEntry* iterator = iteratorTableEntry(table->entries);
 164         uint i=0;
 165         while(hasNextTableEntry(iterator)) {
 166                 TableEntry* entry = nextTableEntry(iterator);
 167                 ASSERT(entry!=NULL);
 168                 uint inputNum = getSizeArrayElement(elements);
 169                 Edge carray[inputNum];
 170                 for(uint j=0; j<inputNum; j++){
 171                         Element* el= getArrayElement(elements, j);
 172                         carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
 173                 }
 174                 Edge output = getElementValueConstraint(This, (Element*)func, entry->output);
 175                 Edge row;
 176                 switch(undefStatus ){
 177                         case IGNOREBEHAVIOR: {
 178                                 row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), output);
 179                                 break;
 180                         }
 181                         case FLAGFORCEUNDEFINED: {
 182                                 Edge undefConst = ((BooleanVar*)func->overflowstatus)->var;
 183                                 row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintAND2(This->cnf, output, constraintNegate(undefConst)));
 184                                 break;
 185                         }
 186                         default:
 187                                 ASSERT(0);
 188
 189                 }
 190                 constraints[i++]=row;
 191         }
 192         deleteIterTableEntry(iterator);
 193         addConstraintCNF(This->cnf, constraintAND(This->cnf, size, constraints));
 194 }
 195
 196 void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* elemFunc){
 197 #ifdef TRACE_DEBUG
 198         model_print("Enumeration Table functions ...\n");
 199 #endif
 200         ASSERT(GETFUNCTIONTYPE(elemFunc->function)==TABLEFUNC);
 201         //First encode children
 202         ArrayElement* elements= &elemFunc->inputs;
 203         for(uint i=0; i<getSizeArrayElement(elements); i++){
 204                 Element *elem = getArrayElement( elements, i);
 205                 encodeElementSATEncoder(This, elem);
 206         }
 207
 208         FunctionTable* function =(FunctionTable*)elemFunc->function;
 209         model_print("undefBehavior: %d\n", function->undefBehavior);
 210         switch(function->undefBehavior){
 211                 case IGNOREBEHAVIOR:
 212                 case FLAGFORCEUNDEFINED:
 213                         return encodeEnumEntriesTableElemFuncSATEncoder(This, elemFunc);
 214                 default:
 215                         break;
 216         }
 217
 218         uint numDomains=getSizeArraySet(&function->table->domains);
 219
 220         VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses
 221
 222         uint indices[numDomains]; //setup indices
 223         bzero(indices, sizeof(uint)*numDomains);
 224
 225         uint64_t vals[numDomains]; //setup value array
 226         for(uint i=0;i<numDomains; i++) {
 227                 Set * set=getArraySet(&function->table->domains, i);
 228                 vals[i]=getSetElement(set, indices[i]);
 229         }
 230
 231         Edge undefConstraint = ((BooleanVar*) elemFunc->overflowstatus)->var;
 232
 233         bool notfinished=true;
 234         while(notfinished) {
 235                 Edge carray[numDomains+1];
 236                 TableEntry* tableEntry = getTableEntryFromTable(function->table, vals, numDomains);
 237                 bool isInRange = tableEntry!=NULL;
 238                 ASSERT(function->undefBehavior == UNDEFINEDSETSFLAG || function->undefBehavior == FLAGIFFUNDEFINED);
 239                 //Include this in the set of terms
 240                 for(uint i=0;i<numDomains;i++) {
 241                         Element * elem = getArrayElement(&elemFunc->inputs, i);
 242                         carray[i] = getElementValueConstraint(This, elem, vals[i]);
 243                 }
 244                 if (isInRange) {
 245                         carray[numDomains] = getElementValueConstraint(This, (Element*)elemFunc, tableEntry->output);
 246                 }
 247
 248                 Edge clause;
 249                 switch(function->undefBehavior) {
 250                         case UNDEFINEDSETSFLAG: {
 251                                 if (isInRange) {
 252                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
 253                                 } else {
 254                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
 255                                 }
 256                                 break;
 257                         }
 258                         case FLAGIFFUNDEFINED: {
 259                                 if (isInRange) {
 260                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(undefConstraint)));
 261                                 } else {
 262                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
 263                                 }
 264                                 break;
 265                         }
 266                         default:
 267                                 ASSERT(0);
 268                 }
 269 #ifdef TRACE_DEBUG
 270                 model_print("added clause in function table enumeration ...\n");
 271                 printCNF(clause);
 272                 model_print("\n");
 273 #endif
 274                 pushVectorEdge(clauses, clause);
 275
 276
 277                 notfinished=false;
 278                 for(uint i=0;i<numDomains; i++) {
 279                         uint index=++indices[i];
 280                         Set * set=getArraySet(&function->table->domains, i);
 281
 282                         if (index < getSetSize(set)) {
 283                                 vals[i]=getSetElement(set, index);
 284                                 notfinished=true;
 285                                 break;
 286                         } else {
 287                                 indices[i]=0;
 288                                 vals[i]=getSetElement(set, 0);
 289                         }
 290                 }
 291         }
 292
 293         Edge cor=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
 294         addConstraintCNF(This->cnf, cor);
 295         deleteVectorEdge(clauses);
 296
 297 }