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 ? constraintNegate(result) : 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                         return encodeCircuitOperatorPredicateEncoder(This, constraint);
  52                 default:
  53                         ASSERT(0);
  54         }
  55         exit(-1);
  56 }
  57
  58 Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate * constraint) {
  59         PredicateOperator * predicate = (PredicateOperator*) constraint->predicate;
  60
  61         switch(predicate->op) {
  62         case EQUALS: {
  63                 return encodeCircuitEquals(This, constraint);
  64         }
  65         default:
  66                 ASSERT(0);
  67         }
  68         exit(-1);
  69 }
  70
  71 Edge encodeCircuitEquals(SATEncoder * This, BooleanPredicate * constraint) {
  72         PredicateOperator * predicate = (PredicateOperator*) constraint->predicate;
  73         ASSERT(getSizeArraySet(&predicate->domains) == 2);
  74         Element *elem0 = getArrayElement( &constraint->inputs, 0);
  75         Element *elem1 = getArrayElement( &constraint->inputs, 1);
  76         ElementEncoding *ee0=getElementEncoding(elem0);
  77         ElementEncoding *ee1=getElementEncoding(elem1);
  78         ASSERT(ee0->numVars==ee1->numVars);
  79         uint numVars=ee0->numVars;
  80         Edge carray[numVars];
  81         for (uint i=0; i<numVars; i++) {
  82                 carray[i]=constraintIFF(This->cnf, ee0->variables[i], ee1->variables[i]);
  83         }
  84         return constraintAND(This->cnf, numVars, carray);
  85 }
  86
  87 Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
  88         PredicateOperator* predicate = (PredicateOperator*)constraint->predicate;
  89         uint numDomains=getSizeArraySet(&predicate->domains);
  90
  91         FunctionEncodingType encType = constraint->encoding.type;
  92         bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
  93
  94         /* Call base encoders for children */
  95         for(uint i=0;i<numDomains;i++) {
  96                 Element *elem = getArrayElement( &constraint->inputs, i);
  97                 encodeElementSATEncoder(This, elem);
  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=getArraySet(&predicate->domains, i);
 107                 vals[i]=getSetElement(set, indices[i]);
 108         }
 109
 110         bool notfinished=true;
 111         while(notfinished) {
 112                 Edge carray[numDomains];
 113
 114                 if (evalPredicateOperator(predicate, vals) ^ generateNegation) {
 115                         //Include this in the set of terms
 116                         for(uint i=0;i<numDomains;i++) {
 117                                 Element * elem = getArrayElement(&constraint->inputs, i);
 118                                 carray[i] = getElementValueConstraint(This, elem, vals[i]);
 119                         }
 120                         Edge term=constraintAND(This->cnf, numDomains, carray);
 121                         pushVectorEdge(clauses, term);
 122                 }
 123
 124                 notfinished=false;
 125                 for(uint i=0;i<numDomains; i++) {
 126                         uint index=++indices[i];
 127                         Set * set=getArraySet(&predicate->domains, i);
 128
 129                         if (index < getSetSize(set)) {
 130                                 vals[i]=getSetElement(set, index);
 131                                 notfinished=true;
 132                                 break;
 133                         } else {
 134                                 indices[i]=0;
 135                                 vals[i]=getSetElement(set, 0);
 136                         }
 137                 }
 138         }
 139
 140         Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
 141         deleteVectorEdge(clauses);
 142         return generateNegation ? constraintNegate(cor) : cor;
 143 }
 144
 145
 146 void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction* func) {
 147         FunctionOperator * function = (FunctionOperator *) func->function;
 148         uint numDomains=getSizeArrayElement(&func->inputs);
 149
 150         /* Call base encoders for children */
 151         for(uint i=0;i<numDomains;i++) {
 152                 Element *elem = getArrayElement( &func->inputs, i);
 153                 encodeElementSATEncoder(This, elem);
 154         }
 155
 156         VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses
 157
 158         uint indices[numDomains]; //setup indices
 159         bzero(indices, sizeof(uint)*numDomains);
 160
 161         uint64_t vals[numDomains]; //setup value array
 162         for(uint i=0;i<numDomains; i++) {
 163                 Set * set=getElementSet(getArrayElement(&func->inputs, i));
 164                 vals[i]=getSetElement(set, indices[i]);
 165         }
 166
 167         Edge overFlowConstraint = ((BooleanVar*) func->overflowstatus)->var;
 168
 169         bool notfinished=true;
 170         while(notfinished) {
 171                 Edge carray[numDomains+2];
 172
 173                 uint64_t result=applyFunctionOperator(function, numDomains, vals);
 174                 bool isInRange = isInRangeFunction((FunctionOperator*)func->function, result);
 175                 bool needClause = isInRange;
 176                 if (function->overflowbehavior == OVERFLOWSETSFLAG || function->overflowbehavior == FLAGIFFOVERFLOW) {
 177                         needClause=true;
 178                 }
 179
 180                 if (needClause) {
 181                         //Include this in the set of terms
 182                         for(uint i=0;i<numDomains;i++) {
 183                                 Element * elem = getArrayElement(&func->inputs, i);
 184                                 carray[i] = getElementValueConstraint(This, elem, vals[i]);
 185                         }
 186                         if (isInRange) {
 187                                 carray[numDomains] = getElementValueConstraint(This, &func->base, result);
 188                         }
 189
 190                         Edge clause;
 191                         switch(function->overflowbehavior) {
 192                         case IGNORE:
 193                         case NOOVERFLOW:
 194                         case WRAPAROUND: {
 195                                 clause=constraintAND(This->cnf, numDomains+1, carray);
 196                                 break;
 197                         }
 198                         case FLAGFORCESOVERFLOW: {
 199                                 carray[numDomains+1]=constraintNegate(overFlowConstraint);
 200                                 clause=constraintAND(This->cnf, numDomains+2, carray);
 201                                 break;
 202                         }
 203                         case OVERFLOWSETSFLAG: {
 204                                 if (isInRange) {
 205                                         clause=constraintAND(This->cnf, numDomains+1, carray);
 206                                 } else {
 207                                         carray[numDomains+1]=overFlowConstraint;
 208                                         clause=constraintAND(This->cnf, numDomains+1, carray);
 209                                 }
 210                                 break;
 211                         }
 212                         case FLAGIFFOVERFLOW: {
 213                                 if (isInRange) {
 214                                 carray[numDomains+1]=constraintNegate(overFlowConstraint);
 215                                         clause=constraintAND(This->cnf, numDomains+2, carray);
 216                                 } else {
 217                                         carray[numDomains+1]=overFlowConstraint;
 218                                         clause=constraintAND(This->cnf, numDomains+1, carray);
 219                                 }
 220                                 break;
 221                         }
 222                         default:
 223                                 ASSERT(0);
 224                         }
 225                         pushVectorEdge(clauses, clause);
 226                 }
 227
 228                 notfinished=false;
 229                 for(uint i=0;i<numDomains; i++) {
 230                         uint index=++indices[i];
 231                         Set * set=getElementSet(getArrayElement(&func->inputs, i));
 232
 233                         if (index < getSetSize(set)) {
 234                                 vals[i]=getSetElement(set, index);
 235                                 notfinished=true;
 236                                 break;
 237                         } else {
 238                                 indices[i]=0;
 239                                 vals[i]=getSetElement(set, 0);
 240                         }
 241                 }
 242         }
 243
 244         Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
 245         addConstraintCNF(This->cnf, cor);
 246         deleteVectorEdge(clauses);
 247 }
 248
 249 void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* func){
 250         //FIXME: HANDLE UNDEFINED BEHAVIORS
 251         ASSERT(GETFUNCTIONTYPE(func->function)==TABLEFUNC);
 252         ArrayElement* elements= &func->inputs;
 253         Table* table = ((FunctionTable*) (func->function))->table;
 254         uint size = getSizeVectorTableEntry(&table->entries);
 255         Edge constraints[size]; //FIXME: should add a space for the case that didn't match any entries
 256         for(uint i=0; i<size; i++) {
 257                 TableEntry* entry = getVectorTableEntry(&table->entries, i);
 258                 uint inputNum = getSizeArrayElement(elements);
 259                 Edge carray[inputNum];
 260                 for(uint j=0; j<inputNum; j++){
 261                         Element* el= getArrayElement(elements, j);
 262                         carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
 263                 }
 264                 Edge output = getElementValueConstraint(This, (Element*)func, entry->output);
 265                 Edge row= constraintIMPLIES(This->cnf, constraintAND(This->cnf, inputNum, carray), output);
 266                 constraints[i]=row;
 267         }
 268         addConstraintCNF(This->cnf, constraintOR(This->cnf, size, constraints));
 269 }