From: bdemsky <bdemsky@uci.edu>
Date: Sat, 2 Sep 2017 07:00:52 +0000 (-0700)
Subject: Make integerencoding a completely separate pass...  Fix issue of changing ordersets
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=04b29ee98bb1e665842f1cf1513b5a48f2b8c9c5;hp=d46ee65a6767e2016cab629220a60c3e39b366f1

Make integerencoding a completely separate pass...  Fix issue of changing ordersets
---

diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index ec8b020..85b43b1 100644
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -27,10 +27,10 @@ DecomposeOrderTransform::~DecomposeOrderTransform() {
 }
 
 void DecomposeOrderTransform::doTransform() {
-	Vector<Order *> *orders = solver->getOrders();
-	uint size = orders->getSize();
-	for (uint i = 0; i < size; i++) {
-		Order *order = orders->get(i);
+	HashsetOrder *orders = solver->getActiveOrders()->copy();
+	SetIteratorOrder * orderit=orders->iterator();
+	while(orderit->hasNext()) {
+		Order *order = orderit->next();
 
 		if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0) {
 			continue;
@@ -70,8 +70,11 @@ void DecomposeOrderTransform::doTransform() {
 		decomposeOrder(order, graph);
 		delete graph;
 	}
+	delete orderit;
+	delete orders;
 }
 
+
 void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *currGraph) {
 	Vector<Order *> ordervec;
 	Vector<Order *> partialcandidatevec;
@@ -122,6 +125,7 @@ void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr
 		}
 	}
 	currOrder->setOrderResolver( new DecomposeOrderResolver(currGraph, ordervec) );
+	solver->getActiveOrders()->remove(currOrder);
 	uint pcvsize = partialcandidatevec.getSize();
 	for (uint i = 0; i < pcvsize; i++) {
 		Order *neworder = partialcandidatevec.get(i);
diff --git a/src/ASTTransform/decomposeordertransform.h b/src/ASTTransform/decomposeordertransform.h
index 69f7a1f..1a2865c 100644
--- a/src/ASTTransform/decomposeordertransform.h
+++ b/src/ASTTransform/decomposeordertransform.h
@@ -20,8 +20,6 @@ public:
 
 	CMEMALLOC;
 private:
-	Order *currOrder;
-	OrderGraph *currGraph;
 };
 
 #endif/* ORDERTRANSFORM_H */
diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index d8150b3..6664a67 100644
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -18,13 +18,15 @@ IntegerEncodingTransform::~IntegerEncodingTransform() {
 }
 
 void IntegerEncodingTransform::doTransform() {
-	Vector<Order *> *orders = solver->getOrders();
-	uint size = orders->getSize();
-	for (uint i = 0; i < size; i++) {
-		Order *order = orders->get(i);
+	HashsetOrder *orders = solver->getActiveOrders()->copy();
+	SetIteratorOrder * orderit=orders->iterator();
+	while(orderit->hasNext()) {
+		Order *order = orderit->next();
 		if (GETVARTUNABLE(solver->getTuner(), order->type, ORDERINTEGERENCODING, &onoff))
 			integerEncode(order);
 	}
+	delete orders;
+	delete orderit;
 }
 
 void IntegerEncodingTransform::integerEncode(Order *currOrder) {
@@ -38,13 +40,14 @@ void IntegerEncodingTransform::integerEncode(Order *currOrder) {
 	}
 	uint size = currOrder->constraints.getSize();
 	for (uint i = 0; i < size; i++) {
-		orderIntegerEncodingSATEncoder(currOrder->constraints.get(i));
+		orderIntegerEncodingSATEncoder(currOrder, currOrder->constraints.get(i));
 	}
 	currOrder->setOrderResolver(new IntegerEncOrderResolver(solver, encodingRecord));
+	solver->getActiveOrders()->remove(currOrder);
 }
 
 
-void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder) {
+void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(Order * currOrder, BooleanOrder *boolOrder) {
 	IntegerEncodingRecord *ierec = orderIntEncoding->get(currOrder);
 	//getting two elements and using LT predicate ...
 	Element *elem1 = ierec->getOrderIntegerElement(solver, boolOrder->first);
diff --git a/src/ASTTransform/integerencoding.h b/src/ASTTransform/integerencoding.h
index f051a41..8066c2a 100644
--- a/src/ASTTransform/integerencoding.h
+++ b/src/ASTTransform/integerencoding.h
@@ -14,13 +14,12 @@
 class IntegerEncodingTransform : public Transform {
 public:
 	IntegerEncodingTransform(CSolver *solver);
-	void orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder);
+	void orderIntegerEncodingSATEncoder(Order * currOrder, BooleanOrder *boolOrder);
 	void doTransform();
 	void integerEncode(Order *currOrder);
 
 	virtual ~IntegerEncodingTransform();
 private:
-	Order *currOrder;
 	//FIXME:We can remove it, because we don't need it for translating anymore... -HG
 	HashTableOrderIntEncoding *orderIntEncoding;
 };
diff --git a/src/Collections/corestructs.h b/src/Collections/corestructs.h
index 1e808cb..982e0c5 100644
--- a/src/Collections/corestructs.h
+++ b/src/Collections/corestructs.h
@@ -5,6 +5,8 @@
 #include "hashset.h"
 
 typedef Hashset<Boolean *, uintptr_t, 4> HashsetBoolean;
+typedef Hashset<Order *, uintptr_t, 4> HashsetOrder;
 typedef SetIterator<Boolean *, uintptr_t, 4> SetIteratorBoolean;
+typedef SetIterator<Order *, uintptr_t, 4> SetIteratorOrder;
 
 #endif
diff --git a/src/csolver.cc b/src/csolver.cc
index de9543e..b351914 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -383,6 +383,7 @@ void CSolver::addConstraint(Boolean *constraint) {
 Order *CSolver::createOrder(OrderType type, Set *set) {
 	Order *order = new Order(type, set);
 	allOrders.push(order);
+	activeOrders.add(order);
 	return order;
 }
 
diff --git a/src/csolver.h b/src/csolver.h
index 1ff4cd1..7e8bbad 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -125,6 +125,7 @@ public:
 	bool isUnSAT() { return unsat; }
 
 	Vector<Order *> *getOrders() { return &allOrders;}
+	HashsetOrder * getActiveOrders() { return &activeOrders;}
 
 	Tuner *getTuner() { return tuner; }
 
@@ -173,6 +174,8 @@ private:
 	/** This is a vector of all order structs that we have allocated. */
 	Vector<Order *> allOrders;
 
+	HashsetOrder activeOrders;
+	
 	/** This is a vector of all function structs that we have allocated. */
 	Vector<Function *> allFunctions;