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
   9 void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
  10         Order* order = boolOrder->order;
  11         if (order->elementTable == NULL) {
  12                 order->initializeOrderElementsHashTable();
  13         }
  14         //getting two elements and using LT predicate ...
  15         Element* elem1 = getOrderIntegerElement(This, order, boolOrder->first);
  16         Element* elem2 = getOrderIntegerElement(This, order, boolOrder->second);
  17         Set * sarray[]={order->auxSet, order->auxSet};
  18         Predicate *predicate =new PredicateOperator(LT, sarray, 2);
  19         Element * parray[]={elem1, elem2};
  20         BooleanPredicate * boolean=new BooleanPredicate(predicate, parray, 2, NULL);
  21         {//Adding new elements and boolean/predicate to solver regarding memory management
  22                 This->solver->allBooleans.push(boolean);
  23                 This->solver->allPredicates.push(predicate);
  24                 This->solver->allElements.push(elem1);
  25                 This->solver->allElements.push(elem2);
  26                 This->solver->constraints.add(boolean);
  27         }
  28 }
  29
  30
  31 Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) {
  32         HashSetOrderElement* eset = order->elementTable;
  33         OrderElement oelement ={item, NULL};
  34         if( !eset->contains(&oelement)){
  35                 Element* elem = new ElementSet(order->auxSet);
  36                 eset->add(allocOrderElement(item, elem));
  37                 return elem;
  38         } else
  39                 return eset->get(&oelement)->elem;
  40 }
  41