Adding checks to avoid further processing on UNSAT Problems

[satune.git] / src / ASTTransform / decomposeordertransform.cc

diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index f629a76b5815a3b8b071e2fcd7162c46295b6e17..eaf81415bdb74a31771ad9c541761d1f78187606 100644 (file)
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -16,6 +16,7 @@
 #include "decomposeorderresolver.h"
 #include "tunable.h"
 #include "orderanalysis.h"
+#include "polarityassignment.h"
 
 
 DecomposeOrderTransform::DecomposeOrderTransform(CSolver *_solver)
@@ -27,6 +28,8 @@ DecomposeOrderTransform::~DecomposeOrderTransform() {
 }
 
 void DecomposeOrderTransform::doTransform() {
+       if(solver->isUnSAT())
+               return;
        HashsetOrder *orders = solver->getActiveOrders()->copy();
        SetIteratorOrder *orderit = orders->iterator();
        while (orderit->hasNext()) {
@@ -153,7 +156,7 @@ void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currG
                        }
                        BooleanEdge neworderconstraint = solver->orderConstraint(neworder, orderconstraint->first, orderconstraint->second);
                        solver->replaceBooleanWithBoolean(orderconstraint, neworderconstraint);
-
+                       updateEdgePolarity(neworderconstraint, orderconstraint);
                        dor->setEdgeOrder(from->getID(), to->getID(), from->sccNum);
                }
        }
@@ -213,6 +216,7 @@ void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode
                        }
                        //Add new order constraint
                        BooleanEdge orderconstraint = solver->orderConstraint(graph->getOrder(), srcNode->getID(), sinkNode->getID());
+                       updateEdgePolarity(orderconstraint, P_TRUE);
                        solver->addConstraint(orderconstraint);
 
                        //Add new edge
@@ -244,7 +248,7 @@ void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode
 void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, DecomposeOrderResolver *dor) {
        SetIteratorOrderNode *iterator = graph->getNodes();
        while (iterator->hasNext()) {
-               OrderNode *node = iterator->next();
+               OrderNode *node = (OrderNode *)iterator->next();
                if (node->removed)
                        continue;
                if (isMustBeTrueNode(node)) {
@@ -257,7 +261,7 @@ void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, Decompose
 void DecomposeOrderTransform::mustEdgePrune(OrderGraph *graph, DecomposeOrderResolver *dor) {
        SetIteratorOrderNode *iterator = graph->getNodes();
        while (iterator->hasNext()) {
-               OrderNode *node = iterator->next();
+               OrderNode *node = (OrderNode *)iterator->next();
                if (node->removed)
                        continue;
                attemptNodeMerge(graph, node, dor);
@@ -325,6 +329,7 @@ void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, Ord
 
                BooleanEdge be = solver->orderConstraint(graph->getOrder(), source->getID(), dstnode->getID());
                BooleanEdge benew = solver->orderConstraint(graph->getOrder(), source->getID(), node->getID());
+               updateEdgePolarity(benew, be);
                solver->replaceBooleanWithBoolean(be, benew);
        }
        dstnode->inEdges.reset();
@@ -339,6 +344,7 @@ void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, Ord
                sink->inEdges.remove(outedge);
                //save the remapping that we did
                dor->remapEdge(dstnode->getID(), sink->getID(), node->getID(), sink->getID());
+
                //create the new edge
                OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(node, sink);
                //update the flags
@@ -353,6 +359,7 @@ void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, Ord
 
                BooleanEdge be = solver->orderConstraint(graph->getOrder(), dstnode->getID(), sink->getID());
                BooleanEdge benew = solver->orderConstraint(graph->getOrder(), node->getID(), sink->getID());
+               updateEdgePolarity(benew, be);
                solver->replaceBooleanWithBoolean(be, benew);
        }
        dstnode->outEdges.reset();