Moving OrderPairTable to the resolver + hide translation complexity in OrderPair...

diff --git a/src/AST/order.cc b/src/AST/order.cc
index 35bca4ac4b32fc6a972199363a4385a957b87681..609b4691e0db641ef15c24682595417b71478937 100644 (file)
--- a/src/AST/order.cc
+++ b/src/AST/order.cc
@@ -4,21 +4,16 @@
 #include "boolean.h"
 #include "ordergraph.h"
 #include "csolver.h"
+#include "orderpairresolver.h"
 
 Order::Order(OrderType _type, Set *_set) :
        type(_type),
        set(_set),
-       orderPairTable(NULL),
        graph(NULL),
        encoding(this)
 {
 }
 
-void Order::initializeOrderHashtable() {
-       orderPairTable = new HashtableOrderPair();
-}
-
-
 void Order::addOrderConstraint(BooleanOrder *constraint) {
        constraints.push(constraint);
 }
@@ -36,12 +31,16 @@ Order *Order::clone(CSolver *solver, CloneMap *map) {
        return o;
 }
 
-Order::~Order() {
-       if (orderPairTable != NULL) {
-               orderPairTable->resetanddelete();
-               delete orderPairTable;
+HashtableOrderPair* Order::getOrderPairTable(){
+       ASSERT( encoding.resolver != NULL);
+       if (OrderPairResolver* t = dynamic_cast<OrderPairResolver*>(encoding.resolver)){
+               return t->getOrderPairTable();
+       } else {
+               ASSERT(0);
        }
+}
 
+Order::~Order() {
        if (graph != NULL) {
                delete graph;
        }

diff --git a/src/AST/order.h b/src/AST/order.h
index cc8b45e4adc7774e6b3510ef66fa80309a82ebbd..b1f0559ed629010310bd344df5b40033a533bfbf 100644 (file)
--- a/src/AST/order.h
+++ b/src/AST/order.h
@@ -14,16 +14,15 @@ public:
        ~Order();
        OrderType type;
        Set *set;
-       HashtableOrderPair *orderPairTable;
        OrderGraph *graph;
        Order *clone(CSolver *solver, CloneMap *map);
        Vector<BooleanOrder *> constraints;
        OrderEncoding encoding;
        void setOrderResolver(OrderResolver *_resolver) { ASSERT(encoding.resolver == NULL); encoding.resolver = _resolver;};
-       void initializeOrderHashtable();
        void initializeOrderElementsHashtable();
        void addOrderConstraint(BooleanOrder *constraint);
        void setOrderEncodingType(OrderEncodingType type);
+       HashtableOrderPair* getOrderPairTable();
        CMEMALLOC;
 };
 

diff --git a/src/Backend/orderpair.cc b/src/Backend/orderpair.cc
index 89913bbfe00e5d34025c16b529c9ad65d473d13b..abe29cc64bf6144e80d0b7c072053b51bf98ed28 100644 (file)
--- a/src/Backend/orderpair.cc
+++ b/src/Backend/orderpair.cc
@@ -1,5 +1,7 @@
 #include "orderpair.h"
-
+#include "constraint.h"
+#include "csolver.h"
+#include "satencoder.h"
 
 OrderPair::OrderPair(uint64_t _first, uint64_t _second, Edge _constraint) :
        first(_first),
@@ -12,3 +14,22 @@ OrderPair::OrderPair() :
        second(0),
        constraint(E_NULL) {
 }
+
+OrderPair::~OrderPair(){
+}
+
+Edge OrderPair::getConstraint(){
+       return constraint;
+}
+
+Edge OrderPair::getNegatedConstraint(){
+       return constraintNegate(constraint);
+}
+
+bool OrderPair::getConstraintValue(CSolver* solver){
+       return getValueCNF(solver->getSATEncoder()->getCNF(), constraint);
+}
+
+bool OrderPair::getNegatedConstraintValue(CSolver* solver){
+       return getValueCNF(solver->getSATEncoder()->getCNF(), constraintNegate(constraint));
+}

diff --git a/src/Backend/orderpair.h b/src/Backend/orderpair.h
index aad68ff8315a15c2d6b21d0ed7edd30e2947b643..f65064819da76d111fc87d1eb9862971c7e7fe86 100644 (file)
--- a/src/Backend/orderpair.h
+++ b/src/Backend/orderpair.h
@@ -14,12 +14,20 @@
 
 class OrderPair {
 public:
-       OrderPair(uint64_t first, uint64_t second, Edge constraint);
+       OrderPair(uint64_t first, uint64_t second, Edge constraint = E_NULL);
        OrderPair();
+       virtual ~OrderPair();
+       virtual Edge getConstraint();
+       virtual bool getConstraintValue(CSolver* solver);
+       //for the cases that we swap first and second ... For total order is straight forward.
+       // but for partial order it has some complexity which should be hidden ... -HG
+       virtual Edge getNegatedConstraint();
+       virtual bool getNegatedConstraintValue(CSolver* solver);
        uint64_t first;
        uint64_t second;
-       Edge constraint;
        CMEMALLOC;
+protected:
+       Edge constraint;
 };
 
 #endif/* ORDERPAIR_H */

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 7af3e559178c87a1e7dc796ea715260d43a53ab4..ef3edc6a1eb8bbd810d9fe15d3ece0ddcdf8bb2c 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -64,5 +64,4 @@ private:
 };
 
 void allocElementConstraintVariables(ElementEncoding *ee, uint numVars);
-Edge getOrderConstraint(HashtableOrderPair *table, OrderPair *pair);
 #endif

diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index b977efa782c4ea963f03a4a3da6bbeac80b8da01..91e2d80b9c96f7a82574452edec7e16db258b8f4 100644 (file)
--- a/src/Backend/satorderencoder.cc
+++ b/src/Backend/satorderencoder.cc
@@ -56,7 +56,7 @@ Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) {
        if (!edgeIsNull(gvalue))
                return gvalue;
 
-       HashtableOrderPair *table = order->orderPairTable;
+       HashtableOrderPair *table = order->getOrderPairTable();
        bool negate = false;
        OrderPair flipped;
        if (pair->first < pair->second) {
@@ -65,23 +65,21 @@ Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) {
                flipped.second = pair->first;
                pair = &flipped;
        }
-       Edge constraint;
+       OrderPair* tmp;
        if (!(table->contains(pair))) {
-               constraint = getNewVarSATEncoder();
-               OrderPair *paircopy = new OrderPair(pair->first, pair->second, constraint);
-               table->put(paircopy, paircopy);
-       } else
-               constraint = table->get(pair)->constraint;
-
-       return negate ? constraintNegate(constraint) : constraint;
+               tmp = new OrderPair(pair->first, pair->second, getNewVarSATEncoder());
+               table->put(tmp, tmp);
+       } else {
+               tmp = table->get(pair);
+       }
+       return negate ? tmp->getNegatedConstraint() : tmp->getConstraint();
 }
 
 Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) {
        ASSERT(boolOrder->order->type == SATC_TOTAL);
-       if (boolOrder->order->orderPairTable == NULL) {
+       if (boolOrder->order->encoding.resolver == NULL) {
                //This is pairwised encoding ...
                boolOrder->order->setOrderResolver(new OrderPairResolver(solver, boolOrder->order));
-               boolOrder->order->initializeOrderHashtable();
                bool doOptOrderStructure = GETVARTUNABLE(solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
                if (doOptOrderStructure) {
                        boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
@@ -120,24 +118,6 @@ void SATEncoder::createAllTotalOrderConstraintsSATEncoder(Order *order) {
        }
 }
 
-Edge getOrderConstraint(HashtableOrderPair *table, OrderPair *pair) {
-       ASSERT(pair->first != pair->second);
-       bool negate = false;
-       OrderPair flipped;
-       if (pair->first < pair->second) {
-               negate = true;
-               flipped.first = pair->second;
-               flipped.second = pair->first;
-               pair = &flipped;
-       }
-       if (!table->contains(pair)) {
-               return E_NULL;
-       }
-       Edge constraint = table->get(pair)->constraint;
-       ASSERT(!edgeIsNull(constraint));
-       return negate ? constraintNegate(constraint) : constraint;
-}
-
 Edge SATEncoder::generateTransOrderConstraintSATEncoder(Edge constIJ,Edge constJK,Edge constIK) {
        Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
        Edge loop1 = constraintOR(cnf, 3, carray);

diff --git a/src/Translator/orderpairresolver.cc b/src/Translator/orderpairresolver.cc
index f0cb98d5e10c13c902c05807564a787bf3c9c78a..e32a757ffb57a1838a6c3b3f77f9a6c25907d4ba 100644 (file)
--- a/src/Translator/orderpairresolver.cc
+++ b/src/Translator/orderpairresolver.cc
@@ -16,11 +16,16 @@
 
 OrderPairResolver::OrderPairResolver(CSolver *_solver, Order *_order) :
        solver(_solver),
-       order(_order)
+       order(_order),
+       orderPairTable(new HashtableOrderPair())
 {
 }
 
 OrderPairResolver::~OrderPairResolver() {
+       if (orderPairTable != NULL) {
+               orderPairTable->resetanddelete();
+               delete orderPairTable;
+       }
 }
 
 bool OrderPairResolver::resolveOrder(uint64_t first, uint64_t second) {
@@ -42,24 +47,21 @@ bool OrderPairResolver::resolveOrder(uint64_t first, uint64_t 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);
-       }
-
-
+       return getOrderConstraintValue(first, second);
 }
 
-
-bool 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))
+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;
-       return getValueCNF(solver->getSATEncoder()->getCNF(), var);
+       }
+       OrderPair *pair = orderPairTable->get(&tmp);
+       return negate ? pair->getNegatedConstraintValue(solver) : pair->getConstraintValue(solver);
 }

diff --git a/src/Translator/orderpairresolver.h b/src/Translator/orderpairresolver.h
index bf7210cf7a3f74eb334481680e0c2809bafb5a58..dde73784c42d757cd7b2ce73de56acf40e0484a6 100644 (file)
--- a/src/Translator/orderpairresolver.h
+++ b/src/Translator/orderpairresolver.h
@@ -15,11 +15,14 @@ class OrderPairResolver : public OrderResolver {
 public:
        OrderPairResolver(CSolver *_solver, Order *_order);
        bool resolveOrder(uint64_t first, uint64_t second);
+       HashtableOrderPair* getOrderPairTable() { return orderPairTable;}
        virtual ~OrderPairResolver();
 private:
        CSolver *solver;
        Order *order;
-       bool resolveTotalOrder(uint64_t first, uint64_t second);
+       HashtableOrderPair *orderPairTable;
+       
+       bool getOrderConstraintValue(uint64_t first, uint64_t second);
 };
 
 #endif/* ORDERPAIRRESOLVER_H */