1 #include "integerencoding.h"
2 #include "orderelement.h"
4 #include "satencoder.h"
12 void orderIntegerEncodingSATEncoder(CSolver *solver, 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(solver, order, boolOrder->first);
19 ElementSet *elem2 = (ElementSet *)getOrderIntegerElement(solver, order, boolOrder->second);
20 Set *sarray[] = {elem1->set, elem2->set};
21 Predicate *predicate = solver->createPredicateOperator(LT, sarray, 2);
22 Element *parray[] = {elem1, elem2};
23 Boolean *boolean = solver->applyPredicate(predicate, parray, 2);
24 solver->addConstraint(boolean);
25 solver->replaceBooleanWithBoolean(boolOrder, boolean);
29 Element *getOrderIntegerElement(CSolver * solver, Order *order, uint64_t item) {
30 HashSetOrderElement *eset = order->elementTable;
31 OrderElement oelement(item, NULL);
32 if ( !eset->contains(&oelement)) {
33 Set *set = solver->createRangeSet(order->set->type, 1, (uint64_t) order->set->getSize());
34 Element *elem = solver->getElementVar(set);
35 eset->add(new OrderElement(item, elem));
38 return eset->get(&oelement)->elem;