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