3 * File: orderpairresolver.cc
6 * Created on September 1, 2017, 3:36 PM
9 #include "orderpairresolver.h"
10 #include "ordergraph.h"
12 #include "orderedge.h"
13 #include "ordernode.h"
14 #include "satencoder.h"
17 OrderPairResolver::OrderPairResolver(CSolver* _solver, Order* _order) :
23 OrderPairResolver::~OrderPairResolver() {
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*/);
32 return SATC_UNORDERED;
34 OrderNode *to = graph->getOrderNodeFromOrderGraph(second, false);
36 return SATC_UNORDERED;
39 OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to, false /* Don't create a new edge*/);
40 if (edge != NULL && edge->mustPos){
42 } else if( edge != NULL && edge->mustNeg){
47 //Couldn't infer from graph. Should call the SAT Solver ...
50 resolveTotalOrder(first, second);
52 //TODO: Support for partial order ...
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);
66 return SATC_UNORDERED;
67 return getValueCNF(solver->getSATEncoder()->getCNF(), var) ? SATC_FIRST : SATC_SECOND;