src/ASTTransform/integerencoding.cc

   1 #include "integerencoding.h"
   2 #include "orderelement.h"
   3 #include "order.h"
   4 #include "satencoder.h"
   5 #include "csolver.h"
   6 #include "predicate.h"
   7 #include "element.h"
   8 #include "rewriter.h"
   9 #include "set.h"
  10
  11
  12 void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
  13         Order* order = boolOrder->order;
  14         if (order->elementTable == NULL) {
  15                 order->initializeOrderElementsHashTable();
  16         }
  17         //getting two elements and using LT predicate ...
  18         ElementSet* elem1 = (ElementSet*)getOrderIntegerElement(This, order, boolOrder->first);
  19         ElementSet* elem2 = (ElementSet*)getOrderIntegerElement(This, order, boolOrder->second);
  20         Set * sarray[]={elem1->set, elem2->set};
  21         Predicate *predicate =new PredicateOperator(LT, sarray, 2);
  22         Element * parray[]={elem1, elem2};
  23         BooleanPredicate * boolean=new BooleanPredicate(predicate, parray, 2, NULL);
  24         {//Adding new elements and boolean/predicate to solver regarding memory management
  25                 This->solver->allBooleans.push(boolean);
  26                 This->solver->allPredicates.push(predicate);
  27                 This->solver->constraints.add(boolean);
  28         }
  29         replaceBooleanWithBoolean(This->solver, boolOrder, boolean);
  30 }
  31
  32
  33 Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) {
  34         HashSetOrderElement* eset = order->elementTable;
  35         OrderElement oelement(item, NULL);
  36         if( !eset->contains(&oelement)){
  37                 Set* set = new Set(order->set->type, 1, (uint64_t) order->set->getSize());
  38                 Element* elem = new ElementSet(set);
  39                 eset->add(new OrderElement(item, elem));
  40                 This->solver->allElements.push(elem);
  41                 This->solver->allSets.push(set);
  42                 return elem;
  43         } else
  44                 return eset->get(&oelement)->elem;
  45 }
  46