Interface should be bool, not happenedbefore
authorbdemsky <bdemsky@uci.edu>
Sat, 2 Sep 2017 07:28:06 +0000 (00:28 -0700)
committerbdemsky <bdemsky@uci.edu>
Sat, 2 Sep 2017 07:28:06 +0000 (00:28 -0700)
13 files changed:
src/AST/ops.h
src/ASTAnalyses/ordergraph.cc
src/ASTAnalyses/ordergraph.h
src/Translator/decomposeorderresolver.cc
src/Translator/decomposeorderresolver.h
src/Translator/integerencorderresolver.cc
src/Translator/integerencorderresolver.h
src/Translator/orderpairresolver.cc
src/Translator/orderpairresolver.h
src/Translator/orderresolver.h
src/csolver.cc
src/csolver.h
src/mymemory.h

index a26d1cd..8b08202 100644 (file)
@@ -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
index f797f5e..fcc9eda 100644 (file)
@@ -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;
 }
index d508d03..5f10c1f 100644 (file)
@@ -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);
index 798bb30..f226fda 100644 (file)
@@ -20,25 +20,22 @@ DecomposeOrderResolver::DecomposeOrderResolver(OrderGraph *_graph, Vector<Order
 DecomposeOrderResolver::~DecomposeOrderResolver() {
 }
 
-HappenedBefore DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t second) {
-       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;
-       }
+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:
index 0ca8264..be25a7d 100644 (file)
@@ -16,7 +16,7 @@
 class DecomposeOrderResolver : public OrderResolver {
 public:
        DecomposeOrderResolver(OrderGraph *graph, Vector<Order *> &orders);
-       HappenedBefore resolveOrder(uint64_t first, uint64_t second);
+       bool resolveOrder(uint64_t first, uint64_t second);
        virtual ~DecomposeOrderResolver();
 private:
        OrderGraph *graph;
index 4f67018..a9fb25c 100644 (file)
@@ -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;
 }
index 56941e9..e6f0508 100644 (file)
@@ -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;
index 3f50077..f0cb98d 100644 (file)
@@ -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);
 }
index 80ef7e4..bf7210c 100644 (file)
 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 */
index 7e5ea61..ac82cc3 100644 (file)
@@ -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;
 };
index b351914..22b0661 100644 (file)
@@ -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);
 }
 
index 7e8bbad..8f5d697 100644 (file)
@@ -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);
index 8ad874b..7c63aa1 100644 (file)
@@ -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) {       \