2 #include "integerencoding.h"
5 #include "satencoder.h"
7 #include "integerencodingrecord.h"
9 HashtableOrderIntegerEncoding* IntegerEncodingTransform::orderIntegerEncoding = new HashtableOrderIntegerEncoding();
11 IntegerEncodingTransform::IntegerEncodingTransform(CSolver* _solver, Order* _order)
18 IntegerEncodingTransform::~IntegerEncodingTransform(){
21 bool IntegerEncodingTransform::canExecuteTransform(){
22 return canExecutePass(solver, order->type, ORDERINTEGERENCODING, &offon);
25 void IntegerEncodingTransform::doTransform(){
26 if (!orderIntegerEncoding->contains(order)) {
27 orderIntegerEncoding->put(order, new IntegerEncodingRecord(
28 solver->createRangeSet(order->set->getType(), 0, (uint64_t) order->set->getSize()-1)));
30 uint size = order->constraints.getSize();
31 for(uint i=0; i<size; i++){
32 orderIntegerEncodingSATEncoder(order->constraints.get(i));
37 void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder) {
38 IntegerEncodingRecord* ierec = orderIntegerEncoding->get(order);
39 //getting two elements and using SATC_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(SATC_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);