src/Backend/satencoder.c

   1 #include "satencoder.h"
   2 #include "structs.h"
   3 #include "csolver.h"
   4 #include "boolean.h"
   5 #include "constraint.h"
   6 #include "common.h"
   7 #include "element.h"
   8 #include "function.h"
   9 #include "tableentry.h"
  10 #include "table.h"
  11 #include "order.h"
  12 #include "predicate.h"
  13
  14
  15 SATEncoder * allocSATEncoder() {
  16         SATEncoder *This=ourmalloc(sizeof (SATEncoder));
  17         This->varcount=1;
  18         return This;
  19 }
  20
  21 void deleteSATEncoder(SATEncoder *This) {
  22         ourfree(This);
  23 }
  24
  25 void initializeConstraintVars(CSolver* csolver, SATEncoder* This){
  26         /** We really should not walk the free list to generate constraint
  27                         variables...walk the constraint tree instead.  Or even better
  28                         yet, just do this as you need to during the encodeAllSATEncoder
  29                         walk.  */
  30
  31 //      FIXME!!!!(); // Make sure Hamed sees comment above
  32
  33         uint size = getSizeVectorElement(csolver->allElements);
  34         for(uint i=0; i<size; i++){
  35                 Element* element = getVectorElement(csolver->allElements, i);
  36                 generateElementEncodingVariables(This,getElementEncoding(element));
  37         }
  38 }
  39
  40
  41 Constraint * getElementValueConstraint(Element* This, uint64_t value) {
  42         switch(getElementEncoding(This)->type){
  43                 case ONEHOT:
  44                         ASSERT(0);
  45                         break;
  46                 case UNARY:
  47                         ASSERT(0);
  48                         break;
  49                 case BINARYINDEX:
  50                         ASSERT(0);
  51                         break;
  52                 case ONEHOTBINARY:
  53                         return getElementValueBinaryIndexConstraint(This, value);
  54                         break;
  55                 case BINARYVAL:
  56                         ASSERT(0);
  57                         break;
  58                 default:
  59                         ASSERT(0);
  60                         break;
  61         }
  62         return NULL;
  63 }
  64 Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value) {
  65         ASTNodeType type = GETELEMENTTYPE(This);
  66         ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
  67         ElementEncoding* elemEnc = getElementEncoding(This);
  68         for(uint i=0; i<elemEnc->encArraySize; i++){
  69                 if( isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value){
  70                         return generateBinaryConstraint(elemEnc->numVars,
  71                                 elemEnc->variables, i);
  72                 }
  73         }
  74         ASSERT(0);
  75         return NULL;
  76 }
  77
  78 void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
  79         VectorBoolean *constraints=csolver->constraints;
  80         uint size=getSizeVectorBoolean(constraints);
  81         for(uint i=0;i<size;i++) {
  82                 Boolean *constraint=getVectorBoolean(constraints, i);
  83                 encodeConstraintSATEncoder(This, constraint);
  84         }
  85
  86 //      FIXME: Following line for element!
  87 //      size = getSizeVectorElement(csolver->allElements);
  88 //      for(uint i=0; i<size; i++){
  89 //              Element* element = getVectorElement(csolver->allElements, i);
  90 //              switch(GETELEMENTTYPE(element)){
  91 //                      case ELEMFUNCRETURN:
  92 //                              encodeFunctionElementSATEncoder(This, (ElementFunction*) element);
  93 //                              break;
  94 //                      default:
  95 //                              continue;
  96 //                              //ElementSets that aren't used in any constraints/functions
  97 //                              //will be eliminated.
  98 //              }
  99 //      }
 100 }
 101
 102 Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
 103         switch(GETBOOLEANTYPE(constraint)) {
 104         case ORDERCONST:
 105                 return encodeOrderSATEncoder(This, (BooleanOrder *) constraint);
 106         case BOOLEANVAR:
 107                 return encodeVarSATEncoder(This, (BooleanVar *) constraint);
 108         case LOGICOP:
 109                 return encodeLogicSATEncoder(This, (BooleanLogic *) constraint);
 110         case PREDICATEOP:
 111                 return encodePredicateSATEncoder(This, (BooleanPredicate *) constraint);
 112         default:
 113                 model_print("Unhandled case in encodeConstraintSATEncoder %u", GETBOOLEANTYPE(constraint));
 114                 exit(-1);
 115         }
 116 }
 117
 118 void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray) {
 119         for(uint i=0;i<num;i++)
 120                 carray[i]=getNewVarSATEncoder(encoder);
 121 }
 122
 123 Constraint * getNewVarSATEncoder(SATEncoder *This) {
 124         Constraint * var=allocVarConstraint(VAR, This->varcount);
 125         Constraint * varneg=allocVarConstraint(NOTVAR, This->varcount++);
 126         setNegConstraint(var, varneg);
 127         setNegConstraint(varneg, var);
 128         return var;
 129 }
 130
 131 Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) {
 132         if (constraint->var == NULL) {
 133                 constraint->var=getNewVarSATEncoder(This);
 134         }
 135         return constraint->var;
 136 }
 137
 138 Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) {
 139         Constraint * array[getSizeArrayBoolean(&constraint->inputs)];
 140         for(uint i=0;i<getSizeArrayBoolean(&constraint->inputs);i++)
 141                 array[i]=encodeConstraintSATEncoder(This, getArrayBoolean(&constraint->inputs, i));
 142
 143         switch(constraint->op) {
 144         case L_AND:
 145                 return allocArrayConstraint(AND, getSizeArrayBoolean(&constraint->inputs), array);
 146         case L_OR:
 147                 return allocArrayConstraint(OR, getSizeArrayBoolean(&constraint->inputs), array);
 148         case L_NOT:
 149                 ASSERT(constraint->numArray==1);
 150                 return negateConstraint(array[0]);
 151         case L_XOR: {
 152                 ASSERT(constraint->numArray==2);
 153                 Constraint * nleft=negateConstraint(cloneConstraint(array[0]));
 154                 Constraint * nright=negateConstraint(cloneConstraint(array[1]));
 155                 return allocConstraint(OR,
 156                                                                                                          allocConstraint(AND, array[0], nright),
 157                                                                                                          allocConstraint(AND, nleft, array[1]));
 158         }
 159         case L_IMPLIES:
 160                 ASSERT(constraint->numArray==2);
 161                 return allocConstraint(IMPLIES, array[0], array[1]);
 162         default:
 163                 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
 164                 exit(-1);
 165         }
 166 }
 167
 168 Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
 169         switch( constraint->order->type){
 170                 case PARTIAL:
 171                         return encodePartialOrderSATEncoder(This, constraint);
 172                 case TOTAL:
 173                         return encodeTotalOrderSATEncoder(This, constraint);
 174                 default:
 175                         ASSERT(0);
 176         }
 177         return NULL;
 178 }
 179
 180 Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){
 181         ASSERT(boolOrder->order->type == TOTAL);
 182         HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
 183         if( containsBoolConst(boolToConsts, boolOrder) ){
 184                 return getBoolConst(boolToConsts, boolOrder);
 185         } else {
 186                 Constraint* constraint = getNewVarSATEncoder(This);
 187                 putBoolConst(boolToConsts,boolOrder, constraint);
 188                 VectorBoolean* orderConstrs = &boolOrder->order->constraints;
 189                 uint size= getSizeVectorBoolean(orderConstrs);
 190                 for(uint i=0; i<size; i++){
 191                         ASSERT(GETBOOLEANTYPE( getVectorBoolean(orderConstrs, i)) == ORDERCONST );
 192                         BooleanOrder* tmp = (BooleanOrder*)getVectorBoolean(orderConstrs, i);
 193                         BooleanOrder* newBool;
 194                         Constraint* first, *second;
 195                         if(tmp->second==boolOrder->first){
 196                                 newBool = (BooleanOrder*)allocBooleanOrder(tmp->order,tmp->first,boolOrder->second);
 197                                 first = encodeTotalOrderSATEncoder(This, tmp);
 198                                 second = constraint;
 199
 200                         }else if (boolOrder->second == tmp->first){
 201                                 newBool = (BooleanOrder*)allocBooleanOrder(tmp->order,boolOrder->first,tmp->second);
 202                                 first = constraint;
 203                                 second = encodeTotalOrderSATEncoder(This, tmp);
 204                         }else
 205                                 continue;
 206                         Constraint* transConstr= encodeTotalOrderSATEncoder(This, newBool);
 207                         generateTransOrderConstraintSATEncoder(This, first, second, transConstr );
 208                 }
 209                 return constraint;
 210         }
 211
 212         return NULL;
 213 }
 214
 215 Constraint * generateTransOrderConstraintSATEncoder(SATEncoder *This, Constraint *first,Constraint *second,Constraint *third){
 216         //FIXME: first we should add the the constraint to the satsolver!
 217         return allocConstraint(IMPLIES, allocConstraint(AND, first, second), third);
 218 }
 219
 220 Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint){
 221         return NULL;
 222 }
 223
 224 Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
 225         switch(GETPREDICATETYPE(constraint) ){
 226                 case TABLEPRED:
 227                         return encodeTablePredicateSATEncoder(This, constraint);
 228                 case OPERATORPRED:
 229                         return encodeOperatorPredicateSATEncoder(This, constraint);
 230                 default:
 231                         ASSERT(0);
 232         }
 233         return NULL;
 234 }
 235
 236 Constraint * encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
 237         switch(constraint->encoding.type){
 238                 case ENUMERATEIMPLICATIONS:
 239                         return encodeEnumTablePredicateSATEncoder(This, constraint);
 240                 case CIRCUIT:
 241                         ASSERT(0);
 242                         break;
 243                 default:
 244                         ASSERT(0);
 245         }
 246         return NULL;
 247 }
 248
 249 Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
 250         VectorTableEntry* entries = &(((PredicateTable*)constraint->predicate)->table->entries);
 251         uint size = getSizeVectorTableEntry(entries);
 252         for(uint i=0; i<size; i++){
 253                 TableEntry* entry = getVectorTableEntry(entries, i);
 254
 255         }
 256         return NULL;
 257 }
 258
 259 Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
 260         switch(constraint->encoding.type){
 261                 case ENUMERATEIMPLICATIONS:
 262                         break;
 263                 case CIRCUIT:
 264                         break;
 265                 default:
 266                         ASSERT(0);
 267         }
 268         return NULL;
 269 }
 270
 271 Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){
 272         switch(GETFUNCTIONTYPE(This->function)){
 273                 case TABLEFUNC:
 274                         return encodeTableElementFunctionSATEncoder(encoder, This);
 275                 case OPERATORFUNC:
 276                         return encodeOperatorElementFunctionSATEncoder(encoder, This);
 277                 default:
 278                         ASSERT(0);
 279         }
 280         return NULL;
 281 }
 282
 283 Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
 284         switch(getElementFunctionEncoding(This)->type){
 285                 case ENUMERATEIMPLICATIONS:
 286                         return encodeEnumTableElemFunctionSATEncoder(encoder, This);
 287                         break;
 288                 case CIRCUIT:
 289                         ASSERT(0);
 290                         break;
 291                 default:
 292                         ASSERT(0);
 293         }
 294         return NULL;
 295 }
 296
 297 Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
 298         //FIXME: for now it just adds/substracts inputs exhustively
 299         return NULL;
 300 }
 301
 302 Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
 303         ASSERT(GETFUNCTIONTYPE(This->function)==TABLEFUNC);
 304         ArrayElement* elements= &This->inputs;
 305         Table* table = ((FunctionTable*) (This->function))->table;
 306         uint size = getSizeVectorTableEntry(&table->entries);
 307         Constraint* constraints[size]; //FIXME: should add a space for the case that didn't match any entries
 308         for(uint i=0; i<size; i++){
 309                 TableEntry* entry = getVectorTableEntry(&table->entries, i);
 310                 uint inputNum =getSizeArrayElement(elements);
 311                 Element* el= getArrayElement(elements, i);
 312                 Constraint* carray[inputNum];
 313                 for(uint j=0; j<inputNum; j++){
 314                         carray[inputNum] = getElementValueConstraint(el, entry->inputs[j]);
 315                 }
 316                 Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray),
 317                         getElementValueBinaryIndexConstraint((Element*)This, entry->output));
 318                 constraints[i]=row;
 319         }
 320         Constraint* result = allocArrayConstraint(OR, size, constraints);
 321         return result;
 322 }