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 = predicate->table->numDomains();
  96
  97         if (generateNegation)
  98                 polarity = negatePolarity(polarity);
  99
 100         VectorEdge *clauses = allocDefVectorEdge();
 101
 102         uint indices[numDomains];       //setup indices
 103         bzero(indices, sizeof(uint) * numDomains);
 104
 105         uint64_t vals[numDomains];//setup value array
 106         for (uint i = 0; i < numDomains; i++) {
 107                 Set *set = predicate->table->getDomain(i);
 108                 vals[i] = set->getElement(indices[i]);
 109         }
 110         bool hasOverflow = false;
 111
 112         bool notfinished = true;
 113         while (notfinished) {
 114                 Edge carray[numDomains];
 115                 TableEntry *tableEntry = predicate->table->getTableEntry(vals, numDomains);
 116                 bool isInRange = tableEntry != NULL;
 117                 if (!isInRange && !hasOverflow) {
 118                         hasOverflow = true;
 119                 }
 120                 Edge clause;
 121                 for (uint i = 0; i < numDomains; i++) {
 122                         Element *elem = constraint->inputs.get(i);
 123                         carray[i] = getElementValueConstraint(elem, polarity, vals[i]);
 124                 }
 125
 126                 switch (predicate->undefinedbehavior) {
 127                 case SATC_UNDEFINEDSETSFLAG:
 128                         if (isInRange) {
 129                                 clause = constraintAND(cnf, numDomains, carray);
 130                         } else {
 131                                 Edge undefConstraint = encodeConstraintSATEncoder(constraint->undefStatus);
 132                                 addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), undefConstraint) );
 133                         }
 134                         break;
 135                 case SATC_FLAGIFFUNDEFINED: {
 136                         Edge undefConstraint = encodeConstraintSATEncoder(constraint->undefStatus);
 137                         if (isInRange) {
 138                                 clause = constraintAND(cnf, numDomains, carray);
 139                                 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintNegate(undefConstraint)));
 140                         } else {
 141                                 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint) );
 142                         }
 143                         break;
 144                 }
 145                 default:
 146                         ASSERT(0);
 147                 }
 148
 149                 if (isInRange) {
 150 #ifdef TRACE_DEBUG
 151                         model_print("added clause in predicate table enumeration ...\n");
 152                         printCNF(clause);
 153                         model_print("\n");
 154 #endif
 155                         pushVectorEdge(clauses, clause);
 156                 }
 157
 158                 notfinished = false;
 159                 for (uint i = 0; i < numDomains; i++) {
 160                         uint index = ++indices[i];
 161                         Set *set = predicate->table->getDomain(i);
 162
 163                         if (index < set->getSize()) {
 164                                 vals[i] = set->getElement(index);
 165                                 notfinished = true;
 166                                 break;
 167                         } else {
 168                                 indices[i] = 0;
 169                                 vals[i] = set->getElement(0);
 170                         }
 171                 }
 172         }
 173         Edge result = E_NULL;
 174         ASSERT(getSizeVectorEdge(clauses) != 0);
 175         result = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
 176         if (hasOverflow) {
 177                 Edge undefConstraint = encodeConstraintSATEncoder(constraint->undefStatus);
 178                 result = constraintOR2(cnf, result, undefConstraint);
 179         }
 180         if (generateNegation) {
 181                 ASSERT(!hasOverflow);
 182                 result = constraintNegate(result);
 183         }
 184         deleteVectorEdge(clauses);
 185         return result;
 186 }
 187
 188 void SATEncoder::encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *func) {
 189         UndefinedBehavior undefStatus = ((FunctionTable *) func->getFunction())->undefBehavior;
 190         ASSERT(undefStatus == SATC_IGNOREBEHAVIOR || undefStatus == SATC_FLAGFORCEUNDEFINED);
 191         Array<Element *> *elements = &func->inputs;
 192
 193         Table *table = ((FunctionTable *) (func->getFunction()))->table;
 194         uint size = table->getSize();
 195         Edge constraints[size];
 196         SetIteratorTableEntry *iterator = table->getEntries();
 197         uint i = 0;
 198         while (iterator->hasNext()) {
 199                 TableEntry *entry = iterator->next();
 200                 ASSERT(entry != NULL);
 201                 uint inputNum = elements->getSize();
 202                 Edge carray[inputNum];
 203                 for (uint j = 0; j < inputNum; j++) {
 204                         Element *el = elements->get(j);
 205                         carray[j] = getElementValueConstraint(el, P_FALSE, entry->inputs[j]);
 206                 }
 207                 Edge output = getElementValueConstraint(func, P_TRUE, entry->output);
 208                 switch (undefStatus ) {
 209                 case SATC_IGNOREBEHAVIOR: {
 210                         addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, inputNum, carray), output));
 211                         break;
 212                 }
 213                 case SATC_FLAGFORCEUNDEFINED: {
 214                         Edge undefConst = encodeConstraintSATEncoder(func->overflowstatus);
 215                         addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintAND2(cnf, output, constraintNegate(undefConst))));
 216                         break;
 217                 }
 218                 default:
 219                         ASSERT(0);
 220
 221                 }
 222         }
 223         delete iterator;
 224 }
 225
 226 void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc) {
 227 #ifdef TRACE_DEBUG
 228         model_print("Enumeration Table functions ...\n");
 229 #endif
 230         ASSERT(elemFunc->getFunction()->type == TABLEFUNC);
 231
 232         //First encode children
 233         Array<Element *> *elements = &elemFunc->inputs;
 234         for (uint i = 0; i < elements->getSize(); i++) {
 235                 Element *elem = elements->get(i);
 236                 encodeElementSATEncoder(elem);
 237         }
 238
 239         FunctionTable *function = (FunctionTable *)elemFunc->getFunction();
 240         switch (function->undefBehavior) {
 241         case SATC_IGNOREBEHAVIOR:
 242         case SATC_FLAGFORCEUNDEFINED:
 243                 return encodeEnumEntriesTableElemFuncSATEncoder(elemFunc);
 244         default:
 245                 break;
 246         }
 247
 248         uint numDomains = function->table->numDomains();
 249
 250         uint indices[numDomains];       //setup indices
 251         bzero(indices, sizeof(uint) * numDomains);
 252
 253         uint64_t vals[numDomains];//setup value array
 254         for (uint i = 0; i < numDomains; i++) {
 255                 Set *set = function->table->getDomain(i);
 256                 vals[i] = set->getElement(indices[i]);
 257         }
 258
 259         bool notfinished = true;
 260         while (notfinished) {
 261                 Edge carray[numDomains + 1];
 262                 TableEntry *tableEntry = function->table->getTableEntry(vals, numDomains);
 263                 bool isInRange = tableEntry != NULL;
 264                 ASSERT(function->undefBehavior == SATC_UNDEFINEDSETSFLAG || function->undefBehavior == SATC_FLAGIFFUNDEFINED);
 265                 for (uint i = 0; i < numDomains; i++) {
 266                         Element *elem = elemFunc->inputs.get(i);
 267                         carray[i] = getElementValueConstraint(elem, P_FALSE, vals[i]);
 268                 }
 269                 if (isInRange) {
 270                         carray[numDomains] = getElementValueConstraint(elemFunc, P_TRUE, tableEntry->output);
 271                 }
 272
 273                 switch (function->undefBehavior) {
 274                 case SATC_UNDEFINEDSETSFLAG: {
 275                         if (isInRange) {
 276                                 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]));
 277                         } else {
 278                                 Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus);
 279                                 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
 280                         }
 281                         break;
 282                 }
 283                 case SATC_FLAGIFFUNDEFINED: {
 284                         Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus);
 285                         if (isInRange) {
 286                                 Edge freshvar = constraintNewVar(cnf);
 287                                 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), freshvar ));
 288                                 addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, constraintNegate(undefConstraint) ));
 289                                 addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, carray[numDomains]));
 290                         } else {
 291                                 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
 292                         }
 293                         break;
 294                 }
 295                 default:
 296                         ASSERT(0);
 297                 }
 298                 if (isInRange) {
 299 #ifdef TRACE_DEBUG
 300                         model_print("added clause in function table enumeration ...\n");
 301                         printCNF(clause);
 302                         model_print("\n");
 303 #endif
 304                 }
 305
 306                 notfinished = false;
 307                 for (uint i = 0; i < numDomains; i++) {
 308                         uint index = ++indices[i];
 309                         Set *set = function->table->getDomain(i);
 310
 311                         if (index < set->getSize()) {
 312                                 vals[i] = set->getElement(index);
 313                                 notfinished = true;
 314                                 break;
 315                         } else {
 316                                 indices[i] = 0;
 317                                 vals[i] = set->getElement(0);
 318                         }
 319                 }
 320         }
 321 }