2 #include "integerencoding.h"
5 #include "satencoder.h"
7 #include "integerencodingrecord.h"
8 #include "integerencorderresolver.h"
11 IntegerEncodingTransform::IntegerEncodingTransform(CSolver* _solver)
14 orderIntEncoding = new HashTableOrderIntEncoding();
17 IntegerEncodingTransform::~IntegerEncodingTransform(){
18 orderIntEncoding->resetanddelete();
21 bool IntegerEncodingTransform::canExecuteTransform(){
22 return canExecutePass(solver, currOrder->type, ORDERINTEGERENCODING, &offon);
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);
32 encodingRecord = orderIntEncoding->get(currOrder);
34 uint size = currOrder->constraints.getSize();
35 for(uint i=0; i<size; i++){
36 orderIntegerEncodingSATEncoder(currOrder->constraints.get(i));
38 currOrder->setOrderResolver(new IntegerEncOrderResolver(solver, encodingRecord));
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);