Adding timeout for Alloy interpreter

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

diff --git a/src/ASTTransform/decomposeordertransform.h b/src/ASTTransform/decomposeordertransform.h
index 25aea89d4f0c797fa8d7baecafd3f523222550f9..9020e1cd3938ff90e1d184ab4503e4579556b406 100644 (file)
--- a/src/ASTTransform/decomposeordertransform.h
+++ b/src/ASTTransform/decomposeordertransform.h
@@ -1,4 +1,4 @@
-/* 
+/*
  * File:   ordertransform.h
  * Author: hamed
  *
@@ -13,17 +13,22 @@
 
 class DecomposeOrderTransform : public Transform {
 public:
-       DecomposeOrderTransform(CSolver* _solver, Order* order, Tunables _tunable, TunableDesc* _desc);
-       virtual ~DecomposeOrderTransform();
+       DecomposeOrderTransform(CSolver *_solver);
+       ~DecomposeOrderTransform();
        void doTransform();
-       void setOrderGraph(OrderGraph* _graph){
-               graph = _graph;
-       }
-       bool canExecuteTransform();
+
+       CMEMALLOC;
 private:
-       Order* order;
-       OrderGraph* graph;
+       bool isMustBeTrueNode(OrderNode *node);
+       void bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor);
+       void decomposeOrder(Order *currOrder, OrderGraph *currGraph, DecomposeOrderResolver *dor);
+       void removeMustBeTrueNodes(OrderGraph *graph, DecomposeOrderResolver *dor);
+       void mustEdgePrune(OrderGraph *graph, DecomposeOrderResolver *dor);
+       void attemptNodeMerge(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor);
+       void mergeNodes(OrderGraph *graph, OrderNode *node, OrderEdge *edge, OrderNode *dstnode, DecomposeOrderResolver *dor);
 };
 
-#endif /* ORDERTRANSFORM_H */
+
+
+#endif/* ORDERTRANSFORM_H */