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->resetanddelete();
  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 }