Support for pruning unused order elements

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 a9015d64c26f5a59995efdde34ccee0e8226d538..d469cd97cc46537bd0851f8f6f079731f064a710 100644 (file)
--- a/src/AST/order.h
+++ b/src/AST/order.h
@@ -24,12 +24,15 @@ public:
        void addOrderConstraint(BooleanOrder *constraint);
        void setOrderEncodingType(OrderEncodingType type);
        HashtableOrderPair *getOrderPairTable();
+       SetIterator64Int *getUsedIterator();
        CMEMALLOC;
 private:
        Hashset64Int useditems;
        Vector<BooleanOrder *> constraints;
 public:
        Vector<BooleanOrder *> *getConstraints() {return &constraints;}
+       uint getNumUsed() {return constraints.getSize();}
+
 };
 
 #endif

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index bd1fb4f869c17a1182874e57f41635ec82e9d56c..34bcd745b47e1134d665574f601a5de78e9f4acb 100644 (file)
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -33,7 +33,7 @@ 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 );
 
        Vector<BooleanOrder *> *constraints = currOrder->getConstraints();

diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index 9982039333a6da897c17afc6e5ff54d3d303c7cd..6c254b98a2c98cff1ee6ffa24b5f46e8c726dbff 100644 (file)
--- a/src/Backend/satorderencoder.cc
+++ b/src/Backend/satorderencoder.cc
@@ -121,16 +121,17 @@ void SATEncoder::createAllTotalOrderConstraintsSATEncoder(Order *order) {
        model_print("in total 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->getElement(i);
-               for (uint j = i + 1; j < size; j++) {
-                       uint64_t valueJ = set->getElement(j);
+       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);
-                       for (uint k = j + 1; k < size; k++) {
-                               uint64_t valueK = set->getElement(k);
+                       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);
@@ -227,18 +228,19 @@ void SATEncoder::createAllPartialOrderConstraintsSATEncoder(Order *order) {
        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->getElement(i);
-               for (uint j = i + 1; j < size; j++) {
-                       uint64_t valueJ = set->getElement(j);
+       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);
-                       for (uint k = j + 1; k < size; k++) {
-                               uint64_t valueK = set->getElement(k);
+                       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);

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);