1 #include "integerencoding.h"
2 #include "orderelement.h"
4 #include "satencoder.h"
10 void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
11 Order* order = boolOrder->order;
12 if (order->elementTable == NULL) {
13 order->initializeOrderElementsHashTable();
15 //getting two elements and using LT predicate ...
16 Element* elem1 = getOrderIntegerElement(This, order, boolOrder->first);
17 Element* elem2 = getOrderIntegerElement(This, order, boolOrder->second);
18 Set * sarray[]={order->auxSet, order->auxSet};
19 Predicate *predicate =new PredicateOperator(LT, sarray, 2);
20 Element * parray[]={elem1, elem2};
21 BooleanPredicate * boolean=new BooleanPredicate(predicate, parray, 2, NULL);
22 {//Adding new elements and boolean/predicate to solver regarding memory management
23 This->solver->allBooleans.push(boolean);
24 This->solver->allPredicates.push(predicate);
25 This->solver->allElements.push(elem1);
26 This->solver->allElements.push(elem2);
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 Element* elem = new ElementSet(order->auxSet);
38 eset->add(allocOrderElement(item, elem));
41 return eset->get(&oelement)->elem;