Merging with branch Master

diff --cc src/ASTTransform/integerencoding.cc
index 78b6c6e5b0387a9f83932107c36e0f3ad0150c31,d15c60e365798254924277c8fd77c0fe86935359..411ddc9ddafeab489c9ce3e0b368c8d67847562a
--- 1/src/ASTTransform/integerencoding.cc
--- 2/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@@ -34,12 -35,12 +34,12 @@@ void IntegerEncodingTransform::doTransf
  
  
  void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder) {
 -      IntegerEncodingRecord* ierec = orderIntegerEncoding->get(order);
 -      //getting two elements and using SATC_LT predicate ...
 +      IntegerEncodingRecord* ierec = orderIntEncoding->get(currOrder);
 +      //getting two elements and using LT predicate ...
        Element *elem1 = ierec->getOrderIntegerElement(solver, boolOrder->first);
        Element *elem2 = ierec->getOrderIntegerElement(solver, boolOrder->second);
 -      Set *sarray[] = {ierec->set, ierec->set};
 +      Set *sarray[] = {ierec->getSecondarySet(), ierec->getSecondarySet()};
-       Predicate *predicate = solver->createPredicateOperator(LT, sarray, 2);
+       Predicate *predicate = solver->createPredicateOperator(SATC_LT, sarray, 2);
        Element *parray[] = {elem1, elem2};
        Boolean *boolean = solver->applyPredicate(predicate, parray, 2);
        solver->addConstraint(boolean);

diff --cc src/ASTTransform/integerencodingrecord.cc
index 961524570d09109c9acf27beaf1d042fa70bff2d,6589df76df30f22a3e4cc80cbcdbe8d79cbcd863..7085cf7f9c5e7d916d2c92d941122f28dc6ba133
--- 1/src/ASTTransform/integerencodingrecord.cc
--- 2/src/ASTTransform/integerencodingrecord.cc
+++ b/src/ASTTransform/integerencodingrecord.cc
@@@ -10,9 -10,9 +10,9 @@@
  #include "orderelement.h"
  
  IntegerEncodingRecord::IntegerEncodingRecord(Set* _set):
 -      set(_set)
 +      secondarySet(_set)
  {
-       elementTable = new HashSetOrderElement();
+       elementTable = new HashsetOrderElement();
  }
  
  IntegerEncodingRecord::~IntegerEncodingRecord(){

diff --cc src/ASTTransform/integerencodingrecord.h
index 682b0c3867fae96d6054e4a6a3c8ee0baf3869a1,bafc01812314ad943b79adb2fe9cb44063b5adf1..2b2f1902b7faf94b192015241f3ebd4fd00941f2
--- 1/src/ASTTransform/integerencodingrecord.h
--- 2/src/ASTTransform/integerencodingrecord.h
+++ b/src/ASTTransform/integerencodingrecord.h
@@@ -16,11 -16,11 +16,12 @@@ public
        IntegerEncodingRecord(Set* set);
        ~IntegerEncodingRecord();
        Element* getOrderIntegerElement(CSolver *This, uint64_t item);
-       MEMALLOC;
 +      inline Set* getSecondarySet() { return secondarySet; }
+       CMEMALLOC;
+       
  private:
-       HashSetOrderElement *elementTable;
 +      Set* secondarySet;
+       HashsetOrderElement *elementTable;
  };
  
  #endif /* INTEGERENCODINGRECORD_H */

diff --cc src/ASTTransform/transformer.cc
index 03a684101f334fc12b88261af29fd113dee7c3be,0000000000000000000000000000000000000000..b22b87d6c2abe20ccec957e7b1cbf48a844fa6f3
mode 100644,000000..100644
--- 1/src/ASTTransform/transformer.cc
--- /dev/null
+++ b/src/ASTTransform/transformer.cc
@@@ -1,85 -1,0 +1,85 @@@
-               if (order->type == PARTIAL) {
 +#include "transformer.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"
 +
 +Transformer::Transformer(CSolver *_solver):
 +      integerEncoding(new IntegerEncodingTransform(_solver)),
 +      solver(_solver)
 +{
 +}
 +
 +Transformer::~Transformer(){
 +      delete integerEncoding;
 +}
 +
 +void Transformer::orderAnalysis() {
 +      Vector<Order *> *orders = solver->getOrders();
 +      uint size = orders->getSize();
 +      for (uint i = 0; i < size; i++) {
 +              Order *order = orders->get(i);
 +              DecomposeOrderTransform* decompose = new DecomposeOrderTransform(solver, order);
 +              if (!decompose->canExecuteTransform()){
 +                      delete decompose;
 +                      continue;
 +              }
 +
 +              OrderGraph *graph = buildOrderGraph(order);
-                       //solver pair of analysis is also optional
-                       if (order->type == PARTIAL) {
++              if (order->type == SATC_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(solver->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
 +
 +              if (mustReachGlobal)
 +                      reachMustAnalysis(solver, graph, false);
 +
 +              bool mustReachLocal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
 +
 +              if (mustReachLocal) {
++                      //This pair of analysis is also optional
++                      if (order->type == SATC_PARTIAL) {
 +                              localMustAnalysisPartial(solver, graph);
 +                      } else {
 +                              localMustAnalysisTotal(solver, graph);
 +                      }
 +              }
 +
 +              bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
 +
 +              if (mustReachPrune)
 +                      removeMustBeTrueNodes(solver, graph);
 +
 +              //This is needed for splitorder
 +              computeStronglyConnectedComponentGraph(graph);
 +              decompose->setOrderGraph(graph);
 +              decompose->doTransform();
 +              delete decompose;
 +              delete graph;
 +
 +              integerEncoding->setCurrentOrder(order);
 +              if(!integerEncoding->canExecuteTransform()){
 +                      continue;
 +              }
 +              integerEncoding->doTransform();
 +      }
 +}
 +
 +

diff --cc src/Backend/orderelement.h
index 98509558e694a00a03d02c98aa2c4f2f7f47e333,ab2ef7916d85bc6dc67bcaf614815b3e3f2e8b0b..07913c9aa4fd5a85be0fbe2d2d99d0abec752c43
--- 1/src/Backend/orderelement.h
--- 2/src/Backend/orderelement.h
+++ b/src/Backend/orderelement.h
@@@ -15,13 -15,9 +15,13 @@@
  class OrderElement {
  public:
        OrderElement(uint64_t item, Element *elem);
-       MEMALLOC;
 +      inline uint getHash() {return (uint) item;}
 +      inline bool equals(OrderElement* oe){ return item == oe->item;}
 +      inline Element* getElement() { return elem; }
++      CMEMALLOC;
 +private:
        uint64_t item;
        Element *elem;
 -      CMEMALLOC;
  };
  
  

diff --cc src/Collections/structs.cc
Simple merge

diff --cc src/Collections/structs.h
index b9fa704d1ce31524f4ed411fe64e96d08457b9c1,d0c9185857ed489330263a2c00c9d29b7f2bbe6d..c2ed0e9201ae6a12aef16550e0c85cbf002d0a29
--- 1/src/Collections/structs.h
--- 2/src/Collections/structs.h
+++ b/src/Collections/structs.h
@@@ -16,25 -17,21 +17,21 @@@ 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;
- typedef HashSet<OrderNode *, uintptr_t, 4, order_node_hash_function, order_node_equals> HashSetOrderNode;
- typedef HashSet<OrderEdge *, uintptr_t, 4, order_edge_hash_function, order_edge_equals> HashSetOrderEdge;
- typedef HashSet<OrderElement *, uintptr_t, 4, order_element_hash_function, order_element_equals> HashSetOrderElement;
 -
+ typedef Hashset<TableEntry *, uintptr_t, 4, table_entry_hash_function, table_entry_equals> HashsetTableEntry;
+ typedef Hashset<OrderNode *, uintptr_t, 4, order_node_hash_function, order_node_equals> HashsetOrderNode;
+ typedef Hashset<OrderEdge *, uintptr_t, 4, order_edge_hash_function, order_edge_equals> HashsetOrderEdge;
+ 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> HashTableOrderIntEncoding; 
+ 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> HashtableOrderIntegerEncoding; 
++typedef Hashtable<Order* , IntegerEncodingRecord*, uintptr_t, 4> HashTableOrderIntEncoding; 
  
- 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;
- typedef HSIterator<OrderElement *, uintptr_t, 4, order_element_hash_function, order_element_equals> HSIteratorOrderElement;
+ typedef SetIterator<TableEntry *, uintptr_t, 4, table_entry_hash_function, table_entry_equals> SetIteratorTableEntry;
+ typedef SetIterator<OrderEdge *, uintptr_t, 4, order_edge_hash_function, order_edge_equals> SetIteratorOrderEdge;
+ typedef SetIterator<OrderNode *, uintptr_t, 4, order_node_hash_function, order_node_equals> SetIteratorOrderNode;
 -
++typedef SetIterator<OrderElement *, uintptr_t, 4, order_element_hash_function, order_element_equals> SetIteratorOrderElement;
  
  #endif

diff --cc src/classes.h
index 0000000000000000000000000000000000000000,fe2eab5f9ca0af16a3548cf114e9b2c7d8d00ae0..37694398f69271a16014e92b321bb2d3bf083ca5
mode 000000,100644..100644
--- /dev/null
--- 2/src/classes.h
+++ b/src/classes.h
@@@ -1,0 -1,31 +1,32 @@@
+ /*      Copyright (c) 2015 Regents of the University of California
+  *
+  *      Author: Brian Demsky <bdemsky@uci.edu>
+  *
+  *      This program is free software; you can redistribute it and/or
+  *      modify it under the terms of the GNU General Public License
+  *      version 2 as published by the Free Software Foundation.
+  */
+ 
+ #ifndef CLASSES_H
+ #define CLASSES_H
+ 
+ #include "mymemory.h"
+ #include <inttypes.h>
+ 
+ class SATEncoder;
+ class CSolver;
+ class Boolean;
+ class Element;
+ class Predicate;
+ class Table;
+ class Order;
+ class MutableSet;
+ class Function;
+ class Tuner;
++class Transformer;
+ class Set;
+ class BooleanLogic;
+ typedef uint64_t VarType;
+ typedef unsigned int uint;
+ 
+ #endif

diff --cc src/classlist.h
Simple merge

diff --cc src/csolver.cc
index 707ac01e9fdd1f1cf1e43257a0b3fc805300db81,5ee5157d31f29246f3d6dddd0c7058947d217e6f..3d589b18f94da8668ecfc1233eef4c05ee3ee243
--- 1/src/csolver.cc
--- 2/src/csolver.cc
+++ b/src/csolver.cc
@@@ -11,10 -11,14 +11,14 @@@
  #include "sattranslator.h"
  #include "tunable.h"
  #include "polarityassignment.h"
 -#include "analyzer.h"
 +#include "transformer.h"
  #include "autotuner.h"
+ #include "astops.h"
+ #include "structs.h"
  
  CSolver::CSolver() :
+       boolTrue(new BooleanConst(true)),
+       boolFalse(new BooleanConst(false)),
        unsat(false),
        tuner(NULL),
        elapsedTime(0)
@@@ -61,8 -64,9 +65,10 @@@ CSolver::~CSolver() 
                delete allFunctions.get(i);
        }
  
+       delete boolTrue;
+       delete boolFalse;
        delete satEncoder;
 +      delete transformer;
  }
  
  CSolver *CSolver::clone() {

diff --cc src/csolver.h
index e28052a389637d7cb9c262d206acf41a086029a4,85da23e117e8c0e5b4f5c699bbc4f16209b8a3fc..a067b2fa1cb1495c7a4bba4329534e88efea5974
--- 1/src/csolver.h
--- 2/src/csolver.h
+++ b/src/csolver.h
@@@ -109,9 -113,8 +113,9 @@@ public
        Vector<Order *> *getOrders() { return &allOrders;}
  
        Tuner *getTuner() { return tuner; }
 +      Transformer* getTransformer() {return transformer;}
        
-       HSIteratorBoolean *getConstraints() { return constraints.iterator(); }
+       SetIteratorBoolean *getConstraints() { return constraints.iterator(); }
  
        SATEncoder *getSATEncoder() {return satEncoder;}
  
@@@ -121,7 -124,6 +125,7 @@@
        CSolver *clone();
        void autoTune(uint budget);
  
-       void setTuner(Transformer * _transformer) {  transformer = _transformer; }
++      void setTransformer(Transformer * _transformer) {  transformer = _transformer; }
        void setTuner(Tuner * _tuner) { tuner = _tuner; }
        long long getElapsedTime() { return elapsedTime; }
        long long getEncodeTime();