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