Fix some memory leaks

[satune.git] / src / Translator / orderpairresolver.cc

diff --git a/src/Translator/orderpairresolver.cc b/src/Translator/orderpairresolver.cc
index fa147d0ec4cba71f6b1df6b4c54f8a6eae24cc54..38c8a761824b0139fc0d3bcdda376486bc2f47a9 100644 (file)
--- a/src/Translator/orderpairresolver.cc
+++ b/src/Translator/orderpairresolver.cc
@@ -1,8 +1,8 @@
 
-/* 
+/*
  * File:   orderpairresolver.cc
  * Author: hamed
- * 
+ *
  * Created on September 1, 2017, 3:36 PM
  */
 
@@ -14,55 +14,54 @@
 #include "satencoder.h"
 #include "csolver.h"
 
-OrderPairResolver::OrderPairResolver(CSolver* _solver, Order* _order) :
+OrderPairResolver::OrderPairResolver(CSolver *_solver, Order *_order) :
        solver(_solver),
-       order(_order)
+       order(_order),
+       orderPairTable(new HashtableOrderPair())
 {
 }
 
 OrderPairResolver::~OrderPairResolver() {
+       if (orderPairTable != NULL) {
+               orderPairTable->resetAndDeleteVals();
+               delete orderPairTable;
+       }
 }
 
-HappenedBefore OrderPairResolver::resolveOrder(uint64_t first, uint64_t second){
-       if(order->graph != NULL){
+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;
-               }
+               OrderGraph *graph = order->graph;
+               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*/);
-               if (edge != NULL && edge->mustPos){
-                       return SATC_FIRST;
-               } else if( edge != NULL && edge->mustNeg){
-                       return SATC_SECOND;
+               OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
+
+               if (edge != NULL && edge->mustPos) {
+                       return true;
+               } else if ( edge != NULL && edge->mustNeg) {
+                       return false;
                }
        }
 
        //Couldn't infer from graph. Should call the SAT Solver ...
-       switch( order->type){
-               case SATC_TOTAL:
-                       resolveTotalOrder(first, second);
-               case SATC_PARTIAL:
-                       //TODO: Support for partial order ...
-               default:
-                       ASSERT(0);
-       }
-       
-
+       return getOrderConstraintValue(first, second);
 }
 
-
-HappenedBefore 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;
+bool OrderPairResolver::getOrderConstraintValue(uint64_t first, uint64_t second) {
+       ASSERT(first != second);
+       bool negate = false;
+       OrderPair tmp(first, second);
+       if (first < second) {
+               negate = true;
+               tmp.first = second;
+               tmp.second = first;
+       }
+       if (!orderPairTable->contains(&tmp)) {
+               return false;
+       }
+       OrderPair *pair = orderPairTable->get(&tmp);
+       return negate ? pair->getNegatedConstraintValue(solver) : pair->getConstraintValue(solver);
 }