Merging with branch master and fixing bugs

diff --combined src/AST/order.cc
index bf2e5662fb67e907e5d46d9e73a532f3a8bccdff,c9b0a7943def41aafbfd3c9bc19a464f9da9801b..0944bcae0e3b5ae9602ce351bbc25faeffe54eaa
--- 1/src/AST/order.cc
--- 2/src/AST/order.cc
+++ b/src/AST/order.cc
@@@ -3,11 -3,13 +3,12 @@@
  #include "set.h"
  #include "boolean.h"
  #include "ordergraph.h"
+ #include "csolver.h"
  
  Order::Order(OrderType _type, Set *_set) :
        type(_type),
        set(_set),
        orderPairTable(NULL),
 -      elementTable(NULL),
        graph(NULL),
        order(this)
  {
@@@ -17,6 -19,9 +18,6 @@@ void Order::initializeOrderHashTable() 
        orderPairTable = new HashTableOrderPair();
  }
  
 -void Order::initializeOrderElementsHashTable() {
 -      elementTable = new HashSetOrderElement();
 -}
  
  void Order::addOrderConstraint(BooleanOrder *constraint) {
        constraints.push(constraint);
@@@ -26,12 -31,23 +27,21 @@@ void Order::setOrderEncodingType(OrderE
        order.type = type;
  }
  
+ Order *Order::clone(CSolver *solver, CloneMap *map) {
+       Order *o = (Order *)map->get(this);
+       if (o != NULL)
+               return o;
+       o = solver->createOrder(type, set->clone(solver, map));
+       map->put(this, o);
+       return o;
+ }
+ 
  Order::~Order() {
        if (orderPairTable != NULL) {
                orderPairTable->resetanddelete();
                delete orderPairTable;
        }
 -      if (elementTable != NULL) {
 -              delete elementTable;
 -      }
 +      
        if (graph != NULL) {
                delete graph;
        }

diff --combined 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 --combined 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 --combined src/Collections/structs.h
index ef3beb55d0f1401ba2695e34b12f594bf858118b,43efbc542a7460a86a6a771d1f0eecb910056cc0..afe905fb31c350afb7f0e3d0fa82e2b3a0906554
--- 1/src/Collections/structs.h
--- 2/src/Collections/structs.h
+++ b/src/Collections/structs.h
@@@ -16,9 -16,6 +16,9 @@@ unsigned int order_element_hash_functio
  bool order_element_equals(OrderElement *key1, OrderElement *key2);
  unsigned int order_pair_hash_function(OrderPair *This);
  bool order_pair_equals(OrderPair *key1, OrderPair *key2);
 +unsigned int order_hash_function(Order *This);
 +bool order_pair_equals(Order *key1, Order *key2);
 +
  
  typedef HashSet<Boolean *, uintptr_t, 4> HashSetBoolean;
  typedef HashSet<TableEntry *, uintptr_t, 4, table_entry_hash_function, table_entry_equals> HashSetTableEntry;
@@@ -27,10 -24,12 +27,13 @@@ 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;
  typedef HSIterator<OrderNode *, uintptr_t, 4, order_node_hash_function, order_node_equals> HSIteratorOrderNode;
  
+ 
  #endif

diff --combined src/classlist.h
index e032cd566df216453691456b1e0a54cf25131b8a,97200ea301fc39b8247ecbef2aa6d38d048f6b5b..2e395f7ac87fc74b9a9cb45a5bf39dcbc76f8790
--- 1/src/classlist.h
--- 2/src/classlist.h
+++ b/src/classlist.h
@@@ -14,9 -14,7 +14,7 @@@
  #include <inttypes.h>
  
  class CSolver;
- struct SATEncoder;
- typedef struct SATEncoder SATEncoder;
- 
+ class SATEncoder;
  class Boolean;
  class BooleanOrder;
  class BooleanVar;
@@@ -43,8 -41,6 +41,8 @@@ class Order
  class OrderPair;
  
  class OrderElement;
 +class IntegerEncodingRecord;
 +class Transform;
  
  class ElementEncoding;
  class FunctionEncoding;
@@@ -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;
@@@ -63,9 -60,6 +64,6 @@@
  struct TableEntry;
  typedef struct TableEntry TableEntry;
  
- struct OrderEncoder;
- typedef struct OrderEncoder OrderEncoder;
- 
  class Tuner;
  class TunableDesc;
  

diff --combined 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 */
@@@ -56,8 -60,19 +60,19 @@@ CSolver::~CSolver() 
                delete allFunctions.get(i);
        }
  
-       deleteSATEncoder(satEncoder);
-       delete tuner;
+       delete satEncoder;
+ }
+ 
+ CSolver *CSolver::clone() {
+       CSolver *copy = new CSolver();
+       CloneMap map;
+       HSIteratorBoolean *it = getConstraints();
+       while (it->hasNext()) {
+               Boolean *b = it->next();
+               copy->addConstraint(b->clone(copy, &map));
+       }
+       delete it;
+       return copy;
  }
  
  Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
@@@ -95,15 -110,33 +110,33 @@@ Element *CSolver::getElementVar(Set *se
  }
  
  Element *CSolver::getElementConst(VarType type, uint64_t value) {
-       Element *element = new ElementConst(value, type);
-       allElements.push(element);
-       return element;
+       uint64_t array[] = {value};
+       Set *set = new Set(type, array, 1);
+       Element *element = new ElementConst(value, type, set);
+       Element *e = elemMap.get(element);
+       if (e == NULL) {
+               allSets.push(set);
+               allElements.push(element);
+               elemMap.put(element, element);
+               return element;
+       } else {
+               delete set;
+               delete element;
+               return e;
+       }
  }
  
- Boolean *CSolver::getBooleanVar(VarType type) {
-       Boolean *boolean = new BooleanVar(type);
-       allBooleans.push(boolean);
-       return boolean;
+ Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus) {
+       Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
+       Element *e = elemMap.get(element);
+       if (e == NULL) {
+               allElements.push(element);
+               elemMap.put(element, element);
+               return element;
+       } else {
+               delete element;
+               return e;
+       }
  }
  
  Function *CSolver::createFunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range,OverFlowBehavior overflowbehavior) {
@@@ -144,10 -177,10 +177,10 @@@ Function *CSolver::completeTable(Table 
        return function;
  }
  
- Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus) {
-       Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
-       allElements.push(element);
-       return element;
+ Boolean *CSolver::getBooleanVar(VarType type) {
+       Boolean *boolean = new BooleanVar(type);
+       allBooleans.push(boolean);
+       return boolean;
  }
  
  Boolean *CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) {
@@@ -156,14 -189,34 +189,34 @@@
  
  Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus) {
        BooleanPredicate *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
-       allBooleans.push(boolean);
-       return boolean;
+       Boolean * b = boolMap.get(boolean);
+       if (b == NULL) {
+               boolMap.put(boolean, boolean);
+               allBooleans.push(boolean);
+               return boolean;
+       } else {
+               delete boolean;
+               return b;
+       }
  }
  
  Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) {
        Boolean *boolean = new BooleanLogic(this, op, array, asize);
-       allBooleans.push(boolean);
-       return boolean;
+       Boolean *b = boolMap.get(boolean);
+       if (b == NULL) {
+               boolMap.put(boolean, boolean);
+               allBooleans.push(boolean);
+               return boolean;         
+       } else {
+               delete boolean;
+               return b;
+       }
+ }
+ 
+ Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
+       Boolean *constraint = new BooleanOrder(order, first, second);
+       allBooleans.push(constraint);
+       return constraint;
  }
  
  void CSolver::addConstraint(Boolean *constraint) {
@@@ -176,28 -229,30 +229,30 @@@ Order *CSolver::createOrder(OrderType t
        return order;
  }
  
- Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
-       Boolean *constraint = new BooleanOrder(order, first, second);
-       allBooleans.push(constraint);
-       return constraint;
- }
- 
  int CSolver::startEncoding() {
+       bool deleteTuner = false;
+       if (tuner == NULL) {
+               tuner = new DefaultTuner();
+               deleteTuner = true;
+       }
+               
+       long long startTime = getTimeNano();
        computePolarities(this);
        orderAnalysis(this);
        naiveEncodingDecision(this);
-       encodeAllSATEncoder(this, satEncoder);
-       int result = solveCNF(satEncoder->cnf);
-       model_print("sat_solver's result:%d\tsolutionSize=%d\n", result, satEncoder->cnf->solver->solutionsize);
-       for (int i = 1; i <= satEncoder->cnf->solver->solutionsize; i++) {
-               model_print("%d, ", satEncoder->cnf->solver->solution[i]);
+       satEncoder->encodeAllSATEncoder(this);
+       int result = unsat ? IS_UNSAT : satEncoder->solve();
+       long long finishTime = getTimeNano();
+       elapsedTime = finishTime - startTime;
+       if (deleteTuner) {
+               delete tuner;
+               tuner = NULL;
        }
-       model_print("\n");
        return result;
  }
  
  uint64_t CSolver::getElementValue(Element *element) {
-       switch (GETELEMENTTYPE(element)) {
+       switch (element->type) {
        case ELEMSET:
        case ELEMCONST:
        case ELEMFUNCRETURN:
@@@ -209,7 -264,7 +264,7 @@@
  }
  
  bool CSolver::getBooleanValue(Boolean *boolean) {
-       switch (GETBOOLEANTYPE(boolean)) {
+       switch (boolean->type) {
        case BOOLEANVAR:
                return getBooleanVariableValueSATTranslator(this, boolean);
        default:
@@@ -222,3 -277,13 +277,13 @@@ HappenedBefore CSolver::getOrderConstra
        return getOrderConstraintValueSATTranslator(this, order, first, second);
  }
  
+ long long CSolver::getEncodeTime() { return satEncoder->getEncodeTime(); }
+ 
+ long long CSolver::getSolveTime() { return satEncoder->getSolveTime(); }
+ 
+ void CSolver::autoTune(uint budget) {
+       AutoTuner * autotuner=new AutoTuner(budget);
+       autotuner->addProblem(this);
+       autotuner->tune();
+       delete autotuner;
+ }