src/ASTTransform/integerencoding.cc

   1
   2 #include "integerencoding.h"
   3 #include "set.h"
   4 #include "order.h"
   5 #include "satencoder.h"
   6 #include "csolver.h"
   7 #include "integerencodingrecord.h"
   8
   9 HashTableOrderIntegerEncoding* IntegerEncodingTransform::orderIntegerEncoding = new HashTableOrderIntegerEncoding();
  10
  11 IntegerEncodingTransform::IntegerEncodingTransform(CSolver* _solver, Order* _order, Tunables _tunable, TunableDesc* _desc)
  12         :Transform(_solver, _tunable, _desc),
  13         order(_order)
  14
  15 {
  16 }
  17
  18 IntegerEncodingTransform::~IntegerEncodingTransform(){
  19 }
  20
  21 bool IntegerEncodingTransform::canExecuteTransform(){
  22         return canExecutePass(solver, order->type);
  23 }
  24
  25 void IntegerEncodingTransform::doTransform(){
  26         if (!orderIntegerEncoding->contains(order)) {
  27                 orderIntegerEncoding->put(order, new IntegerEncodingRecord(
  28                 solver->createRangeSet(order->set->type, 0, (uint64_t) order->set->getSize()-1)));
  29         }
  30         uint size = order->constraints.getSize();
  31         for(uint i=0; i<size; i++){
  32                 orderIntegerEncodingSATEncoder(order->constraints.get(i));
  33         }
  34 }
  35
  36
  37 void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder) {
  38         IntegerEncodingRecord* ierec = orderIntegerEncoding->get(order);
  39         //getting two elements and using LT predicate ...
  40         Element *elem1 = ierec->getOrderIntegerElement(solver, boolOrder->first);
  41         Element *elem2 = ierec->getOrderIntegerElement(solver, boolOrder->second);
  42         Set *sarray[] = {ierec->set, ierec->set};
  43         Predicate *predicate = solver->createPredicateOperator(LT, sarray, 2);
  44         Element *parray[] = {elem1, elem2};
  45         Boolean *boolean = solver->applyPredicate(predicate, parray, 2);
  46         solver->addConstraint(boolean);
  47         solver->replaceBooleanWithBoolean(boolOrder, boolean);
  48 }
  49