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 {
  21 }
  22
  23 OrderPairResolver::~OrderPairResolver() {
  24 }
  25
  26 bool OrderPairResolver::resolveOrder(uint64_t first, uint64_t second) {
  27         if (order->graph != NULL) {
  28                 // For the cases that tuning framework decides no to build a graph for order ...
  29                 OrderGraph *graph = order->graph;
  30                 OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
  31                 ASSERT(from != NULL);
  32                 OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
  33                 ASSERT(to != NULL);
  34
  35                 OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
  36
  37                 if (edge != NULL && edge->mustPos) {
  38                         return true;
  39                 } else if ( edge != NULL && edge->mustNeg) {
  40                         return false;
  41                 }
  42         }
  43
  44         //Couldn't infer from graph. Should call the SAT Solver ...
  45         switch ( order->type) {
  46         case SATC_TOTAL:
  47                 resolveTotalOrder(first, second);
  48         case SATC_PARTIAL:
  49         //TODO: Support for partial order ...
  50         default:
  51                 ASSERT(0);
  52         }
  53
  54
  55 }
  56
  57
  58 bool OrderPairResolver::resolveTotalOrder(uint64_t first, uint64_t second) {
  59         ASSERT(order->orderPairTable != NULL);
  60         OrderPair pair(first, second, E_NULL);
  61         Edge var = getOrderConstraint(order->orderPairTable, &pair);
  62         if (edgeIsNull(var))
  63                 return false;
  64         return getValueCNF(solver->getSATEncoder()->getCNF(), var);
  65 }