Adding Transformer and adding integerencoding to it + More OOP
authorHamed <hamed.gorjiara@gmail.com>
Thu, 31 Aug 2017 01:45:27 +0000 (18:45 -0700)
committerHamed <hamed.gorjiara@gmail.com>
Thu, 31 Aug 2017 01:45:27 +0000 (18:45 -0700)
14 files changed:
src/ASTTransform/analyzer.cc [deleted file]
src/ASTTransform/analyzer.h [deleted file]
src/ASTTransform/integerencoding.cc
src/ASTTransform/integerencoding.h
src/ASTTransform/integerencodingrecord.cc
src/ASTTransform/integerencodingrecord.h
src/ASTTransform/transformer.cc [new file with mode: 0644]
src/ASTTransform/transformer.h [new file with mode: 0644]
src/Backend/orderelement.h
src/Collections/structs.cc
src/Collections/structs.h
src/classlist.h
src/csolver.cc
src/csolver.h

diff --git a/src/ASTTransform/analyzer.cc b/src/ASTTransform/analyzer.cc
deleted file mode 100644 (file)
index cfc01a8..0000000
+++ /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
+++ /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 */
-
index 2d405e0..bbb59a1 100644 (file)
@@ -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);
index 6434a95..42175b3 100644 (file)
 
 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;
 };
 
 
index ee3a427..9615245 100644 (file)
@@ -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();
 }
 
index 3069da5..682b0c3 100644 (file)
 
 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
@@ -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
@@ -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 */
+
index a5f08a3..9850955 100644 (file)
 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;
 };
 
 
index 660005c..362e85b 100644 (file)
@@ -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) {
index afe905f..b9fa704 100644 (file)
@@ -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
index 7b842ff..641e486 100644 (file)
@@ -44,6 +44,8 @@ class OrderElement;
 class IntegerEncodingRecord;
 class Transform;
 class Pass;
+class Transformer;
+class AnalysisData;
 
 class ElementEncoding;
 class FunctionEncoding;
index e16574f..707ac01 100644 (file)
@@ -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();
index 63ee0fd..e28052a 100644 (file)
@@ -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