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 =new PredicateOperator(LT, sarray, 2);
22 Element * parray[]={elem1, elem2};
23 BooleanPredicate * boolean=new BooleanPredicate(predicate, parray, 2, NULL);
24 {//Adding new elements and boolean/predicate to solver regarding memory management
25 This->solver->allBooleans.push(boolean);
26 This->solver->allPredicates.push(predicate);
27 This->solver->constraints.add(boolean);
29 replaceBooleanWithBoolean(This->solver, boolOrder, boolean);
33 Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) {
34 HashSetOrderElement* eset = order->elementTable;
35 OrderElement oelement ={item, NULL};
36 if( !eset->contains(&oelement)){
37 Set* set = new Set(order->set->type, 1, (uint64_t) order->set->getSize());
38 Element* elem = new ElementSet(set);
39 eset->add(allocOrderElement(item, elem));
40 This->solver->allElements.push(elem);
41 This->solver->allSets.push(set);
44 return eset->get(&oelement)->elem;