type(_type),
set(_set),
orderPairTable(NULL),
- elementTable(NULL),
graph(NULL),
order(this)
{
orderPairTable = new HashTableOrderPair();
}
-void Order::initializeOrderElementsHashTable() {
- elementTable = new HashSetOrderElement();
-}
void Order::addOrderConstraint(BooleanOrder *constraint) {
constraints.push(constraint);
orderPairTable->resetanddelete();
delete orderPairTable;
}
- if (elementTable != NULL) {
- delete elementTable;
- }
+
if (graph != NULL) {
delete graph;
}
OrderType type;
Set *set;
HashTableOrderPair *orderPairTable;
- HashSetOrderElement *elementTable;
OrderGraph *graph;
Order *clone(CSolver *solver, CloneMap *map);
Vector<BooleanOrder *> constraints;
--- /dev/null
+#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;*/
+ }
+}
+
+
--- /dev/null
+/*
+ * 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 */
+
--- /dev/null
+/*
+ * File: ordertransform.cc
+ * Author: hamed
+ *
+ * Created on August 28, 2017, 10:35 AM
+ */
+
+#include "decomposeordertransform.h"
+#include "order.h"
+#include "orderedge.h"
+#include "ordernode.h"
+#include "boolean.h"
+#include "mutableset.h"
+#include "ordergraph.h"
+#include "csolver.h"
+
+
+DecomposeOrderTransform::DecomposeOrderTransform(CSolver* _solver, Order* _order)
+ :Transform(_solver),
+ order(_order)
+{
+}
+
+DecomposeOrderTransform::~DecomposeOrderTransform() {
+}
+
+bool DecomposeOrderTransform::canExecuteTransform(){
+ return canExecutePass(solver, order->type, DECOMPOSEORDER, &onoff);
+}
+
+void DecomposeOrderTransform::doTransform(){
+ Vector<Order *> ordervec;
+ Vector<Order *> partialcandidatevec;
+ uint size = order->constraints.getSize();
+ for (uint i = 0; i < size; i++) {
+ BooleanOrder *orderconstraint = order->constraints.get(i);
+ OrderNode *from = graph->getOrderNodeFromOrderGraph(orderconstraint->first);
+ OrderNode *to = graph->getOrderNodeFromOrderGraph(orderconstraint->second);
+ model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
+ if (from->sccNum != to->sccNum) {
+ OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
+ if (edge->polPos) {
+ solver->replaceBooleanWithTrue(orderconstraint);
+ } else if (edge->polNeg) {
+ solver->replaceBooleanWithFalse(orderconstraint);
+ } else {
+ //This case should only be possible if constraint isn't in AST
+ ASSERT(0);
+ }
+ } else {
+ //Build new order and change constraint's order
+ Order *neworder = NULL;
+ if (ordervec.getSize() > from->sccNum)
+ neworder = ordervec.get(from->sccNum);
+ if (neworder == NULL) {
+ MutableSet *set = solver->createMutableSet(order->set->type);
+ neworder = solver->createOrder(order->type, set);
+ ordervec.setExpand(from->sccNum, neworder);
+ if (order->type == PARTIAL)
+ partialcandidatevec.setExpand(from->sccNum, neworder);
+ else
+ partialcandidatevec.setExpand(from->sccNum, NULL);
+ }
+ if (from->status != ADDEDTOSET) {
+ from->status = ADDEDTOSET;
+ ((MutableSet *)neworder->set)->addElementMSet(from->id);
+ }
+ if (to->status != ADDEDTOSET) {
+ to->status = ADDEDTOSET;
+ ((MutableSet *)neworder->set)->addElementMSet(to->id);
+ }
+ if (order->type == PARTIAL) {
+ OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
+ if (edge->polNeg)
+ partialcandidatevec.setExpand(from->sccNum, NULL);
+ }
+ orderconstraint->order = neworder;
+ neworder->addOrderConstraint(orderconstraint);
+ }
+ }
+
+ uint pcvsize = partialcandidatevec.getSize();
+ for (uint i = 0; i < pcvsize; i++) {
+ Order *neworder = partialcandidatevec.get(i);
+ if (neworder != NULL) {
+ neworder->type = TOTAL;
+ model_print("i=%u\t", i);
+ }
+ }
+}
--- /dev/null
+/*
+ * File: ordertransform.h
+ * Author: hamed
+ *
+ * Created on August 28, 2017, 10:35 AM
+ */
+
+#ifndef ORDERTRANSFORM_H
+#define ORDERTRANSFORM_H
+#include "classlist.h"
+#include "transform.h"
+
+
+class DecomposeOrderTransform : public Transform {
+public:
+ DecomposeOrderTransform(CSolver* _solver, Order* order);
+ virtual ~DecomposeOrderTransform();
+ void doTransform();
+ void setOrderGraph(OrderGraph* _graph){
+ graph = _graph;
+ }
+ bool canExecuteTransform();
+private:
+ Order* order;
+ OrderGraph* graph;
+};
+
+#endif /* ORDERTRANSFORM_H */
+
+
#include "integerencoding.h"
-#include "orderelement.h"
+#include "set.h"
#include "order.h"
#include "satencoder.h"
#include "csolver.h"
-#include "predicate.h"
-#include "element.h"
-#include "rewriter.h"
-#include "set.h"
+#include "integerencodingrecord.h"
+
+HashTableOrderIntegerEncoding* IntegerEncodingTransform::orderIntegerEncoding = new HashTableOrderIntegerEncoding();
+
+IntegerEncodingTransform::IntegerEncodingTransform(CSolver* _solver, Order* _order)
+ :Transform(_solver),
+ order(_order)
+
+{
+}
+
+IntegerEncodingTransform::~IntegerEncodingTransform(){
+}
+bool IntegerEncodingTransform::canExecuteTransform(){
+ return canExecutePass(solver, order->type, ORDERINTEGERENCODING, &offon);
+}
-void orderIntegerEncodingSATEncoder(CSolver *solver, BooleanOrder *boolOrder) {
- Order *order = boolOrder->order;
- if (order->elementTable == NULL) {
- order->initializeOrderElementsHashTable();
+void IntegerEncodingTransform::doTransform(){
+ if (!orderIntegerEncoding->contains(order)) {
+ orderIntegerEncoding->put(order, new IntegerEncodingRecord(
+ solver->createRangeSet(order->set->type, 0, (uint64_t) order->set->getSize()-1)));
+ }
+ uint size = order->constraints.getSize();
+ for(uint i=0; i<size; i++){
+ orderIntegerEncodingSATEncoder(order->constraints.get(i));
}
+}
+
+
+void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder) {
+ IntegerEncodingRecord* ierec = orderIntegerEncoding->get(order);
//getting two elements and using LT predicate ...
- ElementSet *elem1 = (ElementSet *)getOrderIntegerElement(solver, order, boolOrder->first);
- ElementSet *elem2 = (ElementSet *)getOrderIntegerElement(solver, order, boolOrder->second);
- Set *sarray[] = {elem1->set, elem2->set};
+ Element *elem1 = ierec->getOrderIntegerElement(solver, boolOrder->first);
+ Element *elem2 = ierec->getOrderIntegerElement(solver, boolOrder->second);
+ Set *sarray[] = {ierec->set, ierec->set};
Predicate *predicate = solver->createPredicateOperator(LT, sarray, 2);
Element *parray[] = {elem1, elem2};
Boolean *boolean = solver->applyPredicate(predicate, parray, 2);
solver->replaceBooleanWithBoolean(boolOrder, boolean);
}
-
-Element *getOrderIntegerElement(CSolver * solver, Order *order, uint64_t item) {
- HashSetOrderElement *eset = order->elementTable;
- OrderElement oelement(item, NULL);
- if ( !eset->contains(&oelement)) {
- Set *set = solver->createRangeSet(order->set->type, 1, (uint64_t) order->set->getSize());
- Element *elem = solver->getElementVar(set);
- eset->add(new OrderElement(item, elem));
- return elem;
- } else
- return eset->get(&oelement)->elem;
-}
-
-/*
- * To change this license header, choose License Headers in Project Properties.
- * To change this template file, choose Tools | Templates
- * and open the template in the editor.
- */
-
-/*
+/*
* File: integerencoding.h
* Author: hamed
*
- * Created on August 24, 2017, 5:31 PM
+ * Created on August 27, 2017, 4:36 PM
*/
#ifndef INTEGERENCODING_H
#define INTEGERENCODING_H
#include "classlist.h"
-#include "structs.h"
+#include "transform.h"
+#include "order.h"
+
+class IntegerEncodingTransform : public Transform{
+public:
+ IntegerEncodingTransform(CSolver* solver, Order* order);
+ void orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder);
+ 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;
+};
-Element *getOrderIntegerElement(CSolver *solver, Order *order, uint64_t item);
-void orderIntegerEncodingSATEncoder(CSolver *solver, BooleanOrder *boolOrder);
-#endif/* INTEGERENCODING_H */
+#endif /* INTEGERENCODING_H */
--- /dev/null
+/*
+ * File: integerencodingrecord.cpp
+ * Author: hamed
+ *
+ * Created on August 26, 2017, 6:19 PM
+ */
+
+#include "integerencodingrecord.h"
+#include "csolver.h"
+#include "orderelement.h"
+
+IntegerEncodingRecord::IntegerEncodingRecord(Set* _set):
+ set(_set)
+{
+ elementTable = new HashSetOrderElement();
+}
+
+IntegerEncodingRecord::~IntegerEncodingRecord(){
+ if (elementTable != NULL) {
+ delete elementTable;
+ }
+}
+
+Element * IntegerEncodingRecord::getOrderIntegerElement(CSolver *This, uint64_t item) {
+ OrderElement oelement(item, NULL);
+ if ( !elementTable->contains(&oelement)) {
+ Element *elem = This->getElementVar(set);
+ elementTable->add(new OrderElement(item, elem));
+ return elem;
+ } else
+ return elementTable->get(&oelement)->elem;
+}
+
--- /dev/null
+/*
+ * File: integerencodingrecord.h
+ * Author: hamed
+ *
+ * Created on August 26, 2017, 6:19 PM
+ */
+
+#ifndef INTEGERENCODINGRECORD_H
+#define INTEGERENCODINGRECORD_H
+#include "classlist.h"
+#include "structs.h"
+#include "mymemory.h"
+
+class IntegerEncodingRecord {
+public:
+ Set* set;
+ IntegerEncodingRecord(Set* set);
+ ~IntegerEncodingRecord();
+ Element* getOrderIntegerElement(CSolver *This, uint64_t item);
+ MEMALLOC;
+
+private:
+ HashSetOrderElement *elementTable;
+};
+
+#endif /* INTEGERENCODINGRECORD_H */
+
+++ /dev/null
-#include "orderdecompose.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 "integerencoding.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);
- bool doDecompose = GETVARTUNABLE(This->getTuner(), order->type, DECOMPOSEORDER, &onoff);
- if (!doDecompose)
- 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);
- decomposeOrder(This, order, graph);
- delete graph;
-
- /*
- OrderIntegerEncodingSATEncoder wants a private field that it really shoukldn't need...
-
- bool doIntegerEncoding = GETVARTUNABLE(This->getTuner(), order->order.type, ORDERINTEGERENCODING, &offon );
- if(!doIntegerEncoding)
- continue;
- uint size = order->constraints.getSize();
- for(uint i=0; i<size; i++){
- orderIntegerEncodingSATEncoder(This->satEncoder, order->constraints.get(i));
- }*/
-
- }
-}
-
-void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
- Vector<Order *> ordervec;
- Vector<Order *> partialcandidatevec;
- uint size = order->constraints.getSize();
- for (uint i = 0; i < size; i++) {
- BooleanOrder *orderconstraint = order->constraints.get(i);
- OrderNode *from = graph->getOrderNodeFromOrderGraph(orderconstraint->first);
- OrderNode *to = graph->getOrderNodeFromOrderGraph(orderconstraint->second);
- if (from->sccNum != to->sccNum) {
- OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
- if (edge->polPos) {
- This->replaceBooleanWithTrue(orderconstraint);
- } else if (edge->polNeg) {
- This->replaceBooleanWithFalse(orderconstraint);
- } else {
- //This case should only be possible if constraint isn't in AST
- ASSERT(0);
- }
- } else {
- //Build new order and change constraint's order
- Order *neworder = NULL;
- if (ordervec.getSize() > from->sccNum)
- neworder = ordervec.get(from->sccNum);
- if (neworder == NULL) {
- MutableSet *set = This->createMutableSet(order->set->type);
- neworder = This->createOrder(order->type, set);
- ordervec.setExpand(from->sccNum, neworder);
- if (order->type == PARTIAL)
- partialcandidatevec.setExpand(from->sccNum, neworder);
- else
- partialcandidatevec.setExpand(from->sccNum, NULL);
- }
- if (from->status != ADDEDTOSET) {
- from->status = ADDEDTOSET;
- ((MutableSet *)neworder->set)->addElementMSet(from->id);
- }
- if (to->status != ADDEDTOSET) {
- to->status = ADDEDTOSET;
- ((MutableSet *)neworder->set)->addElementMSet(to->id);
- }
- if (order->type == PARTIAL) {
- OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
- if (edge->polNeg)
- partialcandidatevec.setExpand(from->sccNum, NULL);
- }
- orderconstraint->order = neworder;
- neworder->addOrderConstraint(orderconstraint);
- }
- }
-
- uint pcvsize = partialcandidatevec.getSize();
- for (uint i = 0; i < pcvsize; i++) {
- Order *neworder = partialcandidatevec.get(i);
- if (neworder != NULL) {
- neworder->type = TOTAL;
- model_print("i=%u\t", i);
- }
- }
-}
-
+++ /dev/null
-/*
- * To change this license header, choose License Headers in Project Properties.
- * To change this template file, choose Tools | Templates
- * and open the template in the editor.
- */
-
-/*
- * File: orderdecompose.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);
-void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph);
-
-#endif/* ORDERDECOMPOSE_H */
-
--- /dev/null
+/*
+ * File: pass.h
+ * Author: hamed
+ *
+ * Created on August 28, 2017, 6:23 PM
+ */
+
+#ifndef PASS_H
+#define PASS_H
+#include "classlist.h"
+#include "mymemory.h"
+#include "structs.h"
+#include "tunable.h"
+#include "csolver.h"
+
+class Pass{
+public:
+ Pass(){};
+ virtual ~Pass(){};
+ virtual inline bool canExecutePass(CSolver* This, uint type, Tunables tunable, TunableDesc* desc){
+ return GETVARTUNABLE(This->getTuner(), type, tunable, desc);
+ }
+ MEMALLOC;
+
+};
+
+
+#endif /* PASS_H */
+
--- /dev/null
+/*
+ * File: transform.cc
+ * Author: hamed
+ *
+ * Created on August 26, 2017, 5:14 PM
+ */
+
+#include "transform.h"
+
+Transform::Transform(CSolver* _solver)
+{
+ solver = _solver;
+}
+
+Transform::~Transform(){
+}
--- /dev/null
+/*
+ * File: transform.h
+ * Author: hamed
+ *
+ * Created on August 26, 2017, 5:13 PM
+ */
+
+#ifndef TRANSFORM_H
+#define TRANSFORM_H
+
+#include "classlist.h"
+#include "mymemory.h"
+#include "structs.h"
+#include "pass.h"
+
+class Transform : public Pass{
+public:
+ Transform(CSolver* _solver);
+ virtual ~Transform();
+ virtual bool canExecuteTransform() = 0;
+ virtual void doTransform() = 0;
+protected:
+ // Need solver for translating back the result ...
+ CSolver* solver;
+};
+
+#endif /* TRANSFORM_H */
+
return key1->first == key2->first && key1->second == key2->second;
}
+unsigned int order_hash_function(Order *This) {
+ return (uint) This;
+}
+
+bool order_pair_equals(Order *key1, Order *key2) {
+ return key1==key2;
+}
+
bool order_element_equals(OrderElement *key1, OrderElement *key2);
unsigned int order_pair_hash_function(OrderPair *This);
bool order_pair_equals(OrderPair *key1, OrderPair *key2);
+unsigned int order_hash_function(Order *This);
+bool order_pair_equals(Order *key1, Order *key2);
+
typedef HashSet<Boolean *, uintptr_t, 4> HashSetBoolean;
typedef HashSet<TableEntry *, uintptr_t, 4, table_entry_hash_function, table_entry_equals> HashSetTableEntry;
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 HSIterator<TableEntry *, uintptr_t, 4, table_entry_hash_function, table_entry_equals> HSIteratorTableEntry;
typedef HSIterator<Boolean *, uintptr_t, 4> HSIteratorBoolean;
class OrderPair;
class OrderElement;
+class IntegerEncodingRecord;
+class Transform;
+class Pass;
class ElementEncoding;
class FunctionEncoding;
#include "sattranslator.h"
#include "tunable.h"
#include "polarityassignment.h"
-#include "orderdecompose.h"
+#include "analyzer.h"
#include "autotuner.h"
CSolver::CSolver() :
projects / satune.git / commitdiff