Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/constraint_compiler

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/ASTAnalyses/Order/ordergraph.cc b/src/ASTAnalyses/Order/ordergraph.cc
index 2127db9c466f06b647a54a0799ae667ffd11112a..ce9a0712f0e6f713c8c4bcabedbd59871e7f2306 100644 (file)
--- a/src/ASTAnalyses/Order/ordergraph.cc
+++ b/src/ASTAnalyses/Order/ordergraph.cc
@@ -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;

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..08ec52707c2fe57988df6670022be6263085e888 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -47,11 +47,14 @@ private:
        Edge encodeOrderSATEncoder(BooleanOrder *constraint);
        Edge inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second);
        Edge getPairConstraint(Order *order, OrderPair *pair);
+       Edge getPartialPairConstraint(Order *order, OrderPair *pair);
        Edge encodeTotalOrderSATEncoder(BooleanOrder *constraint);
        Edge encodePartialOrderSATEncoder(BooleanOrder *constraint);
        void createAllTotalOrderConstraintsSATEncoder(Order *order);
+       void createAllPartialOrderConstraintsSATEncoder(Order *order);
        Edge getOrderConstraint(HashtableOrderPair *table, OrderPair *pair);
        Edge generateTransOrderConstraintSATEncoder(Edge constIJ, Edge constJK, Edge constIK);
+       Edge generatePartialOrderConstraintsSATEncoder(Edge ij,Edge ji, Edge jk, Edge kj,Edge ik, Edge ki);
        Edge encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *constraint);
        Edge encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint);
        void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This);
@@ -64,5 +67,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..c90dcf17d44734b5f20948e35c36e22eeeba72d4 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,43 @@ 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;
+               tmp = new OrderPair(pair->first, pair->second, getNewVarSATEncoder());
+               table->put(tmp, tmp);
+       } else {
+               tmp = table->get(pair);
+       }
+       return negate ? tmp->getNegatedConstraint() : tmp->getConstraint();
+}
 
-       return negate ? constraintNegate(constraint) : constraint;
+Edge SATEncoder::getPartialPairConstraint(Order *order, OrderPair *pair) {
+       Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second);
+       if (!edgeIsNull(gvalue))
+               return gvalue;
+
+       HashtableOrderPair *table = order->getOrderPairTable();
+       
+       OrderPair* tmp;
+       if (!(table->contains(pair))) {
+               Edge constraint = getNewVarSATEncoder();
+               tmp = new OrderPair(pair->first, pair->second, constraint);
+               table->put(tmp, tmp);
+               Edge constraint2 = getNewVarSATEncoder();
+               OrderPair *swap = new OrderPair(pair->second, pair->first, constraint2);
+               table->put(swap, swap);
+               addConstraintCNF(cnf, constraintNegate(constraintAND2(cnf, constraint, constraint2)));
+       } else {
+               tmp = table->get(pair);
+       }
+       return 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 +140,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);
@@ -146,7 +148,109 @@ Edge SATEncoder::generateTransOrderConstraintSATEncoder(Edge constIJ,Edge constJ
        return constraintAND2(cnf, loop1, loop2);
 }
 
-Edge SATEncoder::encodePartialOrderSATEncoder(BooleanOrder *constraint) {
-       ASSERT(constraint->order->type == SATC_PARTIAL);
-       return E_BOGUS;
+Edge SATEncoder::generatePartialOrderConstraintsSATEncoder(Edge ij,Edge ji, Edge jk, Edge kj,Edge ik, Edge ki) {
+       Edge uoIJ = constraintAND2(cnf, constraintNegate(ij), constraintNegate(ji));
+       Edge uoJK = constraintAND2(cnf, constraintNegate(jk), constraintNegate(kj));
+       Edge uoIK = constraintAND2(cnf, constraintNegate(ik), constraintNegate(ki));
+               
+       Edge t1[] = {ij, jk, ik};
+       Edge t2[] = {ji, jk, ik};
+       Edge t3[] = {ij, kj, ki};
+       Edge t4[] = {ij, kj, ik};
+       Edge t5[] = {ji, jk, ki};
+       Edge t6[] = {ji, kj, ki};
+       Edge ct1 = constraintAND(cnf, 3, t1);
+       Edge ct2 = constraintAND(cnf, 3, t2);
+       Edge ct3 = constraintAND(cnf, 3, t3);
+       Edge ct4 = constraintAND(cnf, 3, t4);
+       Edge ct5 = constraintAND(cnf, 3, t5);
+       Edge ct6 = constraintAND(cnf, 3, t6);
+       
+       Edge p1[] = {uoIJ, jk, ik};
+       Edge p2[] = {ij, kj, uoIK};
+       Edge p3[] = {ji, uoJK, ki};
+       Edge p4[] = {uoIJ, kj, ki};
+       Edge p5[] = {ji, jk, uoIK};
+       Edge p6[] = {ij, uoJK, ik};
+       Edge cp1 = constraintAND(cnf, 3, p1);
+       Edge cp2 = constraintAND(cnf, 3, p2);
+       Edge cp3 = constraintAND(cnf, 3, p3);
+       Edge cp4 = constraintAND(cnf, 3, p4);
+       Edge cp5 = constraintAND(cnf, 3, p5);
+       Edge cp6 = constraintAND(cnf, 3, p6);
+       
+       Edge o1[] = {uoIJ, uoJK, ik};
+       Edge o2[] = {ij, uoJK, uoIK};
+       Edge o3[] = {uoIK, jk, uoIK};
+       Edge o4[] = {ji, uoJK, uoIK};
+       Edge o5[] = {uoIJ, uoJK, ki};
+       Edge o6[] = {uoIJ, kj, uoIK};
+       Edge co1 = constraintAND(cnf, 3, o1);
+       Edge co2 = constraintAND(cnf, 3, o2);
+       Edge co3 = constraintAND(cnf, 3, o3);
+       Edge co4 = constraintAND(cnf, 3, o4);
+       Edge co5 = constraintAND(cnf, 3, o5);
+       Edge co6 = constraintAND(cnf, 3, o6);
+       
+       Edge unorder [] = {uoIJ, uoJK, uoIK};
+       Edge cunorder = constraintAND(cnf, 3, unorder);
+       
+       
+       Edge res[] = {ct1,ct2,ct3,ct4,ct5,ct6,
+                       cp1,cp2,cp3,cp4,cp5,cp6,
+                       co1,co2,co3,co4,co5,co6,
+                       cunorder};
+       return constraintOR(cnf, 19, res);
+}
+
+Edge SATEncoder::encodePartialOrderSATEncoder(BooleanOrder *boolOrder) {
+       ASSERT(boolOrder->order->type == SATC_PARTIAL);
+       if (boolOrder->order->encoding.resolver == NULL) {
+               //This is pairwised encoding ...
+               boolOrder->order->setOrderResolver(new OrderPairResolver(solver, boolOrder->order));
+               bool doOptOrderStructure = GETVARTUNABLE(solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
+               if (doOptOrderStructure) {
+                       boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
+                       reachMustAnalysis(solver, boolOrder->order->graph, true);
+               }
+               createAllPartialOrderConstraintsSATEncoder(boolOrder->order);
+       }
+       OrderPair pair(boolOrder->first, boolOrder->second, E_NULL);
+       Edge constraint = getPartialPairConstraint(boolOrder->order, &pair);
+       return constraint;
 }
+
+
+void SATEncoder::createAllPartialOrderConstraintsSATEncoder(Order *order) {
+#ifdef CONFIG_DEBUG
+       model_print("in partial order ...\n");
+#endif
+       ASSERT(order->type == SATC_TOTAL);
+       Set *set = order->set;
+       uint size = order->set->getSize();
+       for (uint i = 0; i < size; i++) {
+               uint64_t valueI = set->getMemberAt(i);
+               for (uint j = i + 1; j < size; j++) {
+                       uint64_t valueJ = set->getMemberAt(j);
+                       OrderPair pairIJ(valueI, valueJ, E_NULL);
+                       OrderPair pairJI(valueJ, valueI, E_NULL);
+                       Edge constIJ = getPartialPairConstraint(order, &pairIJ);
+                       Edge constJI = getPartialPairConstraint(order, &pairJI);
+                       for (uint k = j + 1; k < size; k++) {
+                               uint64_t valueK = set->getMemberAt(k);
+                               OrderPair pairJK(valueJ, valueK, E_NULL);
+                               OrderPair pairIK(valueI, valueK, E_NULL);
+                               Edge constIK = getPartialPairConstraint(order, &pairIK);
+                               Edge constJK = getPartialPairConstraint(order, &pairJK);
+                               OrderPair pairKJ(valueK, valueJ, E_NULL);
+                               OrderPair pairKI(valueK, valueI, E_NULL);
+                               Edge constKI = getPartialPairConstraint(order, &pairKI);
+                               Edge constKJ = getPartialPairConstraint(order, &pairKJ);
+                               addConstraintCNF(cnf, generatePartialOrderConstraintsSATEncoder(constIJ, constJI,
+                                       constJK, constKJ, constIK, constKI));
+                       }
+               }
+       }
+}
+
+

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 */