Editing orderresolver design
[satune.git] / src / Translator / decomposeorderresolver.cc
index 49d88550a0661a7e1b286f36abedb453807771f7..61152958cd8bbfe4616024dfb979346424a306f9 100644 (file)
@@ -12,7 +12,7 @@
 #include "ordergraph.h"
 
 DecomposeOrderResolver::DecomposeOrderResolver(OrderGraph* _graph, Vector<Order*>& _orders):
-       OrderResolver(_graph),
+       graph(_graph),
        orders(_orders.getSize(), _orders.expose())
 {
 }
@@ -21,12 +21,36 @@ DecomposeOrderResolver::~DecomposeOrderResolver() {
        delete graph;
 }
 
-HappenedBefore DecomposeOrderResolver::getOrder(OrderNode* from, OrderNode* to){
-       ASSERT(from->id == to->id);
-       // We should ask this query from the suborder ....
-       Order *suborder = NULL;
-       suborder = orders.get(from->sccNum);
-       ASSERT(suborder != NULL);
-       return suborder->encoding.resolver->resolveOrder(from->id, to->id);
+HappenedBefore DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t second){
+       OrderNode *from = graph->getOrderNodeFromOrderGraph(first, false /*Don't create new node if doesn't exist*/);
+       if(from == NULL){
+               return SATC_UNORDERED;
+       }
+       OrderNode *to = graph->getOrderNodeFromOrderGraph(second, false);
+       if(from == NULL){
+               return SATC_UNORDERED;
+       }
+       if (from->sccNum != to->sccNum) {
+               OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to, false /* Don't create a new edge*/);
+               if (edge != NULL && edge->mustPos){
+                       return SATC_FIRST;
+               } else if( edge != NULL && edge->mustNeg){
+                       return SATC_SECOND;
+               }else {
+                       switch(graph->getOrder()->encoding.type){
+                               case SATC_TOTAL:
+                                       return from->sccNum < to->sccNum? SATC_FIRST: SATC_SECOND;
+                               case SATC_PARTIAL:
+                               default:
+                                       ASSERT(0);
+                       }       
+               }
+       } else {
+               Order *suborder = NULL;
+               // We should ask this query from the suborder ....
+               suborder = orders.get(from->sccNum);
+               ASSERT(suborder != NULL);
+               return suborder->encoding.resolver->resolveOrder(from->id, to->id);
+       }
 }