Interface should be bool, not happenedbefore

diff --git a/src/AST/ops.h b/src/AST/ops.h
index a26d1cd5068d6149625fe158eef79e57f3f3d146..8b082025348ffaeab34916512eb55368068473d9 100644 (file)
--- 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 f797f5e28a3ef511e517db54a90115ff23101e6a..fcc9eda132f0b3b1e0c56e5e8e409968a243f9e2 100644 (file)
--- 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 d508d0334759eb74b85c40e3bf01ab7899386f82..5f10c1fba5430fd4736ffe0a45cc9841abf070fd 100644 (file)
--- 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 798bb3085a458a90f4f150f1cba656ee327b95b2..f226fdaee8100dd7915b101d329f57914fb4f7e4 100644 (file)
--- a/src/Translator/decomposeorderresolver.cc
+++ b/src/Translator/decomposeorderresolver.cc
@@ -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:

diff --git a/src/Translator/decomposeorderresolver.h b/src/Translator/decomposeorderresolver.h
index 0ca8264bd91785c3442f73eef60671a71aa2fdaa..be25a7d76dd379f453af4030ac1691401a0e4040 100644 (file)
--- a/src/Translator/decomposeorderresolver.h
+++ b/src/Translator/decomposeorderresolver.h
@@ -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;

diff --git a/src/Translator/integerencorderresolver.cc b/src/Translator/integerencorderresolver.cc
index 4f6701879e6b8a9cc737967bbadc1c1113073dfd..a9fb25c3b365117fd0ab4a4206aa67dbc9a18532 100644 (file)
--- 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 56941e9b9441a3107d924a2e9588bb926fd32c97..e6f050813d0f86a5348ad2b51a33ec844305b2e8 100644 (file)
--- 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 3f500776094324cd49c3cb0f7750ceaf7d39942d..f0cb98d5e10c13c902c05807564a787bf3c9c78a 100644 (file)
--- 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 80ef7e491ae0f07d17b5c339d3e2caae78ea5305..bf7210cf7a3f74eb334481680e0c2809bafb5a58 100644 (file)
--- 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 7e5ea618262f4bb8d1eeace6256244bf77601a45..ac82cc3e37996d32dd0ec4eff893819b5c87ccd3 100644 (file)
--- 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 b351914cd2b0fbe81faa68149bd993a6056e6833..22b0661cb9228b765f7f7f4111ebecd8dd9bb6a7 100644 (file)
--- 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 7e8bbad871019bcc59f06d5e170de317fc2cae02..8f5d6975b5062bbc5245cf0186d1b1bc955937f5 100644 (file)
--- 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 8ad874b2c9e77d802114de59bd0b6716f1a54dd5..7c63aa11c10edb99f259ab9a11fffcae8df89794 100644 (file)
--- 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) {       \