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