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 HappenedBefore 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->getOrderNodeFromOrderGraph(first, false /*Don't create new node if doesn't exist*/);
  31                 if (from == NULL) {
  32                         return SATC_UNORDERED;
  33                 }
  34                 OrderNode *to = graph->getOrderNodeFromOrderGraph(second, false);
  35                 if (from == NULL) {
  36                         return SATC_UNORDERED;
  37                 }
  38
  39                 OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to, false     /* Don't create a new edge*/);
  40                 if (edge != NULL && edge->mustPos) {
  41                         return SATC_FIRST;
  42                 } else if ( edge != NULL && edge->mustNeg) {
  43                         return SATC_SECOND;
  44                 }
  45         }
  46
  47         //Couldn't infer from graph. Should call the SAT Solver ...
  48         switch ( order->type) {
  49         case SATC_TOTAL:
  50                 resolveTotalOrder(first, second);
  51         case SATC_PARTIAL:
  52         //TODO: Support for partial order ...
  53         default:
  54                 ASSERT(0);
  55         }
  56
  57
  58 }
  59
  60
  61 HappenedBefore OrderPairResolver::resolveTotalOrder(uint64_t first, uint64_t second) {
  62         ASSERT(order->orderPairTable != NULL);
  63         OrderPair pair(first, second, E_NULL);
  64         Edge var = getOrderConstraint(order->orderPairTable, &pair);
  65         if (edgeIsNull(var))
  66                 return SATC_UNORDERED;
  67         return getValueCNF(solver->getSATEncoder()->getCNF(), var) ? SATC_FIRST : SATC_SECOND;
  68 }