From: Hamed <hamed.gorjiara@gmail.com>
Date: Mon, 4 Sep 2017 10:06:13 +0000 (-0700)
Subject: Fixing more bugs
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=38f94182e16317a86b84b9a3915d5f16a8769779

Fixing more bugs
---

diff --git a/src/AST/order.h b/src/AST/order.h
index d922235..cc8b45e 100644
--- a/src/AST/order.h
+++ b/src/AST/order.h
@@ -19,7 +19,7 @@ public:
 	Order *clone(CSolver *solver, CloneMap *map);
 	Vector<BooleanOrder *> constraints;
 	OrderEncoding encoding;
-	void setOrderResolver(OrderResolver *_resolver) { encoding.resolver = _resolver;};
+	void setOrderResolver(OrderResolver *_resolver) { ASSERT(encoding.resolver == NULL); encoding.resolver = _resolver;};
 	void initializeOrderHashtable();
 	void initializeOrderElementsHashtable();
 	void addOrderConstraint(BooleanOrder *constraint);
diff --git a/src/ASTAnalyses/ordergraph.cc b/src/ASTAnalyses/ordergraph.cc
index fcc9eda..bb241de 100644
--- a/src/ASTAnalyses/ordergraph.cc
+++ b/src/ASTAnalyses/ordergraph.cc
@@ -13,6 +13,7 @@ OrderGraph::OrderGraph(Order *_order) :
 
 OrderGraph *buildOrderGraph(Order *order) {
 	OrderGraph *orderGraph = new OrderGraph(order);
+	order->graph = orderGraph;
 	uint constrSize = order->constraints.getSize();
 	for (uint j = 0; j < constrSize; j++) {
 		orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j));
diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index 7d276e2..359a3a3 100644
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -60,17 +60,15 @@ void DecomposeOrderTransform::doTransform() {
 			}
 		}
 
-		/*
+		
 		bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
 
 		if (mustReachPrune)
 			removeMustBeTrueNodes(solver, graph);
-		*/
 		
 		//This is needed for splitorder
 		computeStronglyConnectedComponentGraph(graph);
 		decomposeOrder(order, graph);
-		delete graph;
 	}
 	delete orderit;
 	delete orders;
diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index a4aacdf..ab88f20 100644
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -35,6 +35,7 @@ void IntegerEncodingTransform::integerEncode(Order *currOrder) {
 		encodingRecord = new IntegerEncodingRecord(
 			solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->set->getSize() - 1));
 		orderIntEncoding->put(currOrder, encodingRecord);
+		currOrder->setOrderEncodingType( INTEGERENCODING );
 	} else {
 		encodingRecord = orderIntEncoding->get(currOrder);
 	}
diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc
index 466d839..2d77608 100644
--- a/src/Encoders/naiveencoder.cc
+++ b/src/Encoders/naiveencoder.cc
@@ -28,7 +28,8 @@ void naiveEncodingConstraint(Boolean *This) {
 		return;
 	}
 	case ORDERCONST: {
-		((BooleanOrder *) This)->order->setOrderEncodingType(PAIRWISE);
+		if(((BooleanOrder *) This)->order->encoding.type == ORDER_UNASSIGNED)
+			((BooleanOrder *) This)->order->setOrderEncodingType(PAIRWISE);
 		return;
 	}
 	case LOGICOP: {
diff --git a/src/Test/ordertest.cc b/src/Test/ordertest.cc
index 8633415..d9ad852 100755
--- a/src/Test/ordertest.cc
+++ b/src/Test/ordertest.cc
@@ -15,9 +15,15 @@ int main(int numargs, char **argv) {
 	BooleanEdge b2 =  solver->orderConstraint(order, 1, 4);
 	solver->addConstraint(b1);
 	solver->addConstraint(b2);
-	if (solver->solve() == 1)
+	if (solver->solve() == 1){
 		printf("SAT\n");
-	else
+		printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n", 
+			solver->getOrderConstraintValue(order, 5, 1), 
+			solver->getOrderConstraintValue(order, 1, 4),
+			solver->getOrderConstraintValue(order, 5, 4),
+			solver->getOrderConstraintValue(order, 1, 5));
+	} else {
 		printf("UNSAT\n");
+	}
 	delete solver;
 }
diff --git a/src/csolver.cc b/src/csolver.cc
index b353791..f52c4eb 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -400,12 +400,11 @@ int CSolver::solve() {
 	long long startTime = getTimeNano();
 	computePolarities(this);
 
-	DecomposeOrderTransform dot(this);
-	dot.doTransform();
+//	DecomposeOrderTransform dot(this);
+//	dot.doTransform();
 
-	//This leaks like crazy
-	//	IntegerEncodingTransform iet(this);
-	//iet.doTransform();
+	IntegerEncodingTransform iet(this);
+	iet.doTransform();
 
 	naiveEncodingDecision(this);
 	satEncoder->encodeAllSATEncoder(this);