1 #include "integerencoding.h"
2 #include "orderelement.h"
4 #include "satencoder.h"
12 void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
13 Order* order = boolOrder->order;
14 if (order->elementTable == NULL) {
15 order->initializeOrderElementsHashTable();
17 //getting two elements and using LT predicate ...
18 ElementSet* elem1 = (ElementSet*)getOrderIntegerElement(This, order, boolOrder->first);
19 ElementSet* elem2 = (ElementSet*)getOrderIntegerElement(This, order, boolOrder->second);
20 Set * sarray[]={elem1->set, elem2->set};
21 Predicate *predicate =This->solver->createPredicateOperator(LT, sarray, 2);
22 Element * parray[]={elem1, elem2};
23 Boolean * boolean=This->solver->applyPredicate(predicate, parray, 2);
24 This->solver->addConstraint(boolean);
25 This->solver->replaceBooleanWithBoolean(boolOrder, boolean);
29 Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) {
30 HashSetOrderElement* eset = order->elementTable;
31 OrderElement oelement(item, NULL);
32 if( !eset->contains(&oelement)){
33 Set* set = This->solver->createRangeSet(order->set->type, 1, (uint64_t) order->set->getSize());
34 Element* elem = This->solver->getElementVar(set);
35 eset->add(new OrderElement(item, elem));
38 return eset->get(&oelement)->elem;