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         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 = predicate->table->getDomain(i);
 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 = predicate->table->getDomain(i);
 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                         addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, inputNum, carray), output));
 212                         break;
 213                 }
 214                 case SATC_FLAGFORCEUNDEFINED: {
 215                         Edge undefConst = encodeConstraintSATEncoder(func->overflowstatus);
 216                         addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintAND2(cnf, output, constraintNegate(undefConst))));
 217                         break;
 218                 }
 219                 default:
 220                         ASSERT(0);
 221
 222                 }
 223         }
 224         delete iterator;
 225 }
 226
 227 void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc) {
 228 #ifdef TRACE_DEBUG
 229         model_print("Enumeration Table functions ...\n");
 230 #endif
 231         ASSERT(elemFunc->getFunction()->type == TABLEFUNC);
 232
 233         //First encode children
 234         Array<Element *> *elements = &elemFunc->inputs;
 235         for (uint i = 0; i < elements->getSize(); i++) {
 236                 Element *elem = elements->get(i);
 237                 encodeElementSATEncoder(elem);
 238         }
 239
 240         FunctionTable *function = (FunctionTable *)elemFunc->getFunction();
 241         switch (function->undefBehavior) {
 242         case SATC_IGNOREBEHAVIOR:
 243         case SATC_FLAGFORCEUNDEFINED:
 244                 return encodeEnumEntriesTableElemFuncSATEncoder(elemFunc);
 245         default:
 246                 break;
 247         }
 248
 249         uint numDomains = function->table->numDomains();
 250
 251         uint indices[numDomains];       //setup indices
 252         bzero(indices, sizeof(uint) * numDomains);
 253
 254         uint64_t vals[numDomains];//setup value array
 255         for (uint i = 0; i < numDomains; i++) {
 256                 Set *set = function->table->getDomain(i);
 257                 vals[i] = set->getElement(indices[i]);
 258         }
 259
 260         bool notfinished = true;
 261         while (notfinished) {
 262                 Edge carray[numDomains + 1];
 263                 TableEntry *tableEntry = function->table->getTableEntry(vals, numDomains);
 264                 bool isInRange = tableEntry != NULL;
 265                 ASSERT(function->undefBehavior == SATC_UNDEFINEDSETSFLAG || function->undefBehavior == SATC_FLAGIFFUNDEFINED);
 266                 for (uint i = 0; i < numDomains; i++) {
 267                         Element *elem = elemFunc->inputs.get(i);
 268                         carray[i] = getElementValueConstraint(elem, P_FALSE, vals[i]);
 269                 }
 270                 if (isInRange) {
 271                         carray[numDomains] = getElementValueConstraint(elemFunc, P_TRUE, tableEntry->output);
 272                 }
 273
 274                 switch (function->undefBehavior) {
 275                 case SATC_UNDEFINEDSETSFLAG: {
 276                         if (isInRange) {
 277                                 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]));
 278                         } else {
 279                                 Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus);
 280                                 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
 281                         }
 282                         break;
 283                 }
 284                 case SATC_FLAGIFFUNDEFINED: {
 285                         Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus);
 286                         if (isInRange) {
 287                                 Edge freshvar = constraintNewVar(cnf);
 288                                 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), freshvar ));
 289                                 addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, constraintNegate(undefConstraint) ));
 290                                 addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, carray[numDomains]));
 291                         } else {
 292                                 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
 293                         }
 294                         break;
 295                 }
 296                 default:
 297                         ASSERT(0);
 298                 }
 299                 if (isInRange) {
 300 #ifdef TRACE_DEBUG
 301                         model_print("added clause in function table enumeration ...\n");
 302                         printCNF(clause);
 303                         model_print("\n");
 304 #endif
 305                 }
 306
 307                 notfinished = false;
 308                 for (uint i = 0; i < numDomains; i++) {
 309                         uint index = ++indices[i];
 310                         Set *set = function->table->getDomain(i);
 311
 312                         if (index < set->getSize()) {
 313                                 vals[i] = set->getElement(index);
 314                                 notfinished = true;
 315                                 break;
 316                         } else {
 317                                 indices[i] = 0;
 318                                 vals[i] = set->getElement(0);
 319                         }
 320                 }
 321         }
 322 }