+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){