From 13a2b4ac7c072f1896f23b30d23233eb67c05061 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Sat, 2 Sep 2017 00:28:06 -0700 Subject: [PATCH] Interface should be bool, not happenedbefore --- src/AST/ops.h | 3 --- src/ASTAnalyses/ordergraph.cc | 14 ++++-------- src/ASTAnalyses/ordergraph.h | 4 ++-- src/Translator/decomposeorderresolver.cc | 23 +++++++++---------- src/Translator/decomposeorderresolver.h | 2 +- src/Translator/integerencorderresolver.cc | 10 ++++----- src/Translator/integerencorderresolver.h | 2 +- src/Translator/orderpairresolver.cc | 27 ++++++++++------------- src/Translator/orderpairresolver.h | 4 ++-- src/Translator/orderresolver.h | 2 +- src/csolver.cc | 7 +++--- src/csolver.h | 2 +- src/mymemory.h | 6 +++-- 13 files changed, 46 insertions(+), 60 deletions(-) diff --git a/src/AST/ops.h b/src/AST/ops.h index a26d1cd..8b08202 100644 --- a/src/AST/ops.h +++ b/src/AST/ops.h @@ -12,9 +12,6 @@ typedef enum CompOp CompOp; enum OrderType {SATC_PARTIAL, SATC_TOTAL}; typedef enum OrderType OrderType; -enum HappenedBefore {SATC_FIRST, SATC_SECOND, SATC_UNORDERED}; -typedef enum HappenedBefore HappenedBefore; - /** * SATC_FLAGFORCESOVERFLOW forces the operation to overflow if the boolean flag is true * SATC_OVERFLOWSETSFLAG -- sets the flag if the operation overflows diff --git a/src/ASTAnalyses/ordergraph.cc b/src/ASTAnalyses/ordergraph.cc index f797f5e..fcc9eda 100644 --- a/src/ASTAnalyses/ordergraph.cc +++ b/src/ASTAnalyses/ordergraph.cc @@ -105,17 +105,14 @@ void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrd } } -OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id, bool create) { +OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) { OrderNode *node = new OrderNode(id); OrderNode *tmp = nodes->get(node); if ( tmp != NULL) { delete node; node = tmp; - } else if (create) { - nodes->add(node); } else { - delete node; - return NULL; + nodes->add(node); } return node; } @@ -126,17 +123,14 @@ OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) { return tmp; } -OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end, bool create) { +OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) { OrderEdge *edge = new OrderEdge(begin, end); OrderEdge *tmp = edges->get(edge); if ( tmp != NULL ) { delete edge; edge = tmp; - } else if (create) { - edges->add(edge); } else { - delete edge; - return NULL; + edges->add(edge); } return edge; } diff --git a/src/ASTAnalyses/ordergraph.h b/src/ASTAnalyses/ordergraph.h index d508d03..5f10c1f 100644 --- a/src/ASTAnalyses/ordergraph.h +++ b/src/ASTAnalyses/ordergraph.h @@ -17,8 +17,8 @@ public: ~OrderGraph(); void addOrderConstraintToOrderGraph(BooleanOrder *bOrder); void addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder); - OrderNode *getOrderNodeFromOrderGraph(uint64_t id, bool create = true); - OrderEdge *getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end, bool create = true); + OrderNode *getOrderNodeFromOrderGraph(uint64_t id); + OrderEdge *getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end); OrderNode *lookupOrderNodeFromOrderGraph(uint64_t id); OrderEdge *lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end); void addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr); diff --git a/src/Translator/decomposeorderresolver.cc b/src/Translator/decomposeorderresolver.cc index 798bb30..f226fda 100644 --- a/src/Translator/decomposeorderresolver.cc +++ b/src/Translator/decomposeorderresolver.cc @@ -20,25 +20,22 @@ DecomposeOrderResolver::DecomposeOrderResolver(OrderGraph *_graph, VectorgetOrderNodeFromOrderGraph(first, false /*Don't create new node if doesn't exist*/); - if (from == NULL) { - return SATC_UNORDERED; - } - OrderNode *to = graph->getOrderNodeFromOrderGraph(second, false); - if (from == NULL) { - return SATC_UNORDERED; - } +bool DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t second) { + OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first); + ASSERT(from != NULL); + OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second); + ASSERT(to != NULL); + if (from->sccNum != to->sccNum) { - OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to, false /* Don't create a new edge*/); + OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to); if (edge != NULL && edge->mustPos) { - return SATC_FIRST; + return true; } else if ( edge != NULL && edge->mustNeg) { - return SATC_SECOND; + return false; } else { switch (graph->getOrder()->type) { case SATC_TOTAL: - return from->sccNum < to->sccNum ? SATC_FIRST : SATC_SECOND; + return from->sccNum < to->sccNum; case SATC_PARTIAL: //Adding support for partial order ... default: diff --git a/src/Translator/decomposeorderresolver.h b/src/Translator/decomposeorderresolver.h index 0ca8264..be25a7d 100644 --- a/src/Translator/decomposeorderresolver.h +++ b/src/Translator/decomposeorderresolver.h @@ -16,7 +16,7 @@ class DecomposeOrderResolver : public OrderResolver { public: DecomposeOrderResolver(OrderGraph *graph, Vector &orders); - HappenedBefore resolveOrder(uint64_t first, uint64_t second); + bool resolveOrder(uint64_t first, uint64_t second); virtual ~DecomposeOrderResolver(); private: OrderGraph *graph; diff --git a/src/Translator/integerencorderresolver.cc b/src/Translator/integerencorderresolver.cc index 4f67018..a9fb25c 100644 --- a/src/Translator/integerencorderresolver.cc +++ b/src/Translator/integerencorderresolver.cc @@ -20,15 +20,13 @@ IntegerEncOrderResolver::~IntegerEncOrderResolver() { } -HappenedBefore IntegerEncOrderResolver::resolveOrder(uint64_t first, uint64_t second) { +bool IntegerEncOrderResolver::resolveOrder(uint64_t first, uint64_t second) { Element *elem1 = ierecord->getOrderIntegerElement(solver, first, false); - if (elem1 == NULL) - return SATC_UNORDERED; + ASSERT (elem1 != NULL); Element *elem2 = ierecord->getOrderIntegerElement(solver, second, false); - if (elem2 == NULL) - return SATC_UNORDERED; + ASSERT (elem2 != NULL); uint64_t val1 = getElementValueSATTranslator(solver, elem1); uint64_t val2 = getElementValueSATTranslator(solver, elem2); - return val1 < val2 ? SATC_FIRST : val1> val2 ? SATC_SECOND : SATC_UNORDERED; + return val1 < val2; } diff --git a/src/Translator/integerencorderresolver.h b/src/Translator/integerencorderresolver.h index 56941e9..e6f0508 100644 --- a/src/Translator/integerencorderresolver.h +++ b/src/Translator/integerencorderresolver.h @@ -13,7 +13,7 @@ class IntegerEncOrderResolver : public OrderResolver { public: IntegerEncOrderResolver(CSolver *_solver, IntegerEncodingRecord *_ierecord); - HappenedBefore resolveOrder(uint64_t first, uint64_t second); + bool resolveOrder(uint64_t first, uint64_t second); virtual ~IntegerEncOrderResolver(); private: CSolver *solver; diff --git a/src/Translator/orderpairresolver.cc b/src/Translator/orderpairresolver.cc index 3f50077..f0cb98d 100644 --- a/src/Translator/orderpairresolver.cc +++ b/src/Translator/orderpairresolver.cc @@ -23,24 +23,21 @@ OrderPairResolver::OrderPairResolver(CSolver *_solver, Order *_order) : OrderPairResolver::~OrderPairResolver() { } -HappenedBefore OrderPairResolver::resolveOrder(uint64_t first, uint64_t second) { +bool OrderPairResolver::resolveOrder(uint64_t first, uint64_t second) { if (order->graph != NULL) { // For the cases that tuning framework decides no to build a graph for order ... OrderGraph *graph = order->graph; - OrderNode *from = graph->getOrderNodeFromOrderGraph(first, false /*Don't create new node if doesn't exist*/); - if (from == NULL) { - return SATC_UNORDERED; - } - OrderNode *to = graph->getOrderNodeFromOrderGraph(second, false); - if (from == NULL) { - return SATC_UNORDERED; - } + OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first); + ASSERT(from != NULL); + OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second); + ASSERT(to != NULL); - OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to, false /* Don't create a new edge*/); + OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to); + if (edge != NULL && edge->mustPos) { - return SATC_FIRST; + return true; } else if ( edge != NULL && edge->mustNeg) { - return SATC_SECOND; + return false; } } @@ -58,11 +55,11 @@ HappenedBefore OrderPairResolver::resolveOrder(uint64_t first, uint64_t second) } -HappenedBefore OrderPairResolver::resolveTotalOrder(uint64_t first, uint64_t second) { +bool OrderPairResolver::resolveTotalOrder(uint64_t first, uint64_t second) { ASSERT(order->orderPairTable != NULL); OrderPair pair(first, second, E_NULL); Edge var = getOrderConstraint(order->orderPairTable, &pair); if (edgeIsNull(var)) - return SATC_UNORDERED; - return getValueCNF(solver->getSATEncoder()->getCNF(), var) ? SATC_FIRST : SATC_SECOND; + return false; + return getValueCNF(solver->getSATEncoder()->getCNF(), var); } diff --git a/src/Translator/orderpairresolver.h b/src/Translator/orderpairresolver.h index 80ef7e4..bf7210c 100644 --- a/src/Translator/orderpairresolver.h +++ b/src/Translator/orderpairresolver.h @@ -14,12 +14,12 @@ class OrderPairResolver : public OrderResolver { public: OrderPairResolver(CSolver *_solver, Order *_order); - HappenedBefore resolveOrder(uint64_t first, uint64_t second); + bool resolveOrder(uint64_t first, uint64_t second); virtual ~OrderPairResolver(); private: CSolver *solver; Order *order; - HappenedBefore resolveTotalOrder(uint64_t first, uint64_t second); + bool resolveTotalOrder(uint64_t first, uint64_t second); }; #endif/* ORDERPAIRRESOLVER_H */ diff --git a/src/Translator/orderresolver.h b/src/Translator/orderresolver.h index 7e5ea61..ac82cc3 100644 --- a/src/Translator/orderresolver.h +++ b/src/Translator/orderresolver.h @@ -15,7 +15,7 @@ class OrderResolver { public: OrderResolver() {}; - virtual HappenedBefore resolveOrder(uint64_t first, uint64_t second) = 0; + virtual bool resolveOrder(uint64_t first, uint64_t second) = 0; virtual ~OrderResolver() {}; CMEMALLOC; }; diff --git a/src/csolver.cc b/src/csolver.cc index b351914..22b0661 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -400,8 +400,9 @@ int CSolver::solve() { DecomposeOrderTransform dot(this); dot.doTransform(); - IntegerEncodingTransform iet(this); - iet.doTransform(); + //This leaks like crazy + // IntegerEncodingTransform iet(this); + //iet.doTransform(); naiveEncodingDecision(this); satEncoder->encodeAllSATEncoder(this); @@ -437,7 +438,7 @@ bool CSolver::getBooleanValue(Boolean *boolean) { exit(-1); } -HappenedBefore CSolver::getOrderConstraintValue(Order *order, uint64_t first, uint64_t second) { +bool CSolver::getOrderConstraintValue(Order *order, uint64_t first, uint64_t second) { return order->encoding.resolver->resolveOrder(first, second); } diff --git a/src/csolver.h b/src/csolver.h index 7e8bbad..8f5d697 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -115,7 +115,7 @@ public: /** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/ bool getBooleanValue(Boolean *boolean); - HappenedBefore getOrderConstraintValue(Order *order, uint64_t first, uint64_t second); + bool getOrderConstraintValue(Order *order, uint64_t first, uint64_t second); bool isTrue(Boolean *b); bool isFalse(Boolean *b); diff --git a/src/mymemory.h b/src/mymemory.h index 8ad874b..7c63aa1 100644 --- a/src/mymemory.h +++ b/src/mymemory.h @@ -25,7 +25,8 @@ void * ourcalloc(size_t count, size_t size); void * ourrealloc(void *ptr, size_t size); */ - /* + +#if 0 void * model_malloc(size_t size); void model_free(void *ptr); void * model_calloc(size_t count, size_t size); @@ -36,12 +37,13 @@ void * model_realloc(void *ptr, size_t size); #define ourfree model_free #define ourrealloc model_realloc #define ourcalloc model_calloc -*/ +#else static inline void *ourmalloc(size_t size) { return malloc(size); } static inline void ourfree(void *ptr) { free(ptr); } static inline void *ourcalloc(size_t count, size_t size) { return calloc(count, size); } static inline void *ourrealloc(void *ptr, size_t size) { return realloc(ptr, size); } +#endif #define CMEMALLOC \ void *operator new(size_t size) { \ -- 2.34.1