Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/constraint_compiler into...
authorHamed <hamed.gorjiara@gmail.com>
Wed, 6 Sep 2017 18:04:34 +0000 (11:04 -0700)
committerHamed <hamed.gorjiara@gmail.com>
Wed, 6 Sep 2017 18:04:34 +0000 (11:04 -0700)
src/AST/order.cc
src/AST/order.h
src/ASTAnalyses/ordergraph.cc
src/Backend/orderpair.cc
src/Backend/orderpair.h
src/Backend/satencoder.h
src/Backend/satorderencoder.cc
src/Translator/orderpairresolver.cc
src/Translator/orderpairresolver.h

index 35bca4a..609b469 100644 (file)
@@ -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;
        }
index cc8b45e..b1f0559 100644 (file)
@@ -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;
 };
 
index 2127db9..ce9a071 100644 (file)
@@ -184,16 +184,19 @@ bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination){
        SetIteratorOrderEdge *iterator = source->outEdges.iterator();
        bool found = false;
        while(iterator->hasNext()){
-               OrderNode* node = iterator->next()->sink;
-               if(!visited.contains(node)){
-                       if( node == destination ){
-                               found = true;
-                               break;
-                       }
-                       visited.add(node);
-                       found =isTherePathVisit(visited, node, destination);
-                       if(found){
-                               break;
+               OrderEdge* edge = iterator->next();
+               if(edge->polPos){
+                       OrderNode* node = edge->sink;
+                       if(!visited.contains(node)){
+                               if( node == destination ){
+                                       found = true;
+                                       break;
+                               }
+                               visited.add(node);
+                               found =isTherePathVisit(visited, node, destination);
+                               if(found){
+                                       break;
+                               }
                        }
                }
        }
@@ -205,15 +208,18 @@ bool OrderGraph::isTherePathVisit(HashsetOrderNode &visited, OrderNode* current,
        SetIteratorOrderEdge *iterator = current->outEdges.iterator();
        bool found = false;
        while(iterator->hasNext()){
-               OrderNode* node = iterator->next()->sink;
-               if(node == destination){
-                       found = true;
-                       break;
-               }
-               visited.add(node);
-               if(isTherePathVisit(visited, node, destination)){
-                       found = true;
-                       break;
+               OrderEdge* edge = iterator->next();
+               if(edge->polPos){
+                       OrderNode* node = edge->sink;
+                       if(node == destination){
+                               found = true;
+                               break;
+                       }
+                       visited.add(node);
+                       if(isTherePathVisit(visited, node, destination)){
+                               found = true;
+                               break;
+                       }
                }
        }
        delete iterator;
index 89913bb..abe29cc 100644 (file)
@@ -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));
+}
index aad68ff..f650648 100644 (file)
 
 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 */
index 7af3e55..ef3edc6 100644 (file)
@@ -64,5 +64,4 @@ private:
 };
 
 void allocElementConstraintVariables(ElementEncoding *ee, uint numVars);
-Edge getOrderConstraint(HashtableOrderPair *table, OrderPair *pair);
 #endif
index b977efa..91e2d80 100644 (file)
@@ -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);
index f0cb98d..e32a757 100644 (file)
 
 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);
 }
index bf7210c..dde7378 100644 (file)
@@ -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 */