Revert patch to hide symptom of previous bugs

[satune.git] / src / Translator / decomposeorderresolver.cc

diff --git a/src/Translator/decomposeorderresolver.cc b/src/Translator/decomposeorderresolver.cc
index 49d88550a0661a7e1b286f36abedb453807771f7..f226fdaee8100dd7915b101d329f57914fb4f7e4 100644 (file)
--- a/src/Translator/decomposeorderresolver.cc
+++ b/src/Translator/decomposeorderresolver.cc
@@ -1,8 +1,8 @@
 
-/* 
+/*
  * File:   DecomposeOrderResolver.cc
  * Author: hamed
- * 
+ *
  * Created on September 1, 2017, 10:36 AM
  */
 
@@ -11,22 +11,43 @@
 #include "ordernode.h"
 #include "ordergraph.h"
 
-DecomposeOrderResolver::DecomposeOrderResolver(OrderGraph* _graph, Vector<Order*>& _orders):
-       OrderResolver(_graph),
+DecomposeOrderResolver::DecomposeOrderResolver(OrderGraph *_graph, Vector<Order *> &_orders) :
+       graph(_graph),
        orders(_orders.getSize(), _orders.expose())
 {
 }
 
 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);
+bool DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t second) {
+       OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
+       ASSERT(from != NULL);
+       OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
+       ASSERT(to != NULL);
+
+       if (from->sccNum != to->sccNum) {
+               OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
+               if (edge != NULL && edge->mustPos) {
+                       return true;
+               } else if ( edge != NULL && edge->mustNeg) {
+                       return false;
+               } else {
+                       switch (graph->getOrder()->type) {
+                       case SATC_TOTAL:
+                               return from->sccNum < to->sccNum;
+                       case SATC_PARTIAL:
+                       //Adding support for partial order ...
+                       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);
+       }
 }