src/Backend/satfuncencoder.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
  12 Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
  13         VectorTableEntry* entries = &(((PredicateTable*)constraint->predicate)->table->entries);
  14         FunctionEncodingType encType = constraint->encoding.type;
  15         ArrayElement* inputs = &constraint->inputs;
  16         uint inputNum =getSizeArrayElement(inputs);
  17         //Encode all the inputs first ...
  18         for(uint i=0; i<inputNum; i++){
  19                 encodeElementSATEncoder(This, getArrayElement(inputs, i));
  20         }
  21
  22         //WARNING: THIS ASSUMES PREDICATE TABLE IS COMPLETE...SEEMS UNLIKELY TO BE SAFE IN MANY CASES...
  23         //WONDER WHAT BEST WAY TO HANDLE THIS IS...
  24
  25         uint size = getSizeVectorTableEntry(entries);
  26         bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
  27         Edge constraints[size];
  28         for(uint i=0; i<size; i++){
  29                 TableEntry* entry = getVectorTableEntry(entries, i);
  30                 if(generateNegation == entry->output) {
  31                         //Skip the irrelevant entries
  32                         continue;
  33                 }
  34                 Edge carray[inputNum];
  35                 for(uint j=0; j<inputNum; j++){
  36                         Element* el = getArrayElement(inputs, j);
  37                         carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
  38                 }
  39                 constraints[i]=constraintAND(This->cnf, inputNum, carray);
  40         }
  41         Edge result=constraintOR(This->cnf, size, constraints);
  42
  43         return generateNegation ? result: constraintNegate(result);
  44 }
  45
  46 Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
  47         switch(constraint->encoding.type){
  48                 case ENUMERATEIMPLICATIONS:
  49                         return encodeEnumOperatorPredicateSATEncoder(This, constraint);
  50                 case CIRCUIT:
  51                         ASSERT(0);
  52                         break;
  53                 default:
  54                         ASSERT(0);
  55         }
  56         return E_BOGUS;
  57 }
  58
  59 Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
  60         PredicateOperator* predicate = (PredicateOperator*)constraint->predicate;
  61         uint numDomains=getSizeArraySet(&predicate->domains);
  62
  63         FunctionEncodingType encType = constraint->encoding.type;
  64         bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
  65
  66         /* Call base encoders for children */
  67         for(uint i=0;i<numDomains;i++) {
  68                 Element *elem = getArrayElement( &constraint->inputs, i);
  69                 encodeElementSATEncoder(This, elem);
  70         }
  71         VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses
  72
  73         uint indices[numDomains]; //setup indices
  74         bzero(indices, sizeof(uint)*numDomains);
  75
  76         uint64_t vals[numDomains]; //setup value array
  77         for(uint i=0;i<numDomains; i++) {
  78                 Set * set=getArraySet(&predicate->domains, i);
  79                 vals[i]=getSetElement(set, indices[i]);
  80         }
  81
  82         bool notfinished=true;
  83         while(notfinished) {
  84                 Edge carray[numDomains];
  85
  86                 if (evalPredicateOperator(predicate, vals) ^ generateNegation) {
  87                         //Include this in the set of terms
  88                         for(uint i=0;i<numDomains;i++) {
  89                                 Element * elem = getArrayElement(&constraint->inputs, i);
  90                                 carray[i] = getElementValueConstraint(This, elem, vals[i]);
  91                         }
  92                         pushVectorEdge(clauses, constraintAND(This->cnf, numDomains, carray));
  93                 }
  94
  95                 notfinished=false;
  96                 for(uint i=0;i<numDomains; i++) {
  97                         uint index=++indices[i];
  98                         Set * set=getArraySet(&predicate->domains, i);
  99
 100                         if (index < getSetSize(set)) {
 101                                 vals[i]=getSetElement(set, index);
 102                                 notfinished=true;
 103                                 break;
 104                         } else {
 105                                 indices[i]=0;
 106                                 vals[i]=getSetElement(set, 0);
 107                         }
 108                 }
 109         }
 110
 111         Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
 112         deleteVectorEdge(clauses);
 113         return generateNegation ? cor : constraintNegate(cor);
 114 }
 115
 116
 117 Edge encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction* func) {
 118         FunctionOperator * function = (FunctionOperator *) func->function;
 119         uint numDomains=getSizeArrayElement(&func->inputs);
 120
 121         /* Call base encoders for children */
 122         for(uint i=0;i<numDomains;i++) {
 123                 Element *elem = getArrayElement( &func->inputs, i);
 124                 encodeElementSATEncoder(This, elem);
 125         }
 126
 127         VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses
 128
 129         uint indices[numDomains]; //setup indices
 130         bzero(indices, sizeof(uint)*numDomains);
 131
 132         uint64_t vals[numDomains]; //setup value array
 133         for(uint i=0;i<numDomains; i++) {
 134                 Set * set=getElementSet(getArrayElement(&func->inputs, i));
 135                 vals[i]=getSetElement(set, indices[i]);
 136         }
 137
 138         Edge overFlowConstraint = ((BooleanVar*) func->overflowstatus)->var;
 139
 140         bool notfinished=true;
 141         while(notfinished) {
 142                 Edge carray[numDomains+2];
 143
 144                 uint64_t result=applyFunctionOperator(function, numDomains, vals);
 145                 bool isInRange = isInRangeFunction((FunctionOperator*)func->function, result);
 146                 bool needClause = isInRange;
 147                 if (function->overflowbehavior == OVERFLOWSETSFLAG || function->overflowbehavior == FLAGIFFOVERFLOW) {
 148                         needClause=true;
 149                 }
 150
 151                 if (needClause) {
 152                         //Include this in the set of terms
 153                         for(uint i=0;i<numDomains;i++) {
 154                                 Element * elem = getArrayElement(&func->inputs, i);
 155                                 carray[i] = getElementValueConstraint(This, elem, vals[i]);
 156                         }
 157                         if (isInRange) {
 158                                 carray[numDomains] = getElementValueConstraint(This, &func->base, result);
 159                         }
 160
 161                         Edge clause;
 162                         switch(function->overflowbehavior) {
 163                         case IGNORE:
 164                         case NOOVERFLOW:
 165                         case WRAPAROUND: {
 166                                 clause=constraintAND(This->cnf, numDomains+1, carray);
 167                                 break;
 168                         }
 169                         case FLAGFORCESOVERFLOW: {
 170                                 carray[numDomains+1]=constraintNegate(overFlowConstraint);
 171                                 clause=constraintAND(This->cnf, numDomains+2, carray);
 172                                 break;
 173                         }
 174                         case OVERFLOWSETSFLAG: {
 175                                 if (isInRange) {
 176                                         clause=constraintAND(This->cnf, numDomains+1, carray);
 177                                 } else {
 178                                         carray[numDomains+1]=overFlowConstraint;
 179                                         clause=constraintAND(This->cnf, numDomains+1, carray);
 180                                 }
 181                                 break;
 182                         }
 183                         case FLAGIFFOVERFLOW: {
 184                                 if (isInRange) {
 185                                 carray[numDomains+1]=constraintNegate(overFlowConstraint);
 186                                         clause=constraintAND(This->cnf, numDomains+2, carray);
 187                                 } else {
 188                                         carray[numDomains+1]=overFlowConstraint;
 189                                         clause=constraintAND(This->cnf, numDomains+1, carray);
 190                                 }
 191                                 break;
 192                         }
 193                         default:
 194                                 ASSERT(0);
 195                         }
 196                         pushVectorEdge(clauses, clause);
 197                 }
 198
 199                 notfinished=false;
 200                 for(uint i=0;i<numDomains; i++) {
 201                         uint index=++indices[i];
 202                         Set * set=getElementSet(getArrayElement(&func->inputs, i));
 203
 204                         if (index < getSetSize(set)) {
 205                                 vals[i]=getSetElement(set, index);
 206                                 notfinished=true;
 207                                 break;
 208                         } else {
 209                                 indices[i]=0;
 210                                 vals[i]=getSetElement(set, 0);
 211                         }
 212                 }
 213         }
 214
 215         Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
 216         deleteVectorEdge(clauses);
 217         return cor;
 218 }
 219
 220 Edge encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
 221         //FIXME: HANDLE UNDEFINED BEHAVIORS
 222         ASSERT(GETFUNCTIONTYPE(This->function)==TABLEFUNC);
 223         ArrayElement* elements= &This->inputs;
 224         Table* table = ((FunctionTable*) (This->function))->table;
 225         uint size = getSizeVectorTableEntry(&table->entries);
 226         Edge constraints[size]; //FIXME: should add a space for the case that didn't match any entries
 227         for(uint i=0; i<size; i++) {
 228                 TableEntry* entry = getVectorTableEntry(&table->entries, i);
 229                 uint inputNum = getSizeArrayElement(elements);
 230                 Edge carray[inputNum];
 231                 for(uint j=0; j<inputNum; j++){
 232                         Element* el= getArrayElement(elements, j);
 233                         carray[j] = getElementValueConstraint(encoder, el, entry->inputs[j]);
 234                 }
 235                 Edge output = getElementValueConstraint(encoder, (Element*)This, entry->output);
 236                 Edge row= constraintIMPLIES(encoder->cnf, constraintAND(encoder->cnf, inputNum, carray), output);
 237                 constraints[i]=row;
 238         }
 239         return constraintOR(encoder->cnf, size, constraints);
 240 }