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 #include "common.h"
  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         if(getSizeVectorEdge(clauses) == 0)
 140                 return E_False;
 141         Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
 142         deleteVectorEdge(clauses);
 143         return generateNegation ? constraintNegate(cor) : cor;
 144 }
 145
 146
 147 void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction* func) {
 148 #ifdef TRACE_DEBUG
 149         model_print("Operator Function ...\n");
 150 #endif
 151         FunctionOperator * function = (FunctionOperator *) func->function;
 152         uint numDomains=getSizeArrayElement(&func->inputs);
 153
 154         /* Call base encoders for children */
 155         for(uint i=0;i<numDomains;i++) {
 156                 Element *elem = getArrayElement( &func->inputs, i);
 157                 encodeElementSATEncoder(This, elem);
 158         }
 159
 160         VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses
 161
 162         uint indices[numDomains]; //setup indices
 163         bzero(indices, sizeof(uint)*numDomains);
 164
 165         uint64_t vals[numDomains]; //setup value array
 166         for(uint i=0;i<numDomains; i++) {
 167                 Set * set=getElementSet(getArrayElement(&func->inputs, i));
 168                 vals[i]=getSetElement(set, indices[i]);
 169         }
 170
 171         Edge overFlowConstraint = ((BooleanVar*) func->overflowstatus)->var;
 172
 173         bool notfinished=true;
 174         while(notfinished) {
 175                 Edge carray[numDomains+1];
 176
 177                 uint64_t result=applyFunctionOperator(function, numDomains, vals);
 178                 bool isInRange = isInRangeFunction((FunctionOperator*)func->function, result);
 179                 bool needClause = isInRange;
 180                 if (function->overflowbehavior == OVERFLOWSETSFLAG || function->overflowbehavior == FLAGIFFOVERFLOW) {
 181                         needClause=true;
 182                 }
 183
 184                 if (needClause) {
 185                         //Include this in the set of terms
 186                         for(uint i=0;i<numDomains;i++) {
 187                                 Element * elem = getArrayElement(&func->inputs, i);
 188                                 carray[i] = getElementValueConstraint(This, elem, vals[i]);
 189                         }
 190                         if (isInRange) {
 191                                 carray[numDomains] = getElementValueConstraint(This, &func->base, result);
 192                         }
 193
 194                         Edge clause;
 195                         switch(function->overflowbehavior) {
 196                         case IGNORE:
 197                         case NOOVERFLOW:
 198                         case WRAPAROUND: {
 199                                 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
 200                                 break;
 201                         }
 202                         case FLAGFORCESOVERFLOW: {
 203                                 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
 204                                 break;
 205                         }
 206                         case OVERFLOWSETSFLAG: {
 207                                 if (isInRange) {
 208                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
 209                                 } else {
 210                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
 211                                 }
 212                                 break;
 213                         }
 214                         case FLAGIFFOVERFLOW: {
 215                                 if (isInRange) {
 216                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
 217                                 } else {
 218                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
 219                                 }
 220                                 break;
 221                         }
 222                         default:
 223                                 ASSERT(0);
 224                         }
 225 #ifdef TRACE_DEBUG
 226                         model_print("added clause in operator function\n");
 227                         printCNF(clause);
 228                         model_print("\n");
 229 #endif
 230                         pushVectorEdge(clauses, clause);
 231                 }
 232
 233                 notfinished=false;
 234                 for(uint i=0;i<numDomains; i++) {
 235                         uint index=++indices[i];
 236                         Set * set=getElementSet(getArrayElement(&func->inputs, i));
 237
 238                         if (index < getSetSize(set)) {
 239                                 vals[i]=getSetElement(set, index);
 240                                 notfinished=true;
 241                                 break;
 242                         } else {
 243                                 indices[i]=0;
 244                                 vals[i]=getSetElement(set, 0);
 245                         }
 246                 }
 247         }
 248
 249         Edge cor=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
 250         addConstraintCNF(This->cnf, cor);
 251         deleteVectorEdge(clauses);
 252 }
 253
 254 void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* func){
 255 #ifdef TRACE_DEBUG
 256         model_print("Enumeration Table functions ...\n");
 257 #endif
 258         //FIXME: HANDLE UNDEFINED BEHAVIORS
 259         ASSERT(GETFUNCTIONTYPE(func->function)==TABLEFUNC);
 260         ArrayElement* elements= &func->inputs;
 261         for(uint i=0; i<getSizeArrayElement(elements); i++){
 262                 Element *elem = getArrayElement( elements, i);
 263                 encodeElementSATEncoder(This, elem);
 264         }
 265
 266         Table* table = ((FunctionTable*) (func->function))->table;
 267         uint size = getSizeVectorTableEntry(&table->entries);
 268         Edge constraints[size]; //FIXME: should add a space for the case that didn't match any entries
 269         for(uint i=0; i<size; i++) {
 270                 TableEntry* entry = getVectorTableEntry(&table->entries, i);
 271                 uint inputNum = getSizeArrayElement(elements);
 272                 Edge carray[inputNum];
 273                 for(uint j=0; j<inputNum; j++){
 274                         Element* el= getArrayElement(elements, j);
 275                         carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
 276                 }
 277                 Edge output = getElementValueConstraint(This, (Element*)func, entry->output);
 278                 Edge row= constraintIMPLIES(This->cnf, constraintAND(This->cnf, inputNum, carray), output);
 279                 constraints[i]=row;
 280         }
 281         addConstraintCNF(This->cnf, constraintAND(This->cnf, size, constraints));
 282 }