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