Merging with branch Master
authorHamed <hamed.gorjiara@gmail.com>
Thu, 31 Aug 2017 02:32:15 +0000 (19:32 -0700)
committerHamed <hamed.gorjiara@gmail.com>
Thu, 31 Aug 2017 02:32:15 +0000 (19:32 -0700)
1  2 
src/ASTTransform/integerencoding.cc
src/ASTTransform/integerencodingrecord.cc
src/ASTTransform/integerencodingrecord.h
src/ASTTransform/transformer.cc
src/Backend/orderelement.h
src/Collections/structs.cc
src/Collections/structs.h
src/classes.h
src/classlist.h
src/csolver.cc
src/csolver.h

@@@ -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);
@@@ -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(){
@@@ -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 */
index 03a6841,0000000..b22b87d
mode 100644,000000..100644
--- /dev/null
@@@ -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();
 +      }
 +}
 +
 +
  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;
  };
  
  
Simple merge
@@@ -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 0000000,fe2eab5..3769439
mode 000000,100644..100644
--- /dev/null
@@@ -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
  #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
@@@ -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;}
  
        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();