+Edge orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
+ if(boolOrder->order->graph == NULL){
+ bool doOptOrderStructure=GETVARTUNABLE(This->solver->tuner, boolOrder->order->type,
+ OPTIMIZEORDERSTRUCTURE, &onoff);
+ if (doOptOrderStructure ) {
+ boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
+ reachMustAnalysis(This->solver, boolOrder->order->graph, true);
+ }
+ }
+ Order* order = boolOrder->order;
+ Edge gvalue = inferOrderConstraintFromGraph(order, boolOrder->first, boolOrder->second);
+ if(!edgeIsNull(gvalue))
+ return gvalue;
+
+ if (boolOrder->order->elementTable == NULL) {
+ initializeOrderElementsHashTable(boolOrder->order);
+ }
+ //getting two elements and using LT predicate ...
+ Element* elem1 = getOrderIntegerElement(This, order, boolOrder->first);
+ ElementEncoding *encoding = getElementEncoding(elem1);
+ if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
+ setElementEncodingType(encoding, BINARYINDEX);
+ encodingArrayInitialization(encoding);
+ }
+ Element* elem2 = getOrderIntegerElement(This, order, boolOrder->second);
+ encoding = getElementEncoding(elem2);
+ if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
+ setElementEncodingType(encoding, BINARYINDEX);
+ encodingArrayInitialization(encoding);
+ }
+ Predicate *predicate =allocPredicateOperator(LT, (Set*[]){order->set, order->set}, 2);
+ Boolean * boolean=allocBooleanPredicate(predicate, (Element *[]){elem1,elem2}, 2, NULL);
+ setFunctionEncodingType(getPredicateFunctionEncoding((BooleanPredicate*)boolean), CIRCUIT);
+ {//Adding new elements and boolean/predicate to solver regarding memory management
+ pushVectorBoolean(This->solver->allBooleans, boolean);
+ pushVectorPredicate(This->solver->allPredicates, predicate);
+ pushVectorElement(This->solver->allElements, elem1);
+ pushVectorElement(This->solver->allElements, elem2);
+ }
+ return encodeConstraintSATEncoder(This, boolean);
+}
+
+Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _second){
+ if (order->graph != NULL) {
+ OrderGraph *graph=order->graph;
+ OrderNode *first=lookupOrderNodeFromOrderGraph(graph, _first);
+ OrderNode *second=lookupOrderNodeFromOrderGraph(graph, _second);
+ if ((first != NULL) && (second != NULL)) {
+ OrderEdge *edge=lookupOrderEdgeFromOrderGraph(graph, first, second);
+ if (edge != NULL) {
+ if (edge->mustPos)
+ return E_True;
+ else if (edge->mustNeg)
+ return E_False;
+ }
+ OrderEdge *invedge=getOrderEdgeFromOrderGraph(graph, second, first);
+ if (invedge != NULL) {
+ if (invedge->mustPos)
+ return E_False;
+ else if (invedge->mustNeg)
+ return E_True;
+ }
+ }
+ }
+ return E_NULL;
+}
+
+Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) {
+ HashSetOrderElement* eset = order->elementTable;
+ OrderElement oelement ={item, NULL};
+ if( !containsHashSetOrderElement(eset, &oelement)){
+ Element* elem = allocElementSet(order->set);
+ ElementEncoding* encoding = getElementEncoding(elem);
+ setElementEncodingType(encoding, BINARYINDEX);
+ encodingArrayInitialization(encoding);
+ encodeElementSATEncoder(This, elem);
+ addHashSetOrderElement(eset, allocOrderElement(item, elem));
+ return elem;
+ }else
+ return getHashSetOrderElement(eset, &oelement)->elem;
+}
+Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
+ Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second);
+ if(!edgeIsNull(gvalue))
+ return gvalue;
+
+ HashTableOrderPair *table = order->orderPairTable;