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