Merging with branch master and fixing bugs
authorHamed <hamed.gorjiara@gmail.com>
Tue, 29 Aug 2017 22:12:22 +0000 (15:12 -0700)
committerHamed <hamed.gorjiara@gmail.com>
Tue, 29 Aug 2017 22:12:22 +0000 (15:12 -0700)
1  2 
src/AST/order.cc
src/AST/order.h
src/ASTTransform/analyzer.cc
src/Collections/structs.h
src/classlist.h
src/csolver.cc

Simple merge
diff --cc 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();
index f416110,0000000..7d24ae2
mode 100644,000000..100644
--- /dev/null
@@@ -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; */
++      }
 +}
 +
 +
@@@ -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
@@@ -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
  #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 */