From 9979be547581fdc1b75fdc09d006fa3497a7827c Mon Sep 17 00:00:00 2001 From: Hamed Date: Fri, 1 Sep 2017 16:45:39 -0700 Subject: [PATCH] Adding OrderPairResolver --- src/Backend/satorderencoder.cc | 3 ++ src/Translator/decomposeorderresolver.cc | 4 +- src/Translator/orderpairresolver.cc | 68 ++++++++++++++++++++++++ src/Translator/orderpairresolver.h | 26 +++++++++ src/Translator/sattranslator.cc | 8 --- src/Translator/sattranslator.h | 2 +- src/csolver.cc | 3 +- 7 files changed, 102 insertions(+), 12 deletions(-) create mode 100644 src/Translator/orderpairresolver.cc create mode 100644 src/Translator/orderpairresolver.h diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc index 31afdfc..514bad9 100644 --- a/src/Backend/satorderencoder.cc +++ b/src/Backend/satorderencoder.cc @@ -12,8 +12,11 @@ #include "element.h" #include "predicate.h" #include "orderelement.h" +#include "orderpairresolver.h" Edge SATEncoder::encodeOrderSATEncoder(BooleanOrder *constraint) { + //This is pairwised encoding ... + constraint->order->setOrderResolver(new OrderPairResolver(solver, constraint->order)); switch ( constraint->order->type) { case SATC_PARTIAL: return encodePartialOrderSATEncoder(constraint); diff --git a/src/Translator/decomposeorderresolver.cc b/src/Translator/decomposeorderresolver.cc index 6115295..28e3b56 100644 --- a/src/Translator/decomposeorderresolver.cc +++ b/src/Translator/decomposeorderresolver.cc @@ -18,7 +18,6 @@ DecomposeOrderResolver::DecomposeOrderResolver(OrderGraph* _graph, VectormustNeg){ return SATC_SECOND; }else { - switch(graph->getOrder()->encoding.type){ + switch(graph->getOrder()->type){ case SATC_TOTAL: return from->sccNum < to->sccNum? SATC_FIRST: SATC_SECOND; case SATC_PARTIAL: + //Adding support for partial order ... default: ASSERT(0); } diff --git a/src/Translator/orderpairresolver.cc b/src/Translator/orderpairresolver.cc new file mode 100644 index 0000000..fa147d0 --- /dev/null +++ b/src/Translator/orderpairresolver.cc @@ -0,0 +1,68 @@ + +/* + * File: orderpairresolver.cc + * Author: hamed + * + * Created on September 1, 2017, 3:36 PM + */ + +#include "orderpairresolver.h" +#include "ordergraph.h" +#include "order.h" +#include "orderedge.h" +#include "ordernode.h" +#include "satencoder.h" +#include "csolver.h" + +OrderPairResolver::OrderPairResolver(CSolver* _solver, Order* _order) : + solver(_solver), + order(_order) +{ +} + +OrderPairResolver::~OrderPairResolver() { +} + +HappenedBefore 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; + } + + OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to, false /* Don't create a new edge*/); + if (edge != NULL && edge->mustPos){ + return SATC_FIRST; + } else if( edge != NULL && edge->mustNeg){ + return SATC_SECOND; + } + } + + //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); + } + + +} + + +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; +} diff --git a/src/Translator/orderpairresolver.h b/src/Translator/orderpairresolver.h new file mode 100644 index 0000000..8063a90 --- /dev/null +++ b/src/Translator/orderpairresolver.h @@ -0,0 +1,26 @@ + +/* + * File: orderpairresolver.h + * Author: hamed + * + * Created on September 1, 2017, 3:36 PM + */ + +#ifndef ORDERPAIRRESOLVER_H +#define ORDERPAIRRESOLVER_H + +#include "orderresolver.h" + +class OrderPairResolver : public OrderResolver{ +public: + OrderPairResolver(CSolver* _solver, Order* _order); + HappenedBefore resolveOrder(uint64_t first, uint64_t second); + virtual ~OrderPairResolver(); +private: + CSolver* solver; + Order* order; + HappenedBefore resolveTotalOrder(uint64_t first, uint64_t second); +}; + +#endif /* ORDERPAIRRESOLVER_H */ + diff --git a/src/Translator/sattranslator.cc b/src/Translator/sattranslator.cc index 766c5c7..7c48be6 100644 --- a/src/Translator/sattranslator.cc +++ b/src/Translator/sattranslator.cc @@ -85,12 +85,4 @@ bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean) { return getValueSolver(This->getSATEncoder()->getCNF()->solver, index); } -HappenedBefore getOrderConstraintValueSATTranslator(CSolver *This, Order *order, 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(This->getSATEncoder()->getCNF(), var) ? SATC_FIRST : SATC_SECOND; -} diff --git a/src/Translator/sattranslator.h b/src/Translator/sattranslator.h index 1d9964f..3cfaf83 100644 --- a/src/Translator/sattranslator.h +++ b/src/Translator/sattranslator.h @@ -13,7 +13,7 @@ bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean); -HappenedBefore getOrderConstraintValueSATTranslator(CSolver *This, Order *order, uint64_t first, uint64_t second); + /** * most significant bit is represented by variable index 0 */ diff --git a/src/csolver.cc b/src/csolver.cc index 19ebe31..a2081b8 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -15,6 +15,7 @@ #include "autotuner.h" #include "astops.h" #include "structs.h" +#include "orderresolver.h" CSolver::CSolver() : boolTrue(new BooleanConst(true)), @@ -431,7 +432,7 @@ bool CSolver::getBooleanValue(Boolean *boolean) { } HappenedBefore CSolver::getOrderConstraintValue(Order *order, uint64_t first, uint64_t second) { - return getOrderConstraintValueSATTranslator(this, order, first, second); + return order->encoding.resolver->resolveOrder(first, second); } long long CSolver::getEncodeTime() { return satEncoder->getEncodeTime(); } -- 2.34.1