Adding OrderPairResolver
authorHamed <hamed.gorjiara@gmail.com>
Fri, 1 Sep 2017 23:45:39 +0000 (16:45 -0700)
committerHamed <hamed.gorjiara@gmail.com>
Fri, 1 Sep 2017 23:45:39 +0000 (16:45 -0700)
src/Backend/satorderencoder.cc
src/Translator/decomposeorderresolver.cc
src/Translator/orderpairresolver.cc [new file with mode: 0644]
src/Translator/orderpairresolver.h [new file with mode: 0644]
src/Translator/sattranslator.cc
src/Translator/sattranslator.h
src/csolver.cc

index 31afdfc..514bad9 100644 (file)
 #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);
index 6115295..28e3b56 100644 (file)
@@ -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
@@ -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
@@ -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 */
+
index 766c5c7..7c48be6 100644 (file)
@@ -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;
-}
 
index 1d9964f..3cfaf83 100644 (file)
@@ -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
  */
index 19ebe31..a2081b8 100644 (file)
@@ -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(); }