From: Hamed Date: Thu, 31 Aug 2017 01:45:27 +0000 (-0700) Subject: Adding Transformer and adding integerencoding to it + More OOP X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=be23bdb8eb5460972abf1bb3f426cd7e0ae981bb 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 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 *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 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 2d405e0..bbb59a1 100644 --- 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; iconstraints.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 6434a95..42175b3 100644 --- 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 ee3a427..9615245 100644 --- 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 3069da5..682b0c3 100644 --- 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 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 *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 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 a5f08a3..9850955 100644 --- 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 660005c..362e85b 100644 --- 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 afe905f..b9fa704 100644 --- a/src/Collections/structs.h +++ b/src/Collections/structs.h @@ -25,15 +25,16 @@ typedef HashSet HashSetOrderNode; typedef HashSet HashSetOrderEdge; typedef HashSet HashSetOrderElement; + typedef HashTable HashTableNodeToNodeSet; typedef HashTable HashTableOrderPair; typedef HashTable CloneMap; -typedef HashTable HashTableOrderIntegerEncoding; +typedef HashTable HashTableOrderIntEncoding; typedef HSIterator HSIteratorTableEntry; typedef HSIterator HSIteratorBoolean; typedef HSIterator HSIteratorOrderEdge; typedef HSIterator HSIteratorOrderNode; - +typedef HSIterator HSIteratorOrderElement; #endif diff --git a/src/classlist.h b/src/classlist.h index 7b842ff..641e486 100644 --- 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 e16574f..707ac01 100644 --- 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 63ee0fd..e28052a 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -109,6 +109,7 @@ public: Vector *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