Fix some memory leaks
[satune.git] / src / Translator / orderpairresolver.cc
1
2 /*
3  * File:   orderpairresolver.cc
4  * Author: hamed
5  *
6  * Created on September 1, 2017, 3:36 PM
7  */
8
9 #include "orderpairresolver.h"
10 #include "ordergraph.h"
11 #include "order.h"
12 #include "orderedge.h"
13 #include "ordernode.h"
14 #include "satencoder.h"
15 #include "csolver.h"
16
17 OrderPairResolver::OrderPairResolver(CSolver *_solver, Order *_order) :
18         solver(_solver),
19         order(_order),
20         orderPairTable(new HashtableOrderPair())
21 {
22 }
23
24 OrderPairResolver::~OrderPairResolver() {
25         if (orderPairTable != NULL) {
26                 orderPairTable->resetAndDeleteVals();
27                 delete orderPairTable;
28         }
29 }
30
31 bool OrderPairResolver::resolveOrder(uint64_t first, uint64_t second) {
32         if (order->graph != NULL) {
33                 // For the cases that tuning framework decides no to build a graph for order ...
34                 OrderGraph *graph = order->graph;
35                 OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
36                 ASSERT(from != NULL);
37                 OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
38                 ASSERT(to != NULL);
39
40                 OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
41
42                 if (edge != NULL && edge->mustPos) {
43                         return true;
44                 } else if ( edge != NULL && edge->mustNeg) {
45                         return false;
46                 }
47         }
48
49         //Couldn't infer from graph. Should call the SAT Solver ...
50         return getOrderConstraintValue(first, second);
51 }
52
53 bool OrderPairResolver::getOrderConstraintValue(uint64_t first, uint64_t second) {
54         ASSERT(first != second);
55         bool negate = false;
56         OrderPair tmp(first, second);
57         if (first < second) {
58                 negate = true;
59                 tmp.first = second;
60                 tmp.second = first;
61         }
62         if (!orderPairTable->contains(&tmp)) {
63                 return false;
64         }
65         OrderPair *pair = orderPairTable->get(&tmp);
66         return negate ? pair->getNegatedConstraintValue(solver) : pair->getConstraintValue(solver);
67 }