+++ /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 */
-
#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);
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;
};
#include "orderelement.h"
IntegerEncodingRecord::IntegerEncodingRecord(Set* _set):
- set(_set)
+ secondarySet(_set)
{
elementTable = new HashSetOrderElement();
}
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();
}
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;
};
--- /dev/null
+#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();
+ }
+}
+
+
--- /dev/null
+/*
+ * 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 */
+
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;
};
}
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) {
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
class IntegerEncodingRecord;
class Transform;
class Pass;
+class Transformer;
+class AnalysisData;
class ElementEncoding;
class FunctionEncoding;
#include "sattranslator.h"
#include "tunable.h"
#include "polarityassignment.h"
-#include "analyzer.h"
+#include "transformer.h"
#include "autotuner.h"
CSolver::CSolver() :
elapsedTime(0)
{
satEncoder = new SATEncoder(this);
+ transformer = new Transformer(this);
}
/** This function tears down the solver and the entire AST */
}
delete satEncoder;
+ delete transformer;
}
CSolver *CSolver::clone() {
long long startTime = getTimeNano();
computePolarities(this);
- orderAnalysis(this);
+ transformer->orderAnalysis();
naiveEncodingDecision(this);
satEncoder->encodeAllSATEncoder(this);
int result = unsat ? IS_UNSAT : satEncoder->solve();
Vector<Order *> *getOrders() { return &allOrders;}
Tuner *getTuner() { return tuner; }
+ Transformer* getTransformer() {return transformer;}
HSIteratorBoolean *getConstraints() { return constraints.iterator(); }
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();
SATEncoder *satEncoder;
bool unsat;
Tuner *tuner;
-
+ Transformer* transformer;
long long elapsedTime;
};
#endif