From be23bdb8eb5460972abf1bb3f426cd7e0ae981bb Mon Sep 17 00:00:00 2001 From: Hamed Date: Wed, 30 Aug 2017 18:45:27 -0700 Subject: [PATCH] Adding Transformer and adding integerencoding to it + More OOP --- src/ASTTransform/analyzer.h | 16 -------- src/ASTTransform/integerencoding.cc | 24 ++++++------ src/ASTTransform/integerencoding.h | 9 ++--- src/ASTTransform/integerencodingrecord.cc | 6 +-- src/ASTTransform/integerencodingrecord.h | 4 +- .../{analyzer.cc => transformer.cc} | 38 +++++++++++-------- src/ASTTransform/transformer.h | 31 +++++++++++++++ src/Backend/orderelement.h | 6 ++- src/Collections/structs.cc | 4 +- src/Collections/structs.h | 5 ++- src/classlist.h | 2 + src/csolver.cc | 6 ++- src/csolver.h | 4 +- 13 files changed, 93 insertions(+), 62 deletions(-) delete mode 100644 src/ASTTransform/analyzer.h rename src/ASTTransform/{analyzer.cc => transformer.cc} (60%) create mode 100644 src/ASTTransform/transformer.h 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/analyzer.cc b/src/ASTTransform/transformer.cc similarity index 60% rename from src/ASTTransform/analyzer.cc rename to src/ASTTransform/transformer.cc index cfc01a8..03a6841 100644 --- a/src/ASTTransform/analyzer.cc +++ b/src/ASTTransform/transformer.cc @@ -1,4 +1,4 @@ -#include "analyzer.h" +#include "transformer.h" #include "common.h" #include "order.h" #include "boolean.h" @@ -16,12 +16,22 @@ #include "integerencoding.h" #include "decomposeordertransform.h" -void orderAnalysis(CSolver *This) { - Vector *orders = This->getOrders(); +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(This, order); + DecomposeOrderTransform* decompose = new DecomposeOrderTransform(solver, order); if (!decompose->canExecuteTransform()){ delete decompose; continue; @@ -36,26 +46,26 @@ void orderAnalysis(CSolver *This) { } - bool mustReachGlobal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHGLOBAL, &onoff); + bool mustReachGlobal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHGLOBAL, &onoff); if (mustReachGlobal) - reachMustAnalysis(This, graph, false); + reachMustAnalysis(solver, graph, false); - bool mustReachLocal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHLOCAL, &onoff); + bool mustReachLocal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHLOCAL, &onoff); if (mustReachLocal) { - //This pair of analysis is also optional + //solver pair of analysis is also optional if (order->type == PARTIAL) { - localMustAnalysisPartial(This, graph); + localMustAnalysisPartial(solver, graph); } else { - localMustAnalysisTotal(This, graph); + localMustAnalysisTotal(solver, graph); } } - bool mustReachPrune = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHPRUNE, &onoff); + bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff); if (mustReachPrune) - removeMustBeTrueNodes(This, graph); + removeMustBeTrueNodes(solver, graph); //This is needed for splitorder computeStronglyConnectedComponentGraph(graph); @@ -64,13 +74,11 @@ void orderAnalysis(CSolver *This) { delete decompose; delete graph; - IntegerEncodingTransform* integerEncoding = new IntegerEncodingTransform(This, order); + integerEncoding->setCurrentOrder(order); if(!integerEncoding->canExecuteTransform()){ - delete integerEncoding; continue; } integerEncoding->doTransform(); - delete integerEncoding; } } 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 -- 2.34.1