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
  13 Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
  14         Table* table = ((PredicateTable*)constraint->predicate)->table;
  15         FunctionEncodingType encType = constraint->encoding.type;
  16         ArrayElement* inputs = &constraint->inputs;
  17         uint inputNum =getSizeArrayElement(inputs);
  18         //Encode all the inputs first ...
  19         for(uint i=0; i<inputNum; i++){
  20                 encodeElementSATEncoder(This, getArrayElement(inputs, i));
  21         }
  22         uint size = getSizeHashSetTableEntry(table->entrie);
  23         bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
  24         Edge constraints[size];
  25         HSIteratorTableEntry* iterator = iteratorTableEntry(table->entrie);
  26         uint i=0;
  27         while(hasNextTableEntry(iterator)){
  28                 TableEntry* entry = nextTableEntry(iterator);
  29                 if(generateNegation == entry->output) {
  30                         //Skip the irrelevant entries
  31                         continue;
  32                 }
  33                 Edge carray[inputNum];
  34                 for(uint j=0; j<inputNum; j++){
  35                         Element* el = getArrayElement(inputs, j);
  36                         carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
  37                 }
  38                 constraints[i++]=constraintAND(This->cnf, inputNum, carray);
  39         }
  40         Edge result=constraintOR(This->cnf, size, constraints);
  41
  42         return generateNegation ? constraintNegate(result) : result;
  43 }
  44 Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
  45         //FIXME
  46         return E_NULL;
  47 }
  48
  49 Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
  50         switch(constraint->encoding.type){
  51                 case ENUMERATEIMPLICATIONS:
  52                         return encodeEnumOperatorPredicateSATEncoder(This, constraint);
  53                 case CIRCUIT:
  54                         return encodeCircuitOperatorPredicateEncoder(This, constraint);
  55                 default:
  56                         ASSERT(0);
  57         }
  58         exit(-1);
  59 }
  60
  61 Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate * constraint) {
  62         PredicateOperator * predicate = (PredicateOperator*) constraint->predicate;
  63
  64         switch(predicate->op) {
  65         case EQUALS: {
  66                 return encodeCircuitEquals(This, constraint);
  67         }
  68         default:
  69                 ASSERT(0);
  70         }
  71         exit(-1);
  72 }
  73
  74 Edge encodeCircuitEquals(SATEncoder * This, BooleanPredicate * constraint) {
  75         PredicateOperator * predicate = (PredicateOperator*) constraint->predicate;
  76         ASSERT(getSizeArraySet(&predicate->domains) == 2);
  77         Element *elem0 = getArrayElement( &constraint->inputs, 0);
  78         Element *elem1 = getArrayElement( &constraint->inputs, 1);
  79         ElementEncoding *ee0=getElementEncoding(elem0);
  80         ElementEncoding *ee1=getElementEncoding(elem1);
  81         ASSERT(ee0->numVars==ee1->numVars);
  82         uint numVars=ee0->numVars;
  83         Edge carray[numVars];
  84         for (uint i=0; i<numVars; i++) {
  85                 carray[i]=constraintIFF(This->cnf, ee0->variables[i], ee1->variables[i]);
  86         }
  87         return constraintAND(This->cnf, numVars, carray);
  88 }
  89
  90 Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
  91         PredicateOperator* predicate = (PredicateOperator*)constraint->predicate;
  92         uint numDomains=getSizeArraySet(&predicate->domains);
  93
  94         FunctionEncodingType encType = constraint->encoding.type;
  95         bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
  96
  97         /* Call base encoders for children */
  98         for(uint i=0;i<numDomains;i++) {
  99                 Element *elem = getArrayElement( &constraint->inputs, i);
 100                 encodeElementSATEncoder(This, elem);
 101         }
 102         VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses
 103
 104         uint indices[numDomains]; //setup indices
 105         bzero(indices, sizeof(uint)*numDomains);
 106
 107         uint64_t vals[numDomains]; //setup value array
 108         for(uint i=0;i<numDomains; i++) {
 109                 Set * set=getArraySet(&predicate->domains, i);
 110                 vals[i]=getSetElement(set, indices[i]);
 111         }
 112
 113         bool notfinished=true;
 114         while(notfinished) {
 115                 Edge carray[numDomains];
 116
 117                 if (evalPredicateOperator(predicate, vals) ^ generateNegation) {
 118                         //Include this in the set of terms
 119                         for(uint i=0;i<numDomains;i++) {
 120                                 Element * elem = getArrayElement(&constraint->inputs, i);
 121                                 carray[i] = getElementValueConstraint(This, elem, vals[i]);
 122                         }
 123                         Edge term=constraintAND(This->cnf, numDomains, carray);
 124                         pushVectorEdge(clauses, term);
 125                 }
 126
 127                 notfinished=false;
 128                 for(uint i=0;i<numDomains; i++) {
 129                         uint index=++indices[i];
 130                         Set * set=getArraySet(&predicate->domains, i);
 131
 132                         if (index < getSetSize(set)) {
 133                                 vals[i]=getSetElement(set, index);
 134                                 notfinished=true;
 135                                 break;
 136                         } else {
 137                                 indices[i]=0;
 138                                 vals[i]=getSetElement(set, 0);
 139                         }
 140                 }
 141         }
 142         if(getSizeVectorEdge(clauses) == 0)
 143                 return E_False;
 144         Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
 145         deleteVectorEdge(clauses);
 146         return generateNegation ? constraintNegate(cor) : cor;
 147 }
 148
 149
 150 void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction* func) {
 151 #ifdef TRACE_DEBUG
 152         model_print("Operator Function ...\n");
 153 #endif
 154         FunctionOperator * function = (FunctionOperator *) func->function;
 155         uint numDomains=getSizeArrayElement(&func->inputs);
 156
 157         /* Call base encoders for children */
 158         for(uint i=0;i<numDomains;i++) {
 159                 Element *elem = getArrayElement( &func->inputs, i);
 160                 encodeElementSATEncoder(This, elem);
 161         }
 162
 163         VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses
 164
 165         uint indices[numDomains]; //setup indices
 166         bzero(indices, sizeof(uint)*numDomains);
 167
 168         uint64_t vals[numDomains]; //setup value array
 169         for(uint i=0;i<numDomains; i++) {
 170                 Set * set=getElementSet(getArrayElement(&func->inputs, i));
 171                 vals[i]=getSetElement(set, indices[i]);
 172         }
 173
 174         Edge overFlowConstraint = ((BooleanVar*) func->overflowstatus)->var;
 175
 176         bool notfinished=true;
 177         while(notfinished) {
 178                 Edge carray[numDomains+1];
 179
 180                 uint64_t result=applyFunctionOperator(function, numDomains, vals);
 181                 bool isInRange = isInRangeFunction((FunctionOperator*)func->function, result);
 182                 bool needClause = isInRange;
 183                 if (function->overflowbehavior == OVERFLOWSETSFLAG || function->overflowbehavior == FLAGIFFOVERFLOW) {
 184                         needClause=true;
 185                 }
 186
 187                 if (needClause) {
 188                         //Include this in the set of terms
 189                         for(uint i=0;i<numDomains;i++) {
 190                                 Element * elem = getArrayElement(&func->inputs, i);
 191                                 carray[i] = getElementValueConstraint(This, elem, vals[i]);
 192                         }
 193                         if (isInRange) {
 194                                 carray[numDomains] = getElementValueConstraint(This, &func->base, result);
 195                         }
 196
 197                         Edge clause;
 198                         switch(function->overflowbehavior) {
 199                         case IGNORE:
 200                         case NOOVERFLOW:
 201                         case WRAPAROUND: {
 202                                 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
 203                                 break;
 204                         }
 205                         case FLAGFORCESOVERFLOW: {
 206                                 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
 207                                 break;
 208                         }
 209                         case OVERFLOWSETSFLAG: {
 210                                 if (isInRange) {
 211                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
 212                                 } else {
 213                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
 214                                 }
 215                                 break;
 216                         }
 217                         case FLAGIFFOVERFLOW: {
 218                                 if (isInRange) {
 219                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
 220                                 } else {
 221                                         clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
 222                                 }
 223                                 break;
 224                         }
 225                         default:
 226                                 ASSERT(0);
 227                         }
 228 #ifdef TRACE_DEBUG
 229                         model_print("added clause in operator function\n");
 230                         printCNF(clause);
 231                         model_print("\n");
 232 #endif
 233                         pushVectorEdge(clauses, clause);
 234                 }
 235
 236                 notfinished=false;
 237                 for(uint i=0;i<numDomains; i++) {
 238                         uint index=++indices[i];
 239                         Set * set=getElementSet(getArrayElement(&func->inputs, i));
 240
 241                         if (index < getSetSize(set)) {
 242                                 vals[i]=getSetElement(set, index);
 243                                 notfinished=true;
 244                                 break;
 245                         } else {
 246                                 indices[i]=0;
 247                                 vals[i]=getSetElement(set, 0);
 248                         }
 249                 }
 250         }
 251
 252         Edge cor=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
 253         addConstraintCNF(This->cnf, cor);
 254         deleteVectorEdge(clauses);
 255 }
 256
 257 void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder* This, ElementFunction* func){
 258         UndefinedBehavior undefStatus = ((FunctionTable*) func->function)->undefBehavior;
 259         ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
 260         ArrayElement* elements= &func->inputs;
 261         Table* table = ((FunctionTable*) (func->function))->table;
 262         uint size = getSizeHashSetTableEntry(table->entrie);
 263         Edge constraints[size];
 264         HSIteratorTableEntry* iterator = iteratorTableEntry(table->entrie);
 265         uint i=0;
 266         while(hasNextTableEntry(iterator)) {
 267                 TableEntry* entry = nextTableEntry(iterator);
 268                 ASSERT(entry!=NULL);
 269                 uint inputNum = getSizeArrayElement(elements);
 270                 Edge carray[inputNum];
 271                 for(uint j=0; j<inputNum; j++){
 272                         Element* el= getArrayElement(elements, j);
 273                         carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
 274                 }
 275                 Edge output = getElementValueConstraint(This, (Element*)func, entry->output);
 276                 Edge row;
 277                 switch(undefStatus ){
 278                         case IGNOREBEHAVIOR: {
 279                                 row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), output);
 280                                 break;
 281                         }
 282                         case FLAGFORCEUNDEFINED: {
 283                                 Edge undefConst = ((BooleanVar*)func->overflowstatus)->var;
 284                                 row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintAND2(This->cnf, output, constraintNegate(undefConst)));
 285                                 break;
 286                         }
 287                         default:
 288                                 ASSERT(0);
 289
 290                 }
 291                 constraints[i++]=row;
 292         }
 293         deleteIterTableEntry(iterator);
 294         addConstraintCNF(This->cnf, constraintAND(This->cnf, size, constraints));
 295 }
 296
 297 void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* elemFunc){
 298 #ifdef TRACE_DEBUG
 299         model_print("Enumeration Table functions ...\n");
 300 #endif
 301         ASSERT(GETFUNCTIONTYPE(elemFunc->function)==TABLEFUNC);
 302         //First encode children
 303         ArrayElement* elements= &elemFunc->inputs;
 304         for(uint i=0; i<getSizeArrayElement(elements); i++){
 305                 Element *elem = getArrayElement( elements, i);
 306                 encodeElementSATEncoder(This, elem);
 307         }
 308
 309         FunctionTable* function =(FunctionTable*)elemFunc;
 310         switch(function->undefBehavior){
 311                 case IGNOREBEHAVIOR:
 312                 case FLAGFORCEUNDEFINED:
 313                         return encodeEnumEntriesTableElemFuncSATEncoder(This, elemFunc);
 314                 default:
 315                         break;
 316         }
 317
 318         uint numDomains=getSizeArraySet(&function->table->domains);
 319
 320         VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses
 321
 322         uint indices[numDomains]; //setup indices
 323         bzero(indices, sizeof(uint)*numDomains);
 324
 325         uint64_t vals[numDomains]; //setup value array
 326         for(uint i=0;i<numDomains; i++) {
 327                 Set * set=getArraySet(&function->table->domains, i);
 328                 vals[i]=getSetElement(set, indices[i]);
 329         }
 330
 331         Edge undefConstraint = ((BooleanVar*) elemFunc->overflowstatus)->var;
 332
 333         bool notfinished=true;
 334         while(notfinished) {
 335                 Edge carray[numDomains+1];
 336                 TableEntry* tableEntry = getTableEntryFromTable(function->table, vals, numDomains);
 337                 bool isInRange = tableEntry!=NULL;
 338                 bool needClause = isInRange;
 339                 if (function->undefBehavior == UNDEFINEDSETSFLAG || function->undefBehavior == FLAGIFFUNDEFINED) {
 340                         needClause=true;
 341                 }
 342
 343                 if (needClause) {
 344                         //Include this in the set of terms
 345                         for(uint i=0;i<numDomains;i++) {
 346                                 Element * elem = getArrayElement(&elemFunc->inputs, i);
 347                                 carray[i] = getElementValueConstraint(This, elem, vals[i]);
 348                         }
 349                         if (isInRange) {
 350                                 carray[numDomains] = getElementValueConstraint(This, (Element*)elemFunc, tableEntry->output);
 351                         }
 352
 353                         Edge clause;
 354                         switch(function->undefBehavior) {
 355                                 case UNDEFINEDSETSFLAG: {
 356                                         if (isInRange) {
 357                                                 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
 358                                         } else {
 359                                                 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
 360                                         }
 361                                         break;
 362                                 }
 363                                 case FLAGIFFUNDEFINED: {
 364                                         if (isInRange) {
 365                                                 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(undefConstraint)));
 366                                         } else {
 367                                                 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
 368                                         }
 369                                         break;
 370                                 }
 371                                 default:
 372                                         ASSERT(0);
 373                         }
 374 #ifdef TRACE_DEBUG
 375                         model_print("added clause in table enumeration ...\n");
 376                         printCNF(clause);
 377                         model_print("\n");
 378 #endif
 379                         pushVectorEdge(clauses, clause);
 380                 }
 381
 382                 notfinished=false;
 383                 for(uint i=0;i<numDomains; i++) {
 384                         uint index=++indices[i];
 385                         Set * set=getArraySet(&function->table->domains, i);
 386
 387                         if (index < getSetSize(set)) {
 388                                 vals[i]=getSetElement(set, index);
 389                                 notfinished=true;
 390                                 break;
 391                         } else {
 392                                 indices[i]=0;
 393                                 vals[i]=getSetElement(set, 0);
 394                         }
 395                 }
 396         }
 397
 398         Edge cor=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
 399         addConstraintCNF(This->cnf, cor);
 400         deleteVectorEdge(clauses);
 401
 402 }