Adding Transformer and adding integerencoding to it + More OOP

diff --git a/src/ASTTransform/analyzer.cc b/src/ASTTransform/analyzer.cc
deleted file mode 100644 (file)
index cfc01a8..0000000
--- a/src/ASTTransform/analyzer.cc
+++ /dev/null
@@ -1,77 +0,0 @@
-#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 "orderanalysis.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);
-               if (!decompose->canExecuteTransform()){
-                       delete decompose;
-                       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->setOrderGraph(graph);
-               decompose->doTransform();
-               delete decompose;
-               delete graph;
-
-               IntegerEncodingTransform* integerEncoding = new IntegerEncodingTransform(This, order);
-               if(!integerEncoding->canExecuteTransform()){
-                       delete integerEncoding;
-                       continue;
-               }
-               integerEncoding->doTransform();
-               delete integerEncoding;
-       }
-}
-
-

diff --git a/src/ASTTransform/analyzer.h b/src/ASTTransform/analyzer.h
deleted file mode 100644 (file)
index 453e7dc..0000000
--- a/src/ASTTransform/analyzer.h
+++ /dev/null
@@ -1,16 +0,0 @@
-/*
- * 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/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index 2d405e0fe82712f527d05252829793aff4a0c7b8..bbb59a122b9e043c4340a3d0a5da91acbad1509d 100644 (file)
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -6,40 +6,38 @@
 #include "csolver.h"
 #include "integerencodingrecord.h"
 
-HashTableOrderIntegerEncoding* IntegerEncodingTransform::orderIntegerEncoding = new HashTableOrderIntegerEncoding();
 
-IntegerEncodingTransform::IntegerEncodingTransform(CSolver* _solver, Order* _order) 
-       :Transform(_solver),
-       order(_order)
-       
+IntegerEncodingTransform::IntegerEncodingTransform(CSolver* _solver) 
+       :Transform(_solver)
 {      
 }
 
 IntegerEncodingTransform::~IntegerEncodingTransform(){
+       orderIntEncoding->resetanddelete();
 }
 
 bool IntegerEncodingTransform::canExecuteTransform(){
-       return canExecutePass(solver, order->type, ORDERINTEGERENCODING, &offon);
+       return canExecutePass(solver, currOrder->type, ORDERINTEGERENCODING, &offon);
 }
 
 void IntegerEncodingTransform::doTransform(){
-       if (!orderIntegerEncoding->contains(order)) {
-               orderIntegerEncoding->put(order, new IntegerEncodingRecord(
-               solver->createRangeSet(order->set->getType(), 0, (uint64_t) order->set->getSize()-1)));
+       if (!orderIntEncoding->contains(currOrder)) {
+               orderIntEncoding->put(currOrder, new IntegerEncodingRecord(
+               solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->set->getSize()-1)));
        }
-       uint size = order->constraints.getSize();
+       uint size = currOrder->constraints.getSize();
        for(uint i=0; i<size; i++){
-               orderIntegerEncodingSATEncoder(order->constraints.get(i));
+               orderIntegerEncodingSATEncoder(currOrder->constraints.get(i));
        }
 }
 
 
 void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder) {
-       IntegerEncodingRecord* ierec = orderIntegerEncoding->get(order);
+       IntegerEncodingRecord* ierec = orderIntEncoding->get(currOrder);
        //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};
+       Set *sarray[] = {ierec->getSecondarySet(), ierec->getSecondarySet()};
        Predicate *predicate = solver->createPredicateOperator(LT, sarray, 2);
        Element *parray[] = {elem1, elem2};
        Boolean *boolean = solver->applyPredicate(predicate, parray, 2);

diff --git a/src/ASTTransform/integerencoding.h b/src/ASTTransform/integerencoding.h
index 6434a95d903218b64a0d1092041395dd499fdcaf..42175b30f9e40c0db0fc578970c6760297825244 100644 (file)
--- a/src/ASTTransform/integerencoding.h
+++ b/src/ASTTransform/integerencoding.h
@@ -13,16 +13,15 @@
 
 class IntegerEncodingTransform : public Transform{
 public:
-       IntegerEncodingTransform(CSolver* solver, Order* order);
+       IntegerEncodingTransform(CSolver* solver);
        void orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder);
+       void setCurrentOrder(Order* _curr) {currOrder = _curr;}
        void doTransform();
        bool canExecuteTransform();
        virtual ~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;
+       Order* currOrder;
+       HashTableOrderIntEncoding* orderIntEncoding;
 };
 
 

diff --git a/src/ASTTransform/integerencodingrecord.cc b/src/ASTTransform/integerencodingrecord.cc
index ee3a42779b748c532f21bba17132c6fb931cc3f8..961524570d09109c9acf27beaf1d042fa70bff2d 100644 (file)
--- a/src/ASTTransform/integerencodingrecord.cc
+++ b/src/ASTTransform/integerencodingrecord.cc
@@ -10,7 +10,7 @@
 #include "orderelement.h"
 
 IntegerEncodingRecord::IntegerEncodingRecord(Set* _set):
-       set(_set)
+       secondarySet(_set)
 {
        elementTable = new HashSetOrderElement();
 }
@@ -24,10 +24,10 @@ IntegerEncodingRecord::~IntegerEncodingRecord(){
 Element * IntegerEncodingRecord::getOrderIntegerElement(CSolver *This, uint64_t item) {
        OrderElement oelement(item, NULL);
        if ( !elementTable->contains(&oelement)) {
-               Element *elem = This->getElementVar(set);
+               Element *elem = This->getElementVar(secondarySet);
                elementTable->add(new OrderElement(item, elem));
                return elem;
        } else
-               return elementTable->get(&oelement)->elem;
+               return elementTable->get(&oelement)->getElement();
 }
 

diff --git a/src/ASTTransform/integerencodingrecord.h b/src/ASTTransform/integerencodingrecord.h
index 3069da536b6127009f5ba337329e3c5198c48f19..682b0c3867fae96d6054e4a6a3c8ee0baf3869a1 100644 (file)
--- a/src/ASTTransform/integerencodingrecord.h
+++ b/src/ASTTransform/integerencodingrecord.h
@@ -13,13 +13,13 @@
 
 class IntegerEncodingRecord {
 public:
-       Set* set;
        IntegerEncodingRecord(Set* set);
        ~IntegerEncodingRecord();
        Element* getOrderIntegerElement(CSolver *This, uint64_t item);
+       inline Set* getSecondarySet() { return secondarySet; }
        MEMALLOC;
-       
 private:
+       Set* secondarySet;
        HashSetOrderElement *elementTable;
 };
 

diff --git a/src/ASTTransform/transformer.cc b/src/ASTTransform/transformer.cc
new file mode 100644 (file)
index 0000000..03a6841
--- /dev/null
+++ b/src/ASTTransform/transformer.cc
@@ -0,0 +1,85 @@
+#include "transformer.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 "orderanalysis.h"
+#include "tunable.h"
+#include "transform.h"
+#include "element.h"
+#include "integerencoding.h"
+#include "decomposeordertransform.h"
+
+Transformer::Transformer(CSolver *_solver):
+       integerEncoding(new IntegerEncodingTransform(_solver)),
+       solver(_solver)
+{
+}
+
+Transformer::~Transformer(){
+       delete integerEncoding;
+}
+
+void Transformer::orderAnalysis() {
+       Vector<Order *> *orders = solver->getOrders();
+       uint size = orders->getSize();
+       for (uint i = 0; i < size; i++) {
+               Order *order = orders->get(i);
+               DecomposeOrderTransform* decompose = new DecomposeOrderTransform(solver, order);
+               if (!decompose->canExecuteTransform()){
+                       delete decompose;
+                       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(solver->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
+
+               if (mustReachGlobal)
+                       reachMustAnalysis(solver, graph, false);
+
+               bool mustReachLocal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
+
+               if (mustReachLocal) {
+                       //solver pair of analysis is also optional
+                       if (order->type == PARTIAL) {
+                               localMustAnalysisPartial(solver, graph);
+                       } else {
+                               localMustAnalysisTotal(solver, graph);
+                       }
+               }
+
+               bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
+
+               if (mustReachPrune)
+                       removeMustBeTrueNodes(solver, graph);
+
+               //This is needed for splitorder
+               computeStronglyConnectedComponentGraph(graph);
+               decompose->setOrderGraph(graph);
+               decompose->doTransform();
+               delete decompose;
+               delete graph;
+
+               integerEncoding->setCurrentOrder(order);
+               if(!integerEncoding->canExecuteTransform()){
+                       continue;
+               }
+               integerEncoding->doTransform();
+       }
+}
+
+

diff --git a/src/ASTTransform/transformer.h b/src/ASTTransform/transformer.h
new file mode 100644 (file)
index 0000000..24922d0
--- /dev/null
+++ b/src/ASTTransform/transformer.h
@@ -0,0 +1,31 @@
+/*
+ * File:   transformer.h
+ * Author: hamed
+ *
+ * Created on August 24, 2017, 5:33 PM
+ */
+
+#ifndef ORDERDECOMPOSE_H
+#define ORDERDECOMPOSE_H
+#include "classlist.h"
+#include "structs.h"
+#include "transform.h"
+#include "integerencoding.h"
+
+class Transformer{
+public:
+       Transformer(CSolver* solver);
+       ~Transformer();
+       IntegerEncodingTransform* getIntegerEncodingTransform(){ return integerEncoding; }
+       void orderAnalysis();
+private:
+       //For now we can just add transforms here, but in future we may want take a smarter approach.
+       IntegerEncodingTransform* integerEncoding;
+       
+       
+       CSolver* solver;
+};
+
+
+#endif/* ORDERDECOMPOSE_H */
+

