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 = encodeConstraintSATEncoder(This, constraint->undefStatus);
  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 = encodeConstraintSATEncoder (This, constraint->undefStatus);
  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 = encodeConstraintSATEncoder(This, func->overflowstatus);
 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         switch(function->undefBehavior){
 210                 case IGNOREBEHAVIOR:
 211                 case FLAGFORCEUNDEFINED:
 212                         return encodeEnumEntriesTableElemFuncSATEncoder(This, elemFunc);
 213                 default:
 214                         break;
 215         }
 216
 217         uint numDomains=getSizeArraySet(&function->table->domains);
 218
 219         VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses
 220
 221         uint indices[numDomains]; //setup indices
 222         bzero(indices, sizeof(uint)*numDomains);
 223
 224         uint64_t vals[numDomains]; //setup value array
 225         for(uint i=0;i<numDomains; i++) {
 226                 Set * set=getArraySet(&function->table->domains, i);
 227                 vals[i]=getSetElement(set, indices[i]);
 228         }
 229
 230         Edge undefConstraint = encodeConstraintSATEncoder(This, elemFunc->overflowstatus);
 231         bool notfinished=true;
 232         while(notfinished) {
 233                 Edge carray[numDomains+1];
 234                 TableEntry* tableEntry = getTableEntryFromTable(function->table, vals, numDomains);
 235                 bool isInRange = tableEntry!=NULL;
 236                 ASSERT(function->undefBehavior == UNDEFINEDSETSFLAG || function->undefBehavior == FLAGIFFUNDEFINED);
 237                 //Include this in the set of terms
 238                 for(uint i=0;i<numDomains;i++) {
 239                         Element * elem = getArrayElement(&elemFunc->inputs, i);
 240                         carray[i] = getElementValueConstraint(This, elem, vals[i]);
 241                 }
 242                 if (isInRange) {
 243                         carray[numDomains] = getElementValueConstraint(This, (Element*)elemFunc, tableEntry->output);
 244                 }
 245
 246                 Edge clause;
 247                 switch(function->undefBehavior) {
 248                         case UNDEFINEDSETSFLAG: {
 249                                 if (isInRange) {
 250                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
 251                                 } else {
 252                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
 253                                 }
 254                                 break;
 255                         }
 256                         case FLAGIFFUNDEFINED: {
 257                                 if (isInRange) {
 258                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(undefConstraint)));
 259                                 } else {
 260                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
 261                                 }
 262                                 break;
 263                         }
 264                         default:
 265                                 ASSERT(0);
 266                 }
 267 #ifdef TRACE_DEBUG
 268                 model_print("added clause in function table enumeration ...\n");
 269                 printCNF(clause);
 270                 model_print("\n");
 271 #endif
 272                 pushVectorEdge(clauses, clause);
 273
 274
 275                 notfinished=false;
 276                 for(uint i=0;i<numDomains; i++) {
 277                         uint index=++indices[i];
 278                         Set * set=getArraySet(&function->table->domains, i);
 279
 280                         if (index < getSetSize(set)) {
 281                                 vals[i]=getSetElement(set, index);
 282                                 notfinished=true;
 283                                 break;
 284                         } else {
 285                                 indices[i]=0;
 286                                 vals[i]=getSetElement(set, 0);
 287                         }
 288                 }
 289         }
 290
 291         Edge cor=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
 292         addConstraintCNF(This->cnf, cor);
 293         deleteVectorEdge(clauses);
 294
 295 }