Support for pruning unused order elements
authorbdemsky <bdemsky@uci.edu>
Tue, 19 Mar 2019 21:18:05 +0000 (14:18 -0700)
committerbdemsky <bdemsky@uci.edu>
Tue, 19 Mar 2019 21:18:05 +0000 (14:18 -0700)
src/AST/order.cc
src/AST/order.h
src/ASTTransform/integerencoding.cc
src/Backend/satorderencoder.cc
src/Collections/hashset.h

index 315b112..82e4c53 100644 (file)
@@ -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) {
index a9015d6..d469cd9 100644 (file)
@@ -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
index bd1fb4f..34bcd74 100644 (file)
@@ -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();
index 9982039..6c254b9 100644 (file)
@@ -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);
index 86cbce9..05bb7af 100644 (file)
@@ -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);