src/Backend/satfuncopencoder.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::encodeOperatorPredicateSATEncoder(BooleanPredicate *constraint) {
  14         switch (constraint->encoding.type) {
  15         case ENUMERATEIMPLICATIONS:
  16                 return encodeEnumOperatorPredicateSATEncoder(constraint);
  17         case CIRCUIT:
  18                 return encodeCircuitOperatorPredicateEncoder(constraint);
  19         default:
  20                 ASSERT(0);
  21         }
  22         exit(-1);
  23 }
  24
  25 Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constraint) {
  26         PredicateOperator *predicate = (PredicateOperator *)constraint->predicate;
  27         uint numDomains = predicate->domains.getSize();
  28         Polarity polarity = constraint->polarity;
  29         FunctionEncodingType encType = constraint->encoding.type;
  30         bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
  31         if (generateNegation)
  32                 polarity = negatePolarity(polarity);
  33
  34         /* Call base encoders for children */
  35         for (uint i = 0; i < numDomains; i++) {
  36                 Element *elem = constraint->inputs.get(i);
  37                 encodeElementSATEncoder(elem);
  38         }
  39         VectorEdge *clauses = vector;
  40
  41         uint indices[numDomains];       //setup indices
  42         bzero(indices, sizeof(uint) * numDomains);
  43
  44         uint64_t vals[numDomains];//setup value array
  45         for (uint i = 0; i < numDomains; i++) {
  46                 Set *set = predicate->domains.get(i);
  47                 vals[i] = set->getElement(indices[i]);
  48         }
  49
  50         bool notfinished = true;
  51         while (notfinished) {
  52                 Edge carray[numDomains];
  53
  54                 if (predicate->evalPredicateOperator(vals) != generateNegation) {
  55                         //Include this in the set of terms
  56                         for (uint i = 0; i < numDomains; i++) {
  57                                 Element *elem = constraint->inputs.get(i);
  58                                 carray[i] = getElementValueConstraint(elem, polarity, vals[i]);
  59                         }
  60                         Edge term = constraintAND(cnf, numDomains, carray);
  61                         pushVectorEdge(clauses, term);
  62                         ASSERT(getSizeVectorEdge(clauses) > 0);
  63                 }
  64
  65                 notfinished = false;
  66                 for (uint i = 0; i < numDomains; i++) {
  67                         uint index = ++indices[i];
  68                         Set *set = predicate->domains.get(i);
  69
  70                         if (index < set->getSize()) {
  71                                 vals[i] = set->getElement(index);
  72                                 notfinished = true;
  73                                 break;
  74                         } else {
  75                                 indices[i] = 0;
  76                                 vals[i] = set->getElement(0);
  77                         }
  78                 }
  79         }
  80         if (getSizeVectorEdge(clauses) == 0) {
  81                 return E_False;
  82         }
  83         Edge cor = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
  84         clearVectorEdge(clauses);
  85         return generateNegation ? constraintNegate(cor) : cor;
  86 }
  87
  88
  89 void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func) {
  90 #ifdef TRACE_DEBUG
  91         model_print("Operator Function ...\n");
  92 #endif
  93         FunctionOperator *function = (FunctionOperator *) func->getFunction();
  94         uint numDomains = func->inputs.getSize();
  95
  96         /* Call base encoders for children */
  97         for (uint i = 0; i < numDomains; i++) {
  98                 Element *elem = func->inputs.get(i);
  99                 encodeElementSATEncoder(elem);
 100         }
 101
 102         VectorEdge *clauses = allocDefVectorEdge();     // Setup array of clauses
 103
 104         uint indices[numDomains];       //setup indices
 105         bzero(indices, sizeof(uint) * numDomains);
 106
 107         uint64_t vals[numDomains];//setup value array
 108         for (uint i = 0; i < numDomains; i++) {
 109                 Set *set = func->inputs.get(i)->getRange();
 110                 vals[i] = set->getElement(indices[i]);
 111         }
 112
 113         bool notfinished = true;
 114         while (notfinished) {
 115                 Edge carray[numDomains + 1];
 116
 117                 uint64_t result = function->applyFunctionOperator(numDomains, vals);
 118                 bool isInRange = ((FunctionOperator *)func->getFunction())->isInRangeFunction(result);
 119                 bool needClause = isInRange;
 120                 if (function->overflowbehavior == SATC_OVERFLOWSETSFLAG || function->overflowbehavior == SATC_FLAGIFFOVERFLOW) {
 121                         needClause = true;
 122                 }
 123
 124                 if (needClause) {
 125                         //Include this in the set of terms
 126                         for (uint i = 0; i < numDomains; i++) {
 127                                 Element *elem = func->inputs.get(i);
 128                                 carray[i] = getElementValueConstraint(elem, P_FALSE, vals[i]);
 129                         }
 130                         if (isInRange) {
 131                                 carray[numDomains] = getElementValueConstraint(func, P_TRUE, result);
 132                         }
 133
 134                         Edge clause;
 135                         switch (function->overflowbehavior) {
 136                         case SATC_IGNORE:
 137                         case SATC_NOOVERFLOW:
 138                         case SATC_WRAPAROUND: {
 139                                 clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
 140                                 break;
 141                         }
 142                         case SATC_FLAGFORCESOVERFLOW: {
 143                                 Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
 144                                 clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
 145                                 break;
 146                         }
 147                         case SATC_OVERFLOWSETSFLAG: {
 148                                 if (isInRange) {
 149                                         clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
 150                                 } else {
 151                                         Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
 152                                         clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), overFlowConstraint);
 153                                 }
 154                                 break;
 155                         }
 156                         case SATC_FLAGIFFOVERFLOW: {
 157                                 Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
 158                                 if (isInRange) {
 159                                         clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
 160                                 } else {
 161                                         clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), overFlowConstraint);
 162                                 }
 163                                 break;
 164                         }
 165                         default:
 166                                 ASSERT(0);
 167                         }
 168 #ifdef TRACE_DEBUG
 169                         model_print("added clause in operator function\n");
 170                         printCNF(clause);
 171                         model_print("\n");
 172 #endif
 173                         pushVectorEdge(clauses, clause);
 174                 }
 175
 176                 notfinished = false;
 177                 for (uint i = 0; i < numDomains; i++) {
 178                         uint index = ++indices[i];
 179                         Set *set = func->inputs.get(i)->getRange();
 180
 181                         if (index < set->getSize()) {
 182                                 vals[i] = set->getElement(index);
 183                                 notfinished = true;
 184                                 break;
 185                         } else {
 186                                 indices[i] = 0;
 187                                 vals[i] = set->getElement(0);
 188                         }
 189                 }
 190         }
 191         if (getSizeVectorEdge(clauses) == 0) {
 192                 deleteVectorEdge(clauses);
 193                 return;
 194         }
 195         Edge cor = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
 196         addConstraintCNF(cnf, cor);
 197         deleteVectorEdge(clauses);
 198 }
 199
 200 Edge SATEncoder::encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constraint) {
 201         PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
 202         Element *elem0 = constraint->inputs.get(0);
 203         encodeElementSATEncoder(elem0);
 204         Element *elem1 = constraint->inputs.get(1);
 205         encodeElementSATEncoder(elem1);
 206         ElementEncoding *ee0 = elem0->getElementEncoding();
 207         ElementEncoding *ee1 = elem1->getElementEncoding();
 208         ASSERT(ee0->numVars == ee1->numVars);
 209         uint numVars = ee0->numVars;
 210         switch (predicate->getOp()) {
 211         case SATC_EQUALS:
 212                 return generateEquivNVConstraint(cnf, numVars, ee0->variables, ee1->variables);
 213         case SATC_LT:
 214                 return generateLTConstraint(cnf, numVars, ee0->variables, ee1->variables);
 215         case SATC_GT:
 216                 return generateLTConstraint(cnf, numVars, ee1->variables, ee0->variables);
 217         default:
 218                 ASSERT(0);
 219         }
 220         exit(-1);
 221 }
 222