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         if(getSizeVectorEdge(clauses) == 0){
 151                 deleteVectorEdge(clauses);
 152                 return E_False;
 153         }
 154         Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
 155         deleteVectorEdge(clauses);
 156         return generateNegation ? constraintNegate(cor) : cor;
 157 }
 158
 159 void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder* This, ElementFunction* func){
 160         UndefinedBehavior undefStatus = ((FunctionTable*) func->function)->undefBehavior;
 161         ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
 162         ArrayElement* elements= &func->inputs;
 163         Table* table = ((FunctionTable*) (func->function))->table;
 164         uint size = getSizeHashSetTableEntry(table->entries);
 165         Edge constraints[size];
 166         HSIteratorTableEntry* iterator = iteratorTableEntry(table->entries);
 167         uint i=0;
 168         while(hasNextTableEntry(iterator)) {
 169                 TableEntry* entry = nextTableEntry(iterator);
 170                 ASSERT(entry!=NULL);
 171                 uint inputNum = getSizeArrayElement(elements);
 172                 Edge carray[inputNum];
 173                 for(uint j=0; j<inputNum; j++){
 174                         Element* el= getArrayElement(elements, j);
 175                         carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
 176                 }
 177                 Edge output = getElementValueConstraint(This, (Element*)func, entry->output);
 178                 Edge row;
 179                 switch(undefStatus ){
 180                         case IGNOREBEHAVIOR: {
 181                                 row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), output);
 182                                 break;
 183                         }
 184                         case FLAGFORCEUNDEFINED: {
 185                                 Edge undefConst = encodeConstraintSATEncoder(This, func->overflowstatus);
 186                                 row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintAND2(This->cnf, output, constraintNegate(undefConst)));
 187                                 break;
 188                         }
 189                         default:
 190                                 ASSERT(0);
 191
 192                 }
 193                 constraints[i++]=row;
 194         }
 195         deleteIterTableEntry(iterator);
 196         addConstraintCNF(This->cnf, constraintAND(This->cnf, size, constraints));
 197 }
 198
 199 void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* elemFunc){
 200 #ifdef TRACE_DEBUG
 201         model_print("Enumeration Table functions ...\n");
 202 #endif
 203         ASSERT(GETFUNCTIONTYPE(elemFunc->function)==TABLEFUNC);
 204         //First encode children
 205         ArrayElement* elements= &elemFunc->inputs;
 206         for(uint i=0; i<getSizeArrayElement(elements); i++){
 207                 Element *elem = getArrayElement( elements, i);
 208                 encodeElementSATEncoder(This, elem);
 209         }
 210
 211         FunctionTable* function =(FunctionTable*)elemFunc->function;
 212         switch(function->undefBehavior){
 213                 case IGNOREBEHAVIOR:
 214                 case FLAGFORCEUNDEFINED:
 215                         return encodeEnumEntriesTableElemFuncSATEncoder(This, elemFunc);
 216                 default:
 217                         break;
 218         }
 219
 220         uint numDomains=getSizeArraySet(&function->table->domains);
 221
 222         VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses
 223
 224         uint indices[numDomains]; //setup indices
 225         bzero(indices, sizeof(uint)*numDomains);
 226
 227         uint64_t vals[numDomains]; //setup value array
 228         for(uint i=0;i<numDomains; i++) {
 229                 Set * set=getArraySet(&function->table->domains, i);
 230                 vals[i]=getSetElement(set, indices[i]);
 231         }
 232
 233         Edge undefConstraint = encodeConstraintSATEncoder(This, elemFunc->overflowstatus);
 234         bool notfinished=true;
 235         while(notfinished) {
 236                 Edge carray[numDomains+1];
 237                 TableEntry* tableEntry = getTableEntryFromTable(function->table, vals, numDomains);
 238                 bool isInRange = tableEntry!=NULL;
 239                 ASSERT(function->undefBehavior == UNDEFINEDSETSFLAG || function->undefBehavior == FLAGIFFUNDEFINED);
 240                 //Include this in the set of terms
 241                 for(uint i=0;i<numDomains;i++) {
 242                         Element * elem = getArrayElement(&elemFunc->inputs, i);
 243                         carray[i] = getElementValueConstraint(This, elem, vals[i]);
 244                 }
 245                 if (isInRange) {
 246                         carray[numDomains] = getElementValueConstraint(This, (Element*)elemFunc, tableEntry->output);
 247                 }
 248
 249                 Edge clause;
 250                 switch(function->undefBehavior) {
 251                         case UNDEFINEDSETSFLAG: {
 252                                 if (isInRange) {
 253                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
 254                                 } else {
 255                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
 256                                 }
 257                                 break;
 258                         }
 259                         case FLAGIFFUNDEFINED: {
 260                                 if (isInRange) {
 261                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(undefConstraint)));
 262                                 } else {
 263                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
 264                                 }
 265                                 break;
 266                         }
 267                         default:
 268                                 ASSERT(0);
 269                 }
 270 #ifdef TRACE_DEBUG
 271                 model_print("added clause in function table enumeration ...\n");
 272                 printCNF(clause);
 273                 model_print("\n");
 274 #endif
 275                 pushVectorEdge(clauses, clause);
 276
 277
 278                 notfinished=false;
 279                 for(uint i=0;i<numDomains; i++) {
 280                         uint index=++indices[i];
 281                         Set * set=getArraySet(&function->table->domains, i);
 282
 283                         if (index < getSetSize(set)) {
 284                                 vals[i]=getSetElement(set, index);
 285                                 notfinished=true;
 286                                 break;
 287                         } else {
 288                                 indices[i]=0;
 289                                 vals[i]=getSetElement(set, 0);
 290                         }
 291                 }
 292         }
 293         if(getSizeVectorEdge(clauses) == 0){
 294                 deleteVectorEdge(clauses);
 295                 return;
 296         }
 297         Edge cor=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
 298         addConstraintCNF(This->cnf, cor);
 299         deleteVectorEdge(clauses);
 300
 301 }