OrderPairResolver::OrderPairResolver(CSolver *_solver, Order *_order) :
solver(_solver),
- order(_order)
+ order(_order),
+ orderPairTable(new HashtableOrderPair())
{
}
OrderPairResolver::~OrderPairResolver() {
+ if (orderPairTable != NULL) {
+ orderPairTable->resetAndDeleteVals();
+ delete orderPairTable;
+ }
}
-HappenedBefore OrderPairResolver::resolveOrder(uint64_t first, uint64_t second) {
+bool OrderPairResolver::resolveOrder(uint64_t first, uint64_t second) {
if (order->graph != NULL) {
// For the cases that tuning framework decides no to build a graph for order ...
OrderGraph *graph = order->graph;
- OrderNode *from = graph->getOrderNodeFromOrderGraph(first, false /*Don't create new node if doesn't exist*/);
- if (from == NULL) {
- return SATC_UNORDERED;
- }
- OrderNode *to = graph->getOrderNodeFromOrderGraph(second, false);
- if (from == NULL) {
- return SATC_UNORDERED;
- }
+ OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
+ ASSERT(from != NULL);
+ OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
+ ASSERT(to != NULL);
+
+ OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
- OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to, false /* Don't create a new edge*/);
if (edge != NULL && edge->mustPos) {
- return SATC_FIRST;
+ return true;
} else if ( edge != NULL && edge->mustNeg) {
- return SATC_SECOND;
+ return false;
}
}
//Couldn't infer from graph. Should call the SAT Solver ...
- switch ( order->type) {
- case SATC_TOTAL:
- resolveTotalOrder(first, second);
- case SATC_PARTIAL:
- //TODO: Support for partial order ...
- default:
- ASSERT(0);
- }
-
-
+ return getOrderConstraintValue(first, second);
}
-
-HappenedBefore OrderPairResolver::resolveTotalOrder(uint64_t first, uint64_t second) {
- ASSERT(order->orderPairTable != NULL);
- OrderPair pair(first, second, E_NULL);
- Edge var = getOrderConstraint(order->orderPairTable, &pair);
- if (edgeIsNull(var))
- return SATC_UNORDERED;
- return getValueCNF(solver->getSATEncoder()->getCNF(), var) ? SATC_FIRST : SATC_SECOND;
+bool OrderPairResolver::getOrderConstraintValue(uint64_t first, uint64_t second) {
+ ASSERT(first != second);
+ bool negate = false;
+ OrderPair tmp(first, second);
+ if (first < second) {
+ negate = true;
+ tmp.first = second;
+ tmp.second = first;
+ }
+ if (!orderPairTable->contains(&tmp)) {
+ return false;
+ }
+ OrderPair *pair = orderPairTable->get(&tmp);
+ return negate ? pair->getNegatedConstraintValue(solver) : pair->getConstraintValue(solver);
}