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