From 250304ccf75e2f6f6544022234dd5ad3ca7adbb2 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Tue, 19 Mar 2019 14:18:05 -0700
Subject: [PATCH] Support for pruning unused order elements

---
 src/AST/order.cc                    |  2 ++
 src/AST/order.h                     |  3 +++
 src/ASTTransform/integerencoding.cc |  2 +-
 src/Backend/satorderencoder.cc      | 34 +++++++++++++++--------------
 src/Collections/hashset.h           |  5 +++++
 5 files changed, 29 insertions(+), 17 deletions(-)

diff --git a/src/AST/order.cc b/src/AST/order.cc
index 315b112..82e4c53 100644
--- 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 a9015d6..d469cd9 100644
--- 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 bd1fb4f..34bcd74 100644
--- 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 9982039..6c254b9 100644
--- 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 86cbce9..05bb7af 100644
--- 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);
-- 
2.34.1