src/Backend/satfunctableencoder.cc

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