diff --git a/src/Backend/orderelement.h b/src/Backend/orderelement.h
index a5f08a3a85f0001c05ba9c9fbebcc694a02c1338..98509558e694a00a03d02c98aa2c4f2f7f47e333 100644 (file)
--- a/src/Backend/orderelement.h
+++ b/src/Backend/orderelement.h
@@ -15,9 +15,13 @@
 class OrderElement {
 public:
        OrderElement(uint64_t item, Element *elem);
+       inline uint getHash() {return (uint) item;}
+       inline bool equals(OrderElement* oe){ return item == oe->item;}
+       inline Element* getElement() { return elem; }
+       MEMALLOC;
+private:
        uint64_t item;
        Element *elem;
-       MEMALLOC;
 };
 
 

diff --git a/src/Collections/structs.cc b/src/Collections/structs.cc
index 660005c787f58497e49de41d0bd0389aaf22a353..362e85b02bbfc7356964ddf88985dfecbef4d41d 100644 (file)
--- a/src/Collections/structs.cc
+++ b/src/Collections/structs.cc
@@ -42,11 +42,11 @@ bool order_edge_equals(OrderEdge *key1, OrderEdge *key2) {
 }
 
 unsigned int order_element_hash_function(OrderElement *This) {
-       return (uint)This->item;
+       return This->getHash();
 }
 
 bool order_element_equals(OrderElement *key1, OrderElement *key2) {
-       return key1->item == key2->item;
+       return key1->equals(key2);
 }
 
 unsigned int order_pair_hash_function(OrderPair *This) {

diff --git a/src/Collections/structs.h b/src/Collections/structs.h
index afe905fb31c350afb7f0e3d0fa82e2b3a0906554..b9fa704d1ce31524f4ed411fe64e96d08457b9c1 100644 (file)
--- a/src/Collections/structs.h
+++ b/src/Collections/structs.h
@@ -25,15 +25,16 @@ typedef HashSet<TableEntry *, uintptr_t, 4, table_entry_hash_function, table_ent
 typedef HashSet<OrderNode *, uintptr_t, 4, order_node_hash_function, order_node_equals> HashSetOrderNode;
 typedef HashSet<OrderEdge *, uintptr_t, 4, order_edge_hash_function, order_edge_equals> HashSetOrderEdge;
 typedef HashSet<OrderElement *, uintptr_t, 4, order_element_hash_function, order_element_equals> HashSetOrderElement;
+
 typedef HashTable<OrderNode *, HashSetOrderNode *, uintptr_t, 4> HashTableNodeToNodeSet;
 typedef HashTable<OrderPair *, OrderPair *, uintptr_t, 4, order_pair_hash_function, order_pair_equals> HashTableOrderPair;
 typedef HashTable<void *, void *, uintptr_t, 4> CloneMap;
-typedef HashTable<Order* , IntegerEncodingRecord*, uintptr_t, 4, order_hash_function, order_pair_equals> HashTableOrderIntegerEncoding; 
+typedef HashTable<Order* , IntegerEncodingRecord*, uintptr_t, 4, order_hash_function, order_pair_equals> HashTableOrderIntEncoding; 
 
 typedef HSIterator<TableEntry *, uintptr_t, 4, table_entry_hash_function, table_entry_equals> HSIteratorTableEntry;
 typedef HSIterator<Boolean *, uintptr_t, 4> HSIteratorBoolean;
 typedef HSIterator<OrderEdge *, uintptr_t, 4, order_edge_hash_function, order_edge_equals> HSIteratorOrderEdge;
 typedef HSIterator<OrderNode *, uintptr_t, 4, order_node_hash_function, order_node_equals> HSIteratorOrderNode;
-
+typedef HSIterator<OrderElement *, uintptr_t, 4, order_element_hash_function, order_element_equals> HSIteratorOrderElement;
 
 #endif

diff --git a/src/classlist.h b/src/classlist.h
index 7b842ffc84a80c9cfce71332f74a6dc7ad4bb309..641e48662206f5ad7ce3afa3a83ce529580e0688 100644 (file)
--- a/src/classlist.h
+++ b/src/classlist.h
@@ -44,6 +44,8 @@ class OrderElement;
 class IntegerEncodingRecord;
 class Transform;
 class Pass;
+class Transformer;
+class AnalysisData;
 
 class ElementEncoding;
 class FunctionEncoding;

diff --git a/src/csolver.cc b/src/csolver.cc
index e16574f20249428eb1ec18c1e96fba8aa2c98d42..707ac01e9fdd1f1cf1e43257a0b3fc805300db81 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -11,7 +11,7 @@
 #include "sattranslator.h"
 #include "tunable.h"
 #include "polarityassignment.h"
-#include "analyzer.h"
+#include "transformer.h"
 #include "autotuner.h"
 
 CSolver::CSolver() :
@@ -20,6 +20,7 @@ CSolver::CSolver() :
        elapsedTime(0)
 {
        satEncoder = new SATEncoder(this);
+       transformer = new Transformer(this);
 }
 
 /** This function tears down the solver and the entire AST */
@@ -61,6 +62,7 @@ CSolver::~CSolver() {
        }
 
        delete satEncoder;
+       delete transformer;
 }
 
 CSolver *CSolver::clone() {
@@ -238,7 +240,7 @@ int CSolver::startEncoding() {
                
        long long startTime = getTimeNano();
        computePolarities(this);
-       orderAnalysis(this);
+       transformer->orderAnalysis();
        naiveEncodingDecision(this);
        satEncoder->encodeAllSATEncoder(this);
        int result = unsat ? IS_UNSAT : satEncoder->solve();

diff --git a/src/csolver.h b/src/csolver.h
index 63ee0fdf057e84b155467f0f66a27105c1ba0813..e28052a389637d7cb9c262d206acf41a086029a4 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -109,6 +109,7 @@ public:
        Vector<Order *> *getOrders() { return &allOrders;}
 
        Tuner *getTuner() { return tuner; }
+       Transformer* getTransformer() {return transformer;}
        
        HSIteratorBoolean *getConstraints() { return constraints.iterator(); }
 
@@ -120,6 +121,7 @@ public:
        CSolver *clone();
        void autoTune(uint budget);
 
+       void setTuner(Transformer * _transformer) {  transformer = _transformer; }
        void setTuner(Tuner * _tuner) { tuner = _tuner; }
        long long getElapsedTime() { return elapsedTime; }
        long long getEncodeTime();
@@ -165,7 +167,7 @@ private:
        SATEncoder *satEncoder;
        bool unsat;
        Tuner *tuner;
-       
+       Transformer* transformer;
        long long elapsedTime;
 };
 #endif