Merging with branch Master

diff --git a/src/ASTTransform/analyzer.cc b/src/ASTTransform/analyzer.cc
deleted file mode 100644 (file)
index 05329a5..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 == SATC_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 == SATC_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 d15c60e365798254924277c8fd77c0fe86935359..411ddc9ddafeab489c9ce3e0b368c8d67847562a 100644 (file)
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -6,40 +6,39 @@
 #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)
 {      
+       orderIntEncoding = new HashTableOrderIntEncoding();
 }
 
 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);
-       //getting two elements and using SATC_LT predicate ...
+       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(SATC_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 858f7ad08da009ba9418954b07b6a2526a0d2767..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 6589df76df30f22a3e4cc80cbcdbe8d79cbcd863..7085cf7f9c5e7d916d2c92d941122f28dc6ba133 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 bafc01812314ad943b79adb2fe9cb44063b5adf1..2b2f1902b7faf94b192015241f3ebd4fd00941f2 100644 (file)
--- a/src/ASTTransform/integerencodingrecord.h
+++ b/src/ASTTransform/integerencodingrecord.h
@@ -13,13 +13,14 @@
 
 class IntegerEncodingRecord {
 public:
-       Set* set;
        IntegerEncodingRecord(Set* set);
        ~IntegerEncodingRecord();
        Element* getOrderIntegerElement(CSolver *This, uint64_t item);
+       inline Set* getSecondarySet() { return secondarySet; }
        CMEMALLOC;
        
 private:
+       Set* secondarySet;
        HashsetOrderElement *elementTable;
 };
 

diff --git a/src/ASTTransform/transformer.cc b/src/ASTTransform/transformer.cc
new file mode 100644 (file)
index 0000000..b22b87d
--- /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 == SATC_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) {
+                       //This pair of analysis is also optional
+                       if (order->type == SATC_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 ab2ef7916d85bc6dc67bcaf614815b3e3f2e8b0b..07913c9aa4fd5a85be0fbe2d2d99d0abec752c43 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; }
+       CMEMALLOC;
+private:
        uint64_t item;
        Element *elem;
-       CMEMALLOC;
 };
 
 

diff --git a/src/Collections/structs.cc b/src/Collections/structs.cc
index 36f95b4c1444f4249e66b61dd4dd748965d9be45..96b85e7dc1aedb6fd9ae8228ed63f31582777af4 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 d0c9185857ed489330263a2c00c9d29b7f2bbe6d..c2ed0e9201ae6a12aef16550e0c85cbf002d0a29 100644 (file)
--- a/src/Collections/structs.h
+++ b/src/Collections/structs.h
@@ -19,19 +19,19 @@ unsigned int order_pair_hash_function(OrderPair *This);
 bool order_pair_equals(OrderPair *key1, OrderPair *key2);
 
 
-
 typedef Hashset<TableEntry *, uintptr_t, 4, table_entry_hash_function, table_entry_equals> HashsetTableEntry;
 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> HashtableOrderIntegerEncoding; 
+typedef Hashtable<Order* , IntegerEncodingRecord*, uintptr_t, 4> HashTableOrderIntEncoding; 
 
 typedef SetIterator<TableEntry *, uintptr_t, 4, table_entry_hash_function, table_entry_equals> SetIteratorTableEntry;
 typedef SetIterator<OrderEdge *, uintptr_t, 4, order_edge_hash_function, order_edge_equals> SetIteratorOrderEdge;
 typedef SetIterator<OrderNode *, uintptr_t, 4, order_node_hash_function, order_node_equals> SetIteratorOrderNode;
-
+typedef SetIterator<OrderElement *, uintptr_t, 4, order_element_hash_function, order_element_equals> SetIteratorOrderElement;
 
 #endif

diff --git a/src/classes.h b/src/classes.h
index fe2eab5f9ca0af16a3548cf114e9b2c7d8d00ae0..37694398f69271a16014e92b321bb2d3bf083ca5 100644 (file)
--- a/src/classes.h
+++ b/src/classes.h
@@ -23,6 +23,7 @@ class Order;
 class MutableSet;
 class Function;
 class Tuner;
+class Transformer;
 class Set;
 class BooleanLogic;
 typedef uint64_t VarType;

diff --git a/src/classlist.h b/src/classlist.h
index 35370e1a1a5c21681bf562191d0f485c6c1d06bc..e8ab113ab24e360a552c159d3a4c4d9d5b0c4586 100644 (file)
--- a/src/classlist.h
+++ b/src/classlist.h
@@ -42,6 +42,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 5ee5157d31f29246f3d6dddd0c7058947d217e6f..3d589b18f94da8668ecfc1233eef4c05ee3ee243 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"
 #include "astops.h"
 #include "structs.h"
@@ -24,6 +24,7 @@ CSolver::CSolver() :
        elapsedTime(0)
 {
        satEncoder = new SATEncoder(this);
+       transformer = new Transformer(this);
 }
 
 /** This function tears down the solver and the entire AST */
@@ -67,6 +68,7 @@ CSolver::~CSolver() {
        delete boolTrue;
        delete boolFalse;
        delete satEncoder;
+       delete transformer;
 }
 
 CSolver *CSolver::clone() {
@@ -357,7 +359,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 85da23e117e8c0e5b4f5c699bbc4f16209b8a3fc..a067b2fa1cb1495c7a4bba4329534e88efea5974 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -113,6 +113,7 @@ public:
        Vector<Order *> *getOrders() { return &allOrders;}
 
        Tuner *getTuner() { return tuner; }
+       Transformer* getTransformer() {return transformer;}
        
        SetIteratorBoolean *getConstraints() { return constraints.iterator(); }
 
@@ -124,6 +125,7 @@ public:
        CSolver *clone();
        void autoTune(uint budget);
 
+       void setTransformer(Transformer * _transformer) {  transformer = _transformer; }
        void setTuner(Tuner * _tuner) { tuner = _tuner; }
        long long getElapsedTime() { return elapsedTime; }
        long long getEncodeTime();
@@ -172,7 +174,7 @@ private:
        SATEncoder *satEncoder;
        bool unsat;
        Tuner *tuner;
-       
+       Transformer* transformer;
        long long elapsedTime;
 };
 #endif