OOP representation of Transforms
authorHamed <hamed.gorjiara@gmail.com>
Tue, 29 Aug 2017 05:16:01 +0000 (22:16 -0700)
committerHamed <hamed.gorjiara@gmail.com>
Tue, 29 Aug 2017 05:16:01 +0000 (22:16 -0700)
14 files changed:
src/ASTTransform/analyzer.cc [new file with mode: 0644]
src/ASTTransform/analyzer.h [new file with mode: 0644]
src/ASTTransform/decomposeordertransform.cc [new file with mode: 0644]
src/ASTTransform/decomposeordertransform.h [new file with mode: 0644]
src/ASTTransform/integerencoding.cc [new file with mode: 0644]
src/ASTTransform/integerencoding.h [new file with mode: 0644]
src/ASTTransform/orderdecompose.cc [deleted file]
src/ASTTransform/orderdecompose.h [deleted file]
src/ASTTransform/pass.cc [new file with mode: 0644]
src/ASTTransform/pass.h [new file with mode: 0644]
src/ASTTransform/transform.cc
src/ASTTransform/transform.h
src/classlist.h
src/csolver.cc

diff --git a/src/ASTTransform/analyzer.cc b/src/ASTTransform/analyzer.cc
new file mode 100644 (file)
index 0000000..fb8fc33
--- /dev/null
@@ -0,0 +1,73 @@
+#include "analyzer.h"
+#include "common.h"
+#include "order.h"
+#include "boolean.h"
+#include "ordergraph.h"
+#include "ordernode.h"
+#include "rewriter.h"
+#include "orderedge.h"
+#include "mutableset.h"
+#include "ops.h"
+#include "csolver.h"
+#include "orderencoder.h"
+#include "tunable.h"
+#include "transform.h"
+#include "element.h"
+#include "integerencoding.h"
+#include "decomposeordertransform.h"
+
+void orderAnalysis(CSolver *This) {
+       Vector<Order *> *orders = This->getOrders();
+       uint size = orders->getSize();
+       for (uint i = 0; i < size; i++) {
+               Order *order = orders->get(i);
+               DecomposeOrderTransform* decompose = new DecomposeOrderTransform(This, order, DECOMPOSEORDER, &onoff);
+               if (!decompose->canExecuteTransform())
+                       continue;
+
+               OrderGraph *graph = buildOrderGraph(order);
+               if (order->type == PARTIAL) {
+                       //Required to do SCC analysis for partial order graphs.  It
+                       //makes sure we don't incorrectly optimize graphs with negative
+                       //polarity edges
+                       completePartialOrderGraph(graph);
+               }
+
+
+               bool mustReachGlobal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
+
+               if (mustReachGlobal)
+                       reachMustAnalysis(This, graph, false);
+
+               bool mustReachLocal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
+
+               if (mustReachLocal) {
+                       //This pair of analysis is also optional
+                       if (order->type == PARTIAL) {
+                               localMustAnalysisPartial(This, graph);
+                       } else {
+                               localMustAnalysisTotal(This, graph);
+                       }
+               }
+
+               bool mustReachPrune = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
+
+               if (mustReachPrune)
+                       removeMustBeTrueNodes(This, graph);
+
+               //This is needed for splitorder
+               computeStronglyConnectedComponentGraph(graph);
+               decompose->doTransform();
+               delete decompose;
+               delete graph;
+
+               
+               IntegerEncodingTransform* integerEncoding = new IntegerEncodingTransform(This, order, ORDERINTEGERENCODING, &offon);
+               if(!integerEncoding->canExecuteTransform())
+                       continue;
+               integerEncoding->doTransform();
+               delete integerEncoding;
+       }
+}
+
+
diff --git a/src/ASTTransform/analyzer.h b/src/ASTTransform/analyzer.h
new file mode 100644 (file)
index 0000000..453e7dc
--- /dev/null
@@ -0,0 +1,16 @@
+/*
+ * File:   analyzer.h
+ * Author: hamed
+ *
+ * Created on August 24, 2017, 5:33 PM
+ */
+
+#ifndef ORDERDECOMPOSE_H
+#define ORDERDECOMPOSE_H
+#include "classlist.h"
+#include "structs.h"
+
+void orderAnalysis(CSolver *This);
+
+#endif/* ORDERDECOMPOSE_H */
+
diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
new file mode 100644 (file)
index 0000000..6df2639
--- /dev/null
@@ -0,0 +1,90 @@
+/* 
+ * File:   ordertransform.cc
+ * Author: hamed
+ * 
+ * Created on August 28, 2017, 10:35 AM
+ */
+
+#include "decomposeordertransform.h"
+#include "order.h"
+#include "orderedge.h"
+#include "ordernode.h"
+#include "boolean.h"
+#include "mutableset.h"
+#include "ordergraph.h"
+#include "csolver.h"
+
+
+DecomposeOrderTransform::DecomposeOrderTransform(CSolver* _solver, Order* _order, Tunables _tunable, TunableDesc* _desc)
+       :Transform(_solver, _tunable, _desc),
+       order(_order)
+{
+}
+
+DecomposeOrderTransform::~DecomposeOrderTransform() {
+}
+
+bool DecomposeOrderTransform::canExecuteTransform(){
+       return canExecutePass(solver, order->type);
+}
+
+void DecomposeOrderTransform::doTransform(){
+       Vector<Order *> ordervec;
+       Vector<Order *> partialcandidatevec;
+       uint size = order->constraints.getSize();
+       for (uint i = 0; i < size; i++) {
+               BooleanOrder *orderconstraint = order->constraints.get(i);
+               OrderNode *from = graph->getOrderNodeFromOrderGraph(orderconstraint->first);
+               OrderNode *to = graph->getOrderNodeFromOrderGraph(orderconstraint->second);
+               model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
+               if (from->sccNum != to->sccNum) {
+                       OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
+                       if (edge->polPos) {
+                               solver->replaceBooleanWithTrue(orderconstraint);
+                       } else if (edge->polNeg) {
+                               solver->replaceBooleanWithFalse(orderconstraint);
+                       } else {
+                               //This case should only be possible if constraint isn't in AST
+                               ASSERT(0);
+                       }
+               } else {
+                       //Build new order and change constraint's order
+                       Order *neworder = NULL;
+                       if (ordervec.getSize() > from->sccNum)
+                               neworder = ordervec.get(from->sccNum);
+                       if (neworder == NULL) {
+                               MutableSet *set = solver->createMutableSet(order->set->type);
+                               neworder = solver->createOrder(order->type, set);
+                               ordervec.setExpand(from->sccNum, neworder);
+                               if (order->type == PARTIAL)
+                                       partialcandidatevec.setExpand(from->sccNum, neworder);
+                               else
+                                       partialcandidatevec.setExpand(from->sccNum, NULL);
+                       }
+                       if (from->status != ADDEDTOSET) {
+                               from->status = ADDEDTOSET;
+                               ((MutableSet *)neworder->set)->addElementMSet(from->id);
+                       }
+                       if (to->status != ADDEDTOSET) {
+                               to->status = ADDEDTOSET;
+                               ((MutableSet *)neworder->set)->addElementMSet(to->id);
+                       }
+                       if (order->type == PARTIAL) {
+                               OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
+                               if (edge->polNeg)
+                                       partialcandidatevec.setExpand(from->sccNum, NULL);
+                       }
+                       orderconstraint->order = neworder;
+                       neworder->addOrderConstraint(orderconstraint);
+               }
+       }
+
+       uint pcvsize = partialcandidatevec.getSize();
+       for (uint i = 0; i < pcvsize; i++) {
+               Order *neworder = partialcandidatevec.get(i);
+               if (neworder != NULL) {
+                       neworder->type = TOTAL;
+                       model_print("i=%u\t", i);
+               }
+       }
+}
diff --git a/src/ASTTransform/decomposeordertransform.h b/src/ASTTransform/decomposeordertransform.h
new file mode 100644 (file)
index 0000000..25aea89
--- /dev/null
@@ -0,0 +1,29 @@
+/* 
+ * File:   ordertransform.h
+ * Author: hamed
+ *
+ * Created on August 28, 2017, 10:35 AM
+ */
+
+#ifndef ORDERTRANSFORM_H
+#define ORDERTRANSFORM_H
+#include "classlist.h"
+#include "transform.h"
+
+
+class DecomposeOrderTransform : public Transform {
+public:
+       DecomposeOrderTransform(CSolver* _solver, Order* order, Tunables _tunable, TunableDesc* _desc);
+       virtual ~DecomposeOrderTransform();
+       void doTransform();
+       void setOrderGraph(OrderGraph* _graph){
+               graph = _graph;
+       }
+       bool canExecuteTransform();
+private:
+       Order* order;
+       OrderGraph* graph;
+};
+
+#endif /* ORDERTRANSFORM_H */
+
diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
new file mode 100644 (file)
index 0000000..b4b0f99
--- /dev/null
@@ -0,0 +1,49 @@
+
+#include "integerencoding.h"
+#include "set.h"
+#include "order.h"
+#include "satencoder.h"
+#include "csolver.h"
+#include "integerencodingrecord.h"
+
+HashTableOrderIntegerEncoding* IntegerEncodingTransform::orderIntegerEncoding = new HashTableOrderIntegerEncoding();
+
+IntegerEncodingTransform::IntegerEncodingTransform(CSolver* _solver, Order* _order, Tunables _tunable, TunableDesc* _desc) 
+       :Transform(_solver, _tunable, _desc),
+       order(_order)
+       
+{      
+}
+
+IntegerEncodingTransform::~IntegerEncodingTransform(){
+}
+
+bool IntegerEncodingTransform::canExecuteTransform(){
+       return canExecutePass(solver, order->type);
+}
+
+void IntegerEncodingTransform::doTransform(){
+       if (!orderIntegerEncoding->contains(order)) {
+               orderIntegerEncoding->put(order, new IntegerEncodingRecord(
+               solver->createRangeSet(order->set->type, 0, (uint64_t) order->set->getSize()-1)));
+       }
+       uint size = order->constraints.getSize();
+       for(uint i=0; i<size; i++){
+               orderIntegerEncodingSATEncoder(order->constraints.get(i));
+       }
+}
+
+
+void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder) {
+       IntegerEncodingRecord* ierec = orderIntegerEncoding->get(order);
+       //getting two elements and using LT predicate ...
+       Element *elem1 = ierec->getOrderIntegerElement(solver, boolOrder->first);
+       Element *elem2 = ierec->getOrderIntegerElement(solver, boolOrder->second);
+       Set *sarray[] = {ierec->set, ierec->set};
+       Predicate *predicate = solver->createPredicateOperator(LT, sarray, 2);
+       Element *parray[] = {elem1, elem2};
+       Boolean *boolean = solver->applyPredicate(predicate, parray, 2);
+       solver->addConstraint(boolean);
+       solver->replaceBooleanWithBoolean(boolOrder, boolean);
+}
+
diff --git a/src/ASTTransform/integerencoding.h b/src/ASTTransform/integerencoding.h
new file mode 100644 (file)
index 0000000..61e1512
--- /dev/null
@@ -0,0 +1,30 @@
+/* 
+ * File:   integerencoding.h
+ * Author: hamed
+ *
+ * Created on August 27, 2017, 4:36 PM
+ */
+
+#ifndef INTEGERENCODING_H
+#define INTEGERENCODING_H
+#include "classlist.h"
+#include "transform.h"
+#include "order.h"
+
+class IntegerEncodingTransform : public Transform{
+public:
+       IntegerEncodingTransform(CSolver* solver, Order* order, Tunables _tunable, TunableDesc* _desc);
+       void orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder);
+       void doTransform();
+       bool canExecuteTransform();
+       ~IntegerEncodingTransform();
+private:
+       Order* order;
+       // In future we can use a singleton class instead of static variable for keeping data that needed
+       // for translating back result
+       static HashTableOrderIntegerEncoding* orderIntegerEncoding;
+};
+
+
+#endif /* INTEGERENCODING_H */
+
diff --git a/src/ASTTransform/orderdecompose.cc b/src/ASTTransform/orderdecompose.cc
deleted file mode 100644 (file)
index ccac62b..0000000
+++ /dev/null
@@ -1,135 +0,0 @@
-#include "orderdecompose.h"
-#include "common.h"
-#include "order.h"
-#include "boolean.h"
-#include "ordergraph.h"
-#include "ordernode.h"
-#include "rewriter.h"
-#include "orderedge.h"
-#include "mutableset.h"
-#include "ops.h"
-#include "csolver.h"
-#include "orderencoder.h"
-#include "tunable.h"
-#include "transform.h"
-#include "element.h"
-
-void orderAnalysis(CSolver *This) {
-       Transform* transform = new Transform();
-       Vector<Order *> *orders = This->getOrders();
-       uint size = orders->getSize();
-       for (uint i = 0; i < size; i++) {
-               Order *order = orders->get(i);
-               bool doDecompose = GETVARTUNABLE(This->getTuner(), order->type, DECOMPOSEORDER, &onoff);
-               if (!doDecompose)
-                       continue;
-
-               OrderGraph *graph = buildOrderGraph(order);
-               if (order->type == PARTIAL) {
-                       //Required to do SCC analysis for partial order graphs.  It
-                       //makes sure we don't incorrectly optimize graphs with negative
-                       //polarity edges
-                       completePartialOrderGraph(graph);
-               }
-
-
-               bool mustReachGlobal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
-
-               if (mustReachGlobal)
-                       reachMustAnalysis(This, graph, false);
-
-               bool mustReachLocal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
-
-               if (mustReachLocal) {
-                       //This pair of analysis is also optional
-                       if (order->type == PARTIAL) {
-                               localMustAnalysisPartial(This, graph);
-                       } else {
-                               localMustAnalysisTotal(This, graph);
-                       }
-               }
-
-               bool mustReachPrune = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
-
-               if (mustReachPrune)
-                       removeMustBeTrueNodes(This, graph);
-
-               //This is needed for splitorder
-               computeStronglyConnectedComponentGraph(graph);
-               decomposeOrder(This, order, graph);
-               delete graph;
-
-               
-               bool doIntegerEncoding = GETVARTUNABLE(This->getTuner(), order->order.type, ORDERINTEGERENCODING, &offon );
-               if(!doIntegerEncoding)
-               continue;
-               uint size = order->constraints.getSize();
-               for(uint i=0; i<size; i++){
-                       transform->orderIntegerEncodingSATEncoder(This, order->constraints.get(i));
-               }
-
-       }
-       delete transform;
-}
-
-void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
-       Vector<Order *> ordervec;
-       Vector<Order *> partialcandidatevec;
-       uint size = order->constraints.getSize();
-       for (uint i = 0; i < size; i++) {
-               BooleanOrder *orderconstraint = order->constraints.get(i);
-               OrderNode *from = graph->getOrderNodeFromOrderGraph(orderconstraint->first);
-               OrderNode *to = graph->getOrderNodeFromOrderGraph(orderconstraint->second);
-               model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
-               if (from->sccNum != to->sccNum) {
-                       OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
-                       if (edge->polPos) {
-                               This->replaceBooleanWithTrue(orderconstraint);
-                       } else if (edge->polNeg) {
-                               This->replaceBooleanWithFalse(orderconstraint);
-                       } else {
-                               //This case should only be possible if constraint isn't in AST
-                               ASSERT(0);
-                       }
-               } else {
-                       //Build new order and change constraint's order
-                       Order *neworder = NULL;
-                       if (ordervec.getSize() > from->sccNum)
-                               neworder = ordervec.get(from->sccNum);
-                       if (neworder == NULL) {
-                               MutableSet *set = This->createMutableSet(order->set->type);
-                               neworder = This->createOrder(order->type, set);
-                               ordervec.setExpand(from->sccNum, neworder);
-                               if (order->type == PARTIAL)
-                                       partialcandidatevec.setExpand(from->sccNum, neworder);
-                               else
-                                       partialcandidatevec.setExpand(from->sccNum, NULL);
-                       }
-                       if (from->status != ADDEDTOSET) {
-                               from->status = ADDEDTOSET;
-                               ((MutableSet *)neworder->set)->addElementMSet(from->id);
-                       }
-                       if (to->status != ADDEDTOSET) {
-                               to->status = ADDEDTOSET;
-                               ((MutableSet *)neworder->set)->addElementMSet(to->id);
-                       }
-                       if (order->type == PARTIAL) {
-                               OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
-                               if (edge->polNeg)
-                                       partialcandidatevec.setExpand(from->sccNum, NULL);
-                       }
-                       orderconstraint->order = neworder;
-                       neworder->addOrderConstraint(orderconstraint);
-               }
-       }
-
-       uint pcvsize = partialcandidatevec.getSize();
-       for (uint i = 0; i < pcvsize; i++) {
-               Order *neworder = partialcandidatevec.get(i);
-               if (neworder != NULL) {
-                       neworder->type = TOTAL;
-                       model_print("i=%u\t", i);
-               }
-       }
-}
-
diff --git a/src/ASTTransform/orderdecompose.h b/src/ASTTransform/orderdecompose.h
deleted file mode 100644 (file)
index 85a5481..0000000
+++ /dev/null
@@ -1,23 +0,0 @@
-/*
- * To change this license header, choose License Headers in Project Properties.
- * To change this template file, choose Tools | Templates
- * and open the template in the editor.
- */
-
-/*
- * File:   orderdecompose.h
- * Author: hamed
- *
- * Created on August 24, 2017, 5:33 PM
- */
-
-#ifndef ORDERDECOMPOSE_H
-#define ORDERDECOMPOSE_H
-#include "classlist.h"
-#include "structs.h"
-
-void orderAnalysis(CSolver *This);
-void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph);
-
-#endif/* ORDERDECOMPOSE_H */
-
diff --git a/src/ASTTransform/pass.cc b/src/ASTTransform/pass.cc
new file mode 100644 (file)
index 0000000..b774ceb
--- /dev/null
@@ -0,0 +1,14 @@
+#include "pass.h"
+#include "tunable.h"
+#include "csolver.h"
+
+Pass::Pass(Tunables _tunable, TunableDesc* _desc): 
+       tunable(_tunable),
+       tunableDesc(_desc)
+{
+       
+}
+
+Pass::~Pass(){
+       
+}
diff --git a/src/ASTTransform/pass.h b/src/ASTTransform/pass.h
new file mode 100644 (file)
index 0000000..2d5c84e
--- /dev/null
@@ -0,0 +1,31 @@
+/* 
+ * File:   pass.h
+ * Author: hamed
+ *
+ * Created on August 28, 2017, 6:23 PM
+ */
+
+#ifndef PASS_H
+#define PASS_H
+#include "classlist.h"
+#include "mymemory.h"
+#include "structs.h"
+#include "tunable.h"
+#include "csolver.h"
+
+class Pass{
+public:
+       Pass(Tunables _tunable, TunableDesc* _desc);
+       virtual ~Pass();
+       virtual inline bool canExecutePass(CSolver* This, uint type=0){
+               return GETVARTUNABLE(This->getTuner(), type, tunable, tunableDesc);
+       }
+       MEMALLOC;
+protected:
+       Tunables tunable;
+       TunableDesc* tunableDesc;
+};
+
+
+#endif /* PASS_H */
+
index 312b450..d28980e 100644 (file)
@@ -1,9 +1,3 @@
-/*
- * To change this license header, choose License Headers in Project Properties.
- * To change this template file, choose Tools | Templates
- * and open the template in the editor.
- */
-
 /* 
  * File:   transform.cc
  * Author: hamed
  */
 
 #include "transform.h"
