Adding OrderPairResolver

diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index 31afdfc6d2858bccbf5cde66d02111b2ba2f2fe7..514bad902442f4dd0e496f1d0bd2256560c321e2 100644 (file)
--- 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 61152958cd8bbfe4616024dfb979346424a306f9..28e3b569b2f588107a4a5ca6f22cdc68fd4079c9 100644 (file)
--- a/src/Translator/decomposeorderresolver.cc
+++ b/src/Translator/decomposeorderresolver.cc
@@ -18,7 +18,6 @@ DecomposeOrderResolver::DecomposeOrderResolver(OrderGraph* _graph, Vector<Order*
 }
 
 DecomposeOrderResolver::~DecomposeOrderResolver() {
-       delete graph;
 }
 
 HappenedBefore DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t second){
@@ -37,10 +36,11 @@ HappenedBefore DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t sec
                } else if( edge != NULL && edge->mustNeg){
                        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 (file)
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 (file)
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 766c5c7cf6928f78e481a49d27d98ce85c09a06b..7c48be6324430b094e51477ac696b8f0075e9ebd 100644 (file)
--- 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 1d9964fe38755cabb1c845b38d5fbcaf76a04c4f..3cfaf83d893c7f9fb19140549344151a63ff8d41 100644 (file)
--- 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 19ebe3156e4691d63e19d4e91fc8549babc0d0f4..a2081b84efdfe822b12bb9bcfb6d1bf0d8016106 100644 (file)
--- 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(); }