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