-#include "set.h"
-#include "order.h"
-#include "satencoder.h"
-#include "csolver.h"
-#include "integerencodingrecord.h"
-
-Transform::Transform() {
-       orderIntegerEncoding = new HashTableOrderIntegerEncoding;
-}
 
-void Transform:: orderIntegerEncodingSATEncoder(CSolver *This, BooleanOrder *boolOrder) {
-       Order *order = boolOrder->order;
-       if (!orderIntegerEncoding->contains(order)) {
-               orderIntegerEncoding->put(order, new IntegerEncodingRecord(
-               This->createRangeSet(order->set->type, 0, (uint64_t) order->set->getSize()-1)));
-       }
-       IntegerEncodingRecord* ierec = orderIntegerEncoding->get(order);
-       //getting two elements and using LT predicate ...
-       Element *elem1 = ierec->getOrderIntegerElement(This, boolOrder->first);
-       Element *elem2 = ierec->getOrderIntegerElement(This, boolOrder->second);
-       Set *sarray[] = {ierec->set, ierec->set};
-       Predicate *predicate = This->createPredicateOperator(LT, sarray, 2);
-       Element *parray[] = {elem1, elem2};
-       Boolean *boolean = This->applyPredicate(predicate, parray, 2);
-       This->addConstraint(boolean);
-       This->replaceBooleanWithBoolean(boolOrder, boolean);
+Transform::Transform(CSolver* _solver, Tunables _tunable, TunableDesc* _desc):
+       Pass(_tunable, _desc)
+{
+       solver = _solver;
 }
 
 Transform::~Transform(){
-       delete orderIntegerEncoding;
 }
index 44b431a..65d8119 100644 (file)
 #include "classlist.h"
 #include "mymemory.h"
 #include "structs.h"
+#include "pass.h"
 
-class Transform {
+class Transform : public Pass{
 public:
-       Transform();
-       ~Transform();
-       void orderIntegerEncodingSATEncoder(CSolver *This, BooleanOrder *boolOrder);
-       MEMALLOC;
-private:
-       HashTableOrderIntegerEncoding* orderIntegerEncoding;
+       Transform(CSolver* _solver,Tunables _tunable, TunableDesc* _desc);
+       virtual ~Transform();
+       virtual bool canExecuteTransform() = 0;
+       virtual void doTransform() = 0;
+protected:
+       // Need solver for translating back the result ...
+       CSolver* solver;
 };
 
 #endif /* TRANSFORM_H */
index 4b19649..e032cd5 100644 (file)
@@ -54,6 +54,8 @@ class OrderGraph;
 class OrderNode;
 class OrderEdge;
 
+class Pass;
+class Transform;
 
 struct IncrementalSolver;
 typedef struct IncrementalSolver IncrementalSolver;
index d825df5..814a140 100644 (file)
@@ -11,7 +11,7 @@
 #include "sattranslator.h"
 #include "tunable.h"
 #include "polarityassignment.h"
-#include "orderdecompose.h"
+#include "analyzer.h"
 
 CSolver::CSolver() : unsat(false) {
        tuner = new Tuner();