#include "predicate.h"
#include "element.h"
#include "rewriter.h"
+#include "set.h"
+
-/*
void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
Order* order = boolOrder->order;
if (order->elementTable == NULL) {
order->initializeOrderElementsHashTable();
}
//getting two elements and using LT predicate ...
- Element* elem1 = getOrderIntegerElement(This, order, boolOrder->first);
- Element* elem2 = getOrderIntegerElement(This, order, boolOrder->second);
- Set * sarray[]={order->auxSet, order->auxSet};
+ ElementSet* elem1 = (ElementSet*)getOrderIntegerElement(This, order, boolOrder->first);
+ ElementSet* elem2 = (ElementSet*)getOrderIntegerElement(This, order, boolOrder->second);
+ Set * sarray[]={elem1->set, elem2->set};
Predicate *predicate =new PredicateOperator(LT, sarray, 2);
Element * parray[]={elem1, elem2};
BooleanPredicate * boolean=new BooleanPredicate(predicate, parray, 2, NULL);
{//Adding new elements and boolean/predicate to solver regarding memory management
This->solver->allBooleans.push(boolean);
This->solver->allPredicates.push(predicate);
- This->solver->allElements.push(elem1);
- This->solver->allElements.push(elem2);
This->solver->constraints.add(boolean);
}
replaceBooleanWithBoolean(This->solver, boolOrder, boolean);
HashSetOrderElement* eset = order->elementTable;
OrderElement oelement ={item, NULL};
if( !eset->contains(&oelement)){
- Element* elem = new ElementSet(order->auxSet);
+ Set* set = new Set(order->set->type, 1, (uint64_t) order->set->getSize());
+ Element* elem = new ElementSet(set);
eset->add(allocOrderElement(item, elem));
+ This->solver->allElements.push(elem);
+ This->solver->allSets.push(set);
return elem;
} else
return eset->get(&oelement)->elem;
}
-*/
#include "csolver.h"
#include "orderencoder.h"
#include "tunable.h"
+#include "integerencoding.h"
void orderAnalysis(CSolver *This) {
uint size = This->allOrders.getSize();
//This is needed for splitorder
computeStronglyConnectedComponentGraph(graph);
-
decomposeOrder(This, order, graph);
-
deleteOrderGraph(graph);
+
+ bool doIntegerEncoding = GETVARTUNABLE(This->tuner, order->order.type, ORDERINTEGERENCODING, &onoff );
+ if(!doIntegerEncoding)
+ continue;
+ uint size = order->constraints.getSize();
+ for(uint i=0; i<size; i++){
+ orderIntegerEncodingSATEncoder(This->satEncoder, order->constraints.get(i));
+ }
+
}
}