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         printCNF(undefConstraint);
  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                 if(isInRange && generateNegation == tableEntry->output)
  99                         goto NEXT;
 100                 Edge clause;
 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                 switch(predicate->undefinedbehavior) {
 107                         case UNDEFINEDSETSFLAG:
 108                                 if(isInRange){
 109                                         clause=constraintAND(This->cnf, numDomains, carray);
 110                                 }else{
 111                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
 112                                 }
 113                                 break;
 114                         case FLAGIFFUNDEFINED:
 115                                 if(isInRange){
 116                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintNegate(undefConstraint));
 117                                 }else{
 118                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
 119                                 }
 120                                 break;
 121
 122                         default:
 123                                 ASSERT(0);
 124                 }
 125 #ifdef TRACE_DEBUG
 126                 model_print("added clause in predicate table enumeration ...\n");
 127                 printCNF(clause);
 128                 model_print("\n");
 129 #endif
 130                 pushVectorEdge(clauses, clause);
 131 NEXT:
 132                 notfinished=false;
 133                 for(uint i=0;i<numDomains; i++) {
 134                         uint index=++indices[i];
 135                         Set * set=getArraySet(&predicate->table->domains, i);
 136
 137                         if (index < getSetSize(set)) {
 138                                 vals[i]=getSetElement(set, index);
 139                                 notfinished=true;
 140                                 break;
 141                         } else {
 142                                 indices[i]=0;
 143                                 vals[i]=getSetElement(set, 0);
 144                         }
 145                 }
 146         }
 147         if(getSizeVectorEdge(clauses) == 0){
 148                 deleteVectorEdge(clauses);
 149                 return E_False;
 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                 for(uint i=0;i<numDomains;i++) {
 238                         Element * elem = getArrayElement(&elemFunc->inputs, i);
 239                         carray[i] = getElementValueConstraint(This, elem, vals[i]);
 240                 }
 241                 if (isInRange) {
 242                         carray[numDomains] = getElementValueConstraint(This, (Element*)elemFunc, tableEntry->output);
 243                 }
 244
 245                 Edge clause;
 246                 switch(function->undefBehavior) {
 247                         case UNDEFINEDSETSFLAG: {
 248                                 if (isInRange) {
 249                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
 250                                 } else {
 251                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
 252                                 }
 253                                 break;
 254                         }
 255                         case FLAGIFFUNDEFINED: {
 256                                 if (isInRange) {
 257                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(undefConstraint)));
 258                                 } else {
 259                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
 260                                 }
 261                                 break;
 262                         }
 263                         default:
 264                                 ASSERT(0);
 265                 }
 266 #ifdef TRACE_DEBUG
 267                 model_print("added clause in function table enumeration ...\n");
 268                 printCNF(clause);
 269                 model_print("\n");
 270 #endif
 271                 pushVectorEdge(clauses, clause);
 272
 273
 274                 notfinished=false;
 275                 for(uint i=0;i<numDomains; i++) {
 276                         uint index=++indices[i];
 277                         Set * set=getArraySet(&function->table->domains, i);
 278
 279                         if (index < getSetSize(set)) {
 280                                 vals[i]=getSetElement(set, index);
 281                                 notfinished=true;
 282                                 break;
 283                         } else {
 284                                 indices[i]=0;
 285                                 vals[i]=getSetElement(set, 0);
 286                         }
 287                 }
 288         }
 289         if(getSizeVectorEdge(clauses) == 0){
 290                 deleteVectorEdge(clauses);
 291                 return;
 292         }
 293         Edge cor=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
 294         addConstraintCNF(This->cnf, cor);
 295         deleteVectorEdge(clauses);
 296
 297 }