src/Backend/satfuncopencoder.c

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