Merging with branch master and fixing bugs

diff --cc src/AST/order.cc
Simple merge

diff --cc src/AST/order.h
index d60208ebc14c1360473cdfaf42142c3071f1c55c,e5f59838741fbc1e824333a2f2bb3e9fe8fd2033..f9bd69b5a3fdca34d6074a9c45399689ffd401bf
--- 1/src/AST/order.h
--- 2/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 f4161105fc6afef892c22a976b30f3bf46422230,0000000000000000000000000000000000000000..7d24ae27b00882e36f41ee48857034443ea83ef1
mode 100644,000000..100644
--- 1/src/ASTTransform/analyzer.cc
--- /dev/null
+++ b/src/ASTTransform/analyzer.cc
@@@ -1,78 -1,0 +1,78 @@@
- #include "orderencoder.h"
 +#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 "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;
 +
-               delete integerEncoding;
-       }
++              /*
 +              IntegerEncodingTransform* integerEncoding = new IntegerEncodingTransform(This, order, ORDERINTEGERENCODING, &offon);
 +              if(!integerEncoding->canExecuteTransform()){
 +                      continue;
 +                      delete integerEncoding;
 +              }
 +              integerEncoding->doTransform();
++              delete integerEncoding; */
++      }
 +}
 +
 +

diff --cc src/Collections/structs.h
index ef3beb55d0f1401ba2695e34b12f594bf858118b,43efbc542a7460a86a6a771d1f0eecb910056cc0..afe905fb31c350afb7f0e3d0fa82e2b3a0906554
--- 1/src/Collections/structs.h
--- 2/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 e032cd566df216453691456b1e0a54cf25131b8a,97200ea301fc39b8247ecbef2aa6d38d048f6b5b..2e395f7ac87fc74b9a9cb45a5bf39dcbc76f8790
--- 1/src/classlist.h
--- 2/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 814a140a1499189a8a387db86822a5be53bb02d2,06ecf78dddbb3b668ec36650879d81e5004affb2..db42f316afaff7d19da8dbe610f822df5c53f84f
--- 1/src/csolver.cc
--- 2/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 */