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

diff --git a/src/AST/order.cc b/src/AST/order.cc
index 315b112d1c2aae07dec86b71dfb8a7db345e29a1..82e4c5329d591b0826704c750e80cc62ff50c3c5 100644 (file)
--- a/src/AST/order.cc
+++ b/src/AST/order.cc
@@ -16,6 +16,8 @@ Order::Order(OrderType _type, Set *_set) :
 
 void Order::addOrderConstraint(BooleanOrder *constraint) {
        constraints.push(constraint);
+       useditems.add(constraint->first);
+       useditems.add(constraint->second);
 }
 
 void Order::setOrderEncodingType(OrderEncodingType type) {

diff --git a/src/AST/order.h b/src/AST/order.h
index cbbe8469fad13ba6072287bd573dbee10a000fdb..4badbdcb8da459e518002cd6069108b93eb31eb6 100644 (file)
--- a/src/AST/order.h
+++ b/src/AST/order.h
@@ -15,18 +15,24 @@ public:
        OrderType type;
        Set *set;
        OrderGraph *graph;
+       OrderEncoding encoding;
        Order *clone(CSolver *solver, CloneMap *map);
        void serialize(Serializer *serializer );
        void print();
-       Vector<BooleanOrder *> constraints;
-       OrderEncoding encoding;
-
-       void setOrderResolver(OrderResolver *_resolver) { ASSERT(encoding.resolver == NULL); encoding.resolver = _resolver;};
+       void setOrderResolver(OrderResolver *_resolver) { ASSERT(encoding.resolver == NULL); encoding.resolver = _resolver;}
        void initializeOrderElementsHashtable();
        void addOrderConstraint(BooleanOrder *constraint);
        void setOrderEncodingType(OrderEncodingType type);
        HashtableOrderPair *getOrderPairTable();
        CMEMALLOC;
+private:
+       Hashset64Int useditems;
+       Vector<BooleanOrder *> constraints;
+public:
+       Vector<BooleanOrder *> *getConstraints() {return &constraints;}
+       uint getNumUsed() {return constraints.getSize();}
+       SetIterator64Int *getUsedIterator() {return useditems.iterator();}
+
 };
 
 #endif

diff --git a/src/ASTAnalyses/Order/ordergraph.cc b/src/ASTAnalyses/Order/ordergraph.cc
index cbc2e2508f1b0821e2f833eaa36e136c6252780f..57d0db8c756fc5f28a8333f7b83e61cbcb6e59be 100644 (file)
--- a/src/ASTAnalyses/Order/ordergraph.cc
+++ b/src/ASTAnalyses/Order/ordergraph.cc
@@ -12,9 +12,10 @@ OrderGraph::OrderGraph(Order *_order) :
 OrderGraph *buildOrderGraph(Order *order) {
        ASSERT(order->graph == NULL);
        OrderGraph *orderGraph = new OrderGraph(order);
-       uint constrSize = order->constraints.getSize();
+       Vector<BooleanOrder *> *constraints = order->getConstraints();
+       uint constrSize = constraints->getSize();
        for (uint j = 0; j < constrSize; j++) {
-               orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j));
+               orderGraph->addOrderConstraintToOrderGraph(constraints->get(j));
        }
        return orderGraph;
 }
@@ -23,9 +24,10 @@ OrderGraph *buildOrderGraph(Order *order) {
 OrderGraph *buildMustOrderGraph(Order *order) {
        ASSERT(order->graph == NULL);
        OrderGraph *orderGraph = new OrderGraph(order);
-       uint constrSize = order->constraints.getSize();
+       Vector<BooleanOrder *> *constraints = order->getConstraints();
+       uint constrSize = constraints->getSize();
        for (uint j = 0; j < constrSize; j++) {
-               orderGraph->addMustOrderConstraintToOrderGraph(order->constraints.get(j));
+               orderGraph->addMustOrderConstraintToOrderGraph(constraints->get(j));
        }
        return orderGraph;
 }

diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index e63cb74c27dff8974a7b243e5319589ba53ae682..2a4f4af0a85e5ded2d490b1119810f51a649efe3 100644 (file)
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -88,9 +88,10 @@ void DecomposeOrderTransform::doTransform() {
 
 void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currGraph, DecomposeOrderResolver *dor) {
        Vector<Order *> partialcandidatevec;
-       uint size = currOrder->constraints.getSize();
+       Vector<BooleanOrder *> *constraints = currOrder->getConstraints();
+       uint size = constraints->getSize();
        for (uint i = 0; i < size; i++) {
-               BooleanOrder *orderconstraint = currOrder->constraints.get(i);
+               BooleanOrder *orderconstraint = constraints->get(i);
                OrderNode *from = currGraph->getOrderNodeFromOrderGraph(orderconstraint->first);
                OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second);
                OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to);

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index d5d769dfc4ad1b5fa99f8aba56c8d5f5c15b5539..34bcd745b47e1134d665574f601a5de78e9f4acb 100644 (file)
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -33,11 +33,13 @@ void IntegerEncodingTransform::doTransform() {
 
 void IntegerEncodingTransform::integerEncode(Order *currOrder) {
        IntegerEncodingRecord *encodingRecord =  new IntegerEncodingRecord(
-               solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->set->getSize() - 1));
+               solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->getNumUsed() - 1));
        currOrder->setOrderEncodingType( INTEGERENCODING );
-       uint size = currOrder->constraints.getSize();
+
+       Vector<BooleanOrder *> *constraints = currOrder->getConstraints();
+       uint size = constraints->getSize();
        for (uint i = 0; i < size; i++) {
-               orderIntegerEncodingSATEncoder(currOrder->constraints.get(i), encodingRecord);
+               orderIntegerEncodingSATEncoder(constraints->get(i), encodingRecord);
        }
        currOrder->setOrderResolver(new IntegerEncOrderResolver(solver, encodingRecord));
        solver->getActiveOrders()->remove(currOrder);

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 63b5a619babcdd4f9b7152457436f55c05fe7e1a..84329ef4e5295317122b6ca2e5579afb67d87a6d 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -55,6 +55,8 @@ private:
        Edge encodePartialOrderSATEncoder(BooleanOrder *constraint);
        void createAllTotalOrderConstraintsSATEncoder(Order *order);
        void createAllPartialOrderConstraintsSATEncoder(Order *order);
+       void createAllTotalOrderConstraintsSATEncoderSparse(Order *order);
+       void createAllPartialOrderConstraintsSATEncoderSparse(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);

diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index 9982039333a6da897c17afc6e5ff54d3d303c7cd..e3d2f334da517a35fe7a1e83d354687627b703a3 100644 (file)
--- a/src/Backend/satorderencoder.cc
+++ b/src/Backend/satorderencoder.cc
@@ -108,7 +108,10 @@ Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) {
                        boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
                        reachMustAnalysis(solver, boolOrder->order->graph, true);
                }
-               createAllTotalOrderConstraintsSATEncoder(boolOrder->order);
+               if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0)
+                       createAllTotalOrderConstraintsSATEncoderSparse(boolOrder->order);
+               else
+                       createAllTotalOrderConstraintsSATEncoder(boolOrder->order);
        }
        OrderPair pair(boolOrder->first, boolOrder->second, E_NULL);
        Edge constraint = getPairConstraint(boolOrder->order, &pair);
@@ -214,7 +217,10 @@ Edge SATEncoder::encodePartialOrderSATEncoder(BooleanOrder *boolOrder) {
                        boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
                        reachMustAnalysis(solver, boolOrder->order->graph, true);
                }
-               createAllPartialOrderConstraintsSATEncoder(boolOrder->order);
+               if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0)
+                       createAllPartialOrderConstraintsSATEncoderSparse(boolOrder->order);
+               else
+                       createAllPartialOrderConstraintsSATEncoder(boolOrder->order);
        }
        OrderPair pair(boolOrder->first, boolOrder->second, E_NULL);
        Edge constraint = getPartialPairConstraint(boolOrder->order, &pair);
@@ -254,4 +260,63 @@ void SATEncoder::createAllPartialOrderConstraintsSATEncoder(Order *order) {
        }
 }
 
+void SATEncoder::createAllTotalOrderConstraintsSATEncoderSparse(Order *order) {
+#ifdef CONFIG_DEBUG
+       model_print("in total order ...\n");
+#endif
+       ASSERT(order->type == SATC_TOTAL);
+       SetIterator64Int *iti = order->getUsedIterator();
+       while (iti->hasNext()) {
+               uint64_t valueI = iti->next();
+               SetIterator64Int *itj = new SetIterator64Int(iti);
+               while (itj->hasNext()) {
+                       uint64_t valueJ = itj->next();
+                       OrderPair pairIJ(valueI, valueJ, E_NULL);
+                       Edge constIJ = getPairConstraint(order, &pairIJ);
+                       SetIterator64Int *itk = new SetIterator64Int(itj);
+                       while (itk->hasNext()) {
+                               uint64_t valueK = itk->next();
+                               OrderPair pairJK(valueJ, valueK, E_NULL);
+                               OrderPair pairIK(valueI, valueK, E_NULL);
+                               Edge constIK = getPairConstraint(order, &pairIK);
+                               Edge constJK = getPairConstraint(order, &pairJK);
+                               addConstraintCNF(cnf, generateTransOrderConstraintSATEncoder(constIJ, constJK, constIK));
+                       }
+               }
+       }
+}
 
+void SATEncoder::createAllPartialOrderConstraintsSATEncoderSparse(Order *order) {
+#ifdef CONFIG_DEBUG
+       model_print("in partial order ...\n");
+#endif
+       ASSERT(order->type == SATC_TOTAL);
+       SetIterator64Int *iti = order->getUsedIterator();
+       while (iti->hasNext()) {
+               uint64_t valueI = iti->next();
+               SetIterator64Int *itj = new SetIterator64Int(iti);
+               while (itj->hasNext()) {
+                       uint64_t valueJ = itj->next();
+                       OrderPair pairIJ(valueI, valueJ, E_NULL);
+                       OrderPair pairJI(valueJ, valueI, E_NULL);
+                       Edge constIJ = getPartialPairConstraint(order, &pairIJ);
+                       Edge constJI = getPartialPairConstraint(order, &pairJI);
+                       SetIterator64Int *itk = new SetIterator64Int(itj);
+                       while (itk->hasNext()) {
+                               uint64_t valueK = itk->next();
+                               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/Collections/hashset.h b/src/Collections/hashset.h
index 86cbce90530034c52b19364a68426b1588dc521a..05bb7af2b42edaa8329b60e97840e790de9d1245 100644 (file)
--- a/src/Collections/hashset.h
+++ b/src/Collections/hashset.h
@@ -30,6 +30,11 @@ public:
        {
        }
 
+       SetIterator(SetIterator *s) : curr(s->curr),
+               last(s->last),
+               set(s->set) {
+       }
+
        /** Override: new operator */
        void *operator new(size_t size) {
                return ourmalloc(size);