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 = This->solver->createPredicateOperator(LT, sarray, 2);
  22         Element *parray[] = {elem1, elem2};
  23         Boolean *boolean = This->solver->applyPredicate(predicate, parray, 2);
  24         This->solver->addConstraint(boolean);
  25         This->solver->replaceBooleanWithBoolean(boolOrder, boolean);
  26 }
  27
  28
  29 Element *getOrderIntegerElement(SATEncoder *This,Order *order, uint64_t item) {
  30         HashSetOrderElement *eset = order->elementTable;
  31         OrderElement oelement(item, NULL);
  32         if ( !eset->contains(&oelement)) {
  33                 Set *set = This->solver->createRangeSet(order->set->type, 1, (uint64_t) order->set->getSize());
  34                 Element *elem = This->solver->getElementVar(set);
  35                 eset->add(new OrderElement(item, elem));
  36                 return elem;
  37         } else
  38                 return eset->get(&oelement)->elem;
  39 }
  40