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