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