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) :
20 orderPairTable(new HashtableOrderPair())
24 OrderPairResolver::~OrderPairResolver() {
25 if (orderPairTable != NULL) {
26 orderPairTable->resetanddelete();
27 delete orderPairTable;
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);
37 OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
40 OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
42 if (edge != NULL && edge->mustPos) {
44 } else if ( edge != NULL && edge->mustNeg) {
49 //Couldn't infer from graph. Should call the SAT Solver ...
50 return getOrderConstraintValue(first, second);
53 bool OrderPairResolver::getOrderConstraintValue(uint64_t first, uint64_t second) {
54 ASSERT(first != second);
56 OrderPair tmp(first, second);
62 if (!orderPairTable->contains(&tmp)) {
65 OrderPair *pair = orderPairTable->get(&tmp);
66 return negate ? pair->getNegatedConstraintValue(solver) : pair->getConstraintValue(solver);