src/ASTTransform/transform.cc

   1 /*
   2  * To change this license header, choose License Headers in Project Properties.
   3  * To change this template file, choose Tools | Templates
   4  * and open the template in the editor.
   5  */
   6
   7 /*
   8  * File:   transform.cc
   9  * Author: hamed
  10  *
  11  * Created on August 26, 2017, 5:14 PM
  12  */
  13
  14 #include "transform.h"
  15 #include "set.h"
  16 #include "order.h"
  17 #include "satencoder.h"
  18 #include "csolver.h"
  19 #include "integerencodingrecord.h"
  20
  21 Transform::Transform() {
  22         orderIntegerEncoding = new HashTableOrderIntegerEncoding;
  23 }
  24
  25 void Transform:: orderIntegerEncodingSATEncoder(CSolver *This, BooleanOrder *boolOrder) {
  26         Order *order = boolOrder->order;
  27         if (!orderIntegerEncoding->contains(order)) {
  28                 orderIntegerEncoding->put(order, new IntegerEncodingRecord(
  29                 This->createRangeSet(order->set->type, 0, (uint64_t) order->set->getSize()-1)));
  30         }
  31         IntegerEncodingRecord* ierec = orderIntegerEncoding->get(order);
  32         //getting two elements and using LT predicate ...
  33         Element *elem1 = ierec->getOrderIntegerElement(This, boolOrder->first);
  34         Element *elem2 = ierec->getOrderIntegerElement(This, boolOrder->second);
  35         Set *sarray[] = {ierec->set, ierec->set};
  36         Predicate *predicate = This->createPredicateOperator(LT, sarray, 2);
  37         Element *parray[] = {elem1, elem2};
  38         Boolean *boolean = This->applyPredicate(predicate, parray, 2);
  39         This->addConstraint(boolean);
  40         This->replaceBooleanWithBoolean(boolOrder, boolean);
  41 }
  42
  43 Transform::~Transform(){
  44         delete orderIntegerEncoding;
  45 }