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