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 c75fbecd3cdedd5213d9525f0d525d051d03b83f..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
@@ -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();
@@ -354,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();