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