src/ASTTransform/integerencoding.cc

   1 #include "integerencoding.h"
   2 #include "set.h"
   3 #include "order.h"
   4 #include "satencoder.h"
   5 #include "csolver.h"
   6 #include "integerencodingrecord.h"
   7 #include "integerencorderresolver.h"
   8 #include "tunable.h"
   9
  10 IntegerEncodingTransform::IntegerEncodingTransform(CSolver *_solver)
  11         : Transform(_solver)
  12 {
  13         orderIntEncoding = new HashTableOrderIntEncoding();
  14 }
  15
  16 IntegerEncodingTransform::~IntegerEncodingTransform() {
  17         orderIntEncoding->resetanddelete();
  18 }
  19
  20 void IntegerEncodingTransform::doTransform() {
  21         Vector<Order *> *orders = solver->getOrders();
  22         uint size = orders->getSize();
  23         for (uint i = 0; i < size; i++) {
  24                 Order *order = orders->get(i);
  25                 if (GETVARTUNABLE(solver->getTuner(), order->type, ORDERINTEGERENCODING, &onoff))
  26                         integerEncode(order);
  27         }
  28 }
  29
  30 void IntegerEncodingTransform::integerEncode(Order *currOrder) {
  31         IntegerEncodingRecord *encodingRecord = NULL;
  32         if (!orderIntEncoding->contains(currOrder)) {
  33                 encodingRecord = new IntegerEncodingRecord(
  34                         solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->set->getSize() - 1));
  35                 orderIntEncoding->put(currOrder, encodingRecord);
  36         } else {
  37                 encodingRecord = orderIntEncoding->get(currOrder);
  38         }
  39         uint size = currOrder->constraints.getSize();
  40         for (uint i = 0; i < size; i++) {
  41                 orderIntegerEncodingSATEncoder(currOrder->constraints.get(i));
  42         }
  43         currOrder->setOrderResolver(new IntegerEncOrderResolver(solver, encodingRecord));
  44 }
  45
  46
  47 void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder) {
  48         IntegerEncodingRecord *ierec = orderIntEncoding->get(currOrder);
  49         //getting two elements and using LT predicate ...
  50         Element *elem1 = ierec->getOrderIntegerElement(solver, boolOrder->first);
  51         Element *elem2 = ierec->getOrderIntegerElement(solver, boolOrder->second);
  52         Set *sarray[] = {ierec->getSecondarySet(), ierec->getSecondarySet()};
  53         Predicate *predicate = solver->createPredicateOperator(SATC_LT, sarray, 2);
  54         Element *parray[] = {elem1, elem2};
  55         Boolean *boolean = solver->applyPredicate(predicate, parray, 2);
  56         solver->addConstraint(boolean);
  57         solver->replaceBooleanWithBoolean(boolOrder, boolean);
  58 }
  59