From: Hamed <hamed.gorjiara@gmail.com>
Date: Tue, 29 Aug 2017 22:12:22 +0000 (-0700)
Subject: Merging with branch master and fixing bugs
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=db18e3357fda778cdf03b6338a0301b4bd9525c2;p=satune.git

Merging with branch master and fixing bugs
---

db18e3357fda778cdf03b6338a0301b4bd9525c2
diff --cc src/AST/order.h
index d60208e,e5f5983..f9bd69b
--- a/src/AST/order.h
+++ b/src/AST/order.h
@@@ -15,7 -15,9 +15,8 @@@ public
  	OrderType type;
  	Set *set;
  	HashTableOrderPair *orderPairTable;
 -	HashSetOrderElement *elementTable;
  	OrderGraph *graph;
+ 	Order *clone(CSolver *solver, CloneMap *map);
  	Vector<BooleanOrder *> constraints;
  	OrderEncoding order;
  	void initializeOrderHashTable();
diff --cc src/ASTTransform/analyzer.cc
index f416110,0000000..7d24ae2
mode 100644,000000..100644
--- a/src/ASTTransform/analyzer.cc
+++ b/src/ASTTransform/analyzer.cc
@@@ -1,78 -1,0 +1,78 @@@
 +#include "analyzer.h"
 +#include "common.h"
 +#include "order.h"
 +#include "boolean.h"
 +#include "ordergraph.h"
 +#include "ordernode.h"
 +#include "rewriter.h"
 +#include "orderedge.h"
 +#include "mutableset.h"
 +#include "ops.h"
 +#include "csolver.h"
- #include "orderencoder.h"
++#include "orderanalysis.h"
 +#include "tunable.h"
 +#include "transform.h"
 +#include "element.h"
 +#include "integerencoding.h"
 +#include "decomposeordertransform.h"
 +
 +void orderAnalysis(CSolver *This) {
 +	Vector<Order *> *orders = This->getOrders();
 +	uint size = orders->getSize();
 +	for (uint i = 0; i < size; i++) {
 +		Order *order = orders->get(i);
 +		DecomposeOrderTransform* decompose = new DecomposeOrderTransform(This, order, DECOMPOSEORDER, &onoff);
 +		if (!decompose->canExecuteTransform()){
 +			continue;
 +			delete decompose;
 +		}
 +
 +		OrderGraph *graph = buildOrderGraph(order);
 +		if (order->type == PARTIAL) {
 +			//Required to do SCC analysis for partial order graphs.  It
 +			//makes sure we don't incorrectly optimize graphs with negative
 +			//polarity edges
 +			completePartialOrderGraph(graph);
 +		}
 +
 +
 +		bool mustReachGlobal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
 +
 +		if (mustReachGlobal)
 +			reachMustAnalysis(This, graph, false);
 +
 +		bool mustReachLocal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
 +
 +		if (mustReachLocal) {
 +			//This pair of analysis is also optional
 +			if (order->type == PARTIAL) {
 +				localMustAnalysisPartial(This, graph);
 +			} else {
 +				localMustAnalysisTotal(This, graph);
 +			}
 +		}
 +
 +		bool mustReachPrune = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
 +
 +		if (mustReachPrune)
 +			removeMustBeTrueNodes(This, graph);
 +
 +		//This is needed for splitorder
 +		computeStronglyConnectedComponentGraph(graph);
 +		decompose->setOrderGraph(graph);
 +		decompose->doTransform();
 +		delete decompose;
 +		delete graph;
 +
- 		
++		/*
 +		IntegerEncodingTransform* integerEncoding = new IntegerEncodingTransform(This, order, ORDERINTEGERENCODING, &offon);
 +		if(!integerEncoding->canExecuteTransform()){
 +			continue;
 +			delete integerEncoding;
 +		}
 +		integerEncoding->doTransform();
- 		delete integerEncoding;
- 	}
++		delete integerEncoding; */
++ 	}
 +}
 +
 +
diff --cc src/Collections/structs.h
index ef3beb5,43efbc5..afe905f
--- a/src/Collections/structs.h
+++ b/src/Collections/structs.h
@@@ -27,7 -24,8 +27,9 @@@ typedef HashSet<OrderEdge *, uintptr_t
  typedef HashSet<OrderElement *, uintptr_t, 4, order_element_hash_function, order_element_equals> HashSetOrderElement;
  typedef HashTable<OrderNode *, HashSetOrderNode *, uintptr_t, 4> HashTableNodeToNodeSet;
  typedef HashTable<OrderPair *, OrderPair *, uintptr_t, 4, order_pair_hash_function, order_pair_equals> HashTableOrderPair;
+ typedef HashTable<void *, void *, uintptr_t, 4> CloneMap;
 +typedef HashTable<Order* , IntegerEncodingRecord*, uintptr_t, 4, order_hash_function, order_pair_equals> HashTableOrderIntegerEncoding; 
+ 
  typedef HSIterator<TableEntry *, uintptr_t, 4, table_entry_hash_function, table_entry_equals> HSIteratorTableEntry;
  typedef HSIterator<Boolean *, uintptr_t, 4> HSIteratorBoolean;
  typedef HSIterator<OrderEdge *, uintptr_t, 4, order_edge_hash_function, order_edge_equals> HSIteratorOrderEdge;
diff --cc src/classlist.h
index e032cd5,97200ea..2e395f7
--- a/src/classlist.h
+++ b/src/classlist.h
@@@ -54,8 -50,9 +52,11 @@@ class OrderGraph
  class OrderNode;
  class OrderEdge;
  
+ class AutoTuner;
+ class SearchTuner;
+ class TunableSetting;
 +class Pass;
 +class Transform;
  
  struct IncrementalSolver;
  typedef struct IncrementalSolver IncrementalSolver;
diff --cc src/csolver.cc
index 814a140,06ecf78..db42f31
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@@ -11,11 -11,15 +11,15 @@@
  #include "sattranslator.h"
  #include "tunable.h"
  #include "polarityassignment.h"
 -#include "orderdecompose.h"
 +#include "analyzer.h"
- 
- CSolver::CSolver() : unsat(false) {
- 	tuner = new Tuner();
- 	satEncoder = allocSATEncoder(this);
+ #include "autotuner.h"
+ 
+ CSolver::CSolver() :
+ 	unsat(false),
+ 	tuner(NULL),
+ 	elapsedTime(0)
+ {
+ 	satEncoder = new SATEncoder(this);
  }
  
  /** This function tears down the solver and the entire AST */