1 #include "integerencoding.h"
2 #include "orderelement.h"
4 #include "satencoder.h"
11 void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
12 Order* order = boolOrder->order;
13 if (order->elementTable == NULL) {
14 order->initializeOrderElementsHashTable();
16 //getting two elements and using LT predicate ...
17 Element* elem1 = getOrderIntegerElement(This, order, boolOrder->first);
18 Element* elem2 = getOrderIntegerElement(This, order, boolOrder->second);
19 Set * sarray[]={order->auxSet, order->auxSet};
20 Predicate *predicate =new PredicateOperator(LT, sarray, 2);
21 Element * parray[]={elem1, elem2};
22 BooleanPredicate * boolean=new BooleanPredicate(predicate, parray, 2, NULL);
23 {//Adding new elements and boolean/predicate to solver regarding memory management
24 This->solver->allBooleans.push(boolean);
25 This->solver->allPredicates.push(predicate);
26 This->solver->allElements.push(elem1);
27 This->solver->allElements.push(elem2);
28 This->solver->constraints.add(boolean);
30 replaceBooleanWithBoolean(This->solver, boolOrder, boolean);
34 Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) {
35 HashSetOrderElement* eset = order->elementTable;
36 OrderElement oelement ={item, NULL};
37 if( !eset->contains(&oelement)){
38 Element* elem = new ElementSet(order->auxSet);
39 eset->add(allocOrderElement(item, elem));
42 return eset->get(&oelement)->elem;