From: bdemsky <bdemsky@uci.edu>
Date: Tue, 19 Mar 2019 20:27:52 +0000 (-0700)
Subject: encapsulate order fields
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=bdb737849a5e0a2620e049dabfc0ba01f4ab23bb;p=satune.git

encapsulate order fields
---

diff --git a/src/AST/order.h b/src/AST/order.h
index cbbe846..a9015d6 100644
--- a/src/AST/order.h
+++ b/src/AST/order.h
@@ -15,18 +15,21 @@ public:
 	OrderType type;
 	Set *set;
 	OrderGraph *graph;
+	OrderEncoding encoding;
 	Order *clone(CSolver *solver, CloneMap *map);
 	void serialize(Serializer *serializer );
 	void print();
-	Vector<BooleanOrder *> constraints;
-	OrderEncoding encoding;
-
-	void setOrderResolver(OrderResolver *_resolver) { ASSERT(encoding.resolver == NULL); encoding.resolver = _resolver;};
+	void setOrderResolver(OrderResolver *_resolver) { ASSERT(encoding.resolver == NULL); encoding.resolver = _resolver;}
 	void initializeOrderElementsHashtable();
 	void addOrderConstraint(BooleanOrder *constraint);
 	void setOrderEncodingType(OrderEncodingType type);
 	HashtableOrderPair *getOrderPairTable();
 	CMEMALLOC;
+private:
+	Hashset64Int useditems;
+	Vector<BooleanOrder *> constraints;
+public:
+	Vector<BooleanOrder *> *getConstraints() {return &constraints;}
 };
 
 #endif
diff --git a/src/ASTAnalyses/Order/ordergraph.cc b/src/ASTAnalyses/Order/ordergraph.cc
index cbc2e25..57d0db8 100644
--- a/src/ASTAnalyses/Order/ordergraph.cc
+++ b/src/ASTAnalyses/Order/ordergraph.cc
@@ -12,9 +12,10 @@ OrderGraph::OrderGraph(Order *_order) :
 OrderGraph *buildOrderGraph(Order *order) {
 	ASSERT(order->graph == NULL);
 	OrderGraph *orderGraph = new OrderGraph(order);
-	uint constrSize = order->constraints.getSize();
+	Vector<BooleanOrder *> *constraints = order->getConstraints();
+	uint constrSize = constraints->getSize();
 	for (uint j = 0; j < constrSize; j++) {
-		orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j));
+		orderGraph->addOrderConstraintToOrderGraph(constraints->get(j));
 	}
 	return orderGraph;
 }
@@ -23,9 +24,10 @@ OrderGraph *buildOrderGraph(Order *order) {
 OrderGraph *buildMustOrderGraph(Order *order) {
 	ASSERT(order->graph == NULL);
 	OrderGraph *orderGraph = new OrderGraph(order);
-	uint constrSize = order->constraints.getSize();
+	Vector<BooleanOrder *> *constraints = order->getConstraints();
+	uint constrSize = constraints->getSize();
 	for (uint j = 0; j < constrSize; j++) {
-		orderGraph->addMustOrderConstraintToOrderGraph(order->constraints.get(j));
+		orderGraph->addMustOrderConstraintToOrderGraph(constraints->get(j));
 	}
 	return orderGraph;
 }
diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index e63cb74..2a4f4af 100644
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -88,9 +88,10 @@ void DecomposeOrderTransform::doTransform() {
 
 void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currGraph, DecomposeOrderResolver *dor) {
 	Vector<Order *> partialcandidatevec;
-	uint size = currOrder->constraints.getSize();
+	Vector<BooleanOrder *> *constraints = currOrder->getConstraints();
+	uint size = constraints->getSize();
 	for (uint i = 0; i < size; i++) {
-		BooleanOrder *orderconstraint = currOrder->constraints.get(i);
+		BooleanOrder *orderconstraint = constraints->get(i);
 		OrderNode *from = currGraph->getOrderNodeFromOrderGraph(orderconstraint->first);
 		OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second);
 		OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to);
diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index d5d769d..bd1fb4f 100644
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -35,9 +35,11 @@ void IntegerEncodingTransform::integerEncode(Order *currOrder) {
 	IntegerEncodingRecord *encodingRecord =  new IntegerEncodingRecord(
 		solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->set->getSize() - 1));
 	currOrder->setOrderEncodingType( INTEGERENCODING );
-	uint size = currOrder->constraints.getSize();
+
+	Vector<BooleanOrder *> *constraints = currOrder->getConstraints();
+	uint size = constraints->getSize();
 	for (uint i = 0; i < size; i++) {
-		orderIntegerEncodingSATEncoder(currOrder->constraints.get(i), encodingRecord);
+		orderIntegerEncodingSATEncoder(constraints->get(i), encodingRecord);
 	}
 	currOrder->setOrderResolver(new IntegerEncOrderResolver(solver, encodingRecord));
 	solver->getActiveOrders()->remove(currOrder);