From: Hamed <hamed.gorjiara@gmail.com>
Date: Thu, 31 Aug 2017 02:32:15 +0000 (-0700)
Subject: Merging with branch Master
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=87e67ce60ad79d235655d7c74276ba27d1d98632

Merging with branch Master
---

87e67ce60ad79d235655d7c74276ba27d1d98632
diff --cc src/ASTTransform/integerencoding.cc
index 78b6c6e,d15c60e..411ddc9
--- a/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 9615245,6589df7..7085cf7
--- a/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 682b0c3,bafc018..2b2f190
--- a/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);
 +	inline Set* getSecondarySet() { return secondarySet; }
- 	MEMALLOC;
+ 	CMEMALLOC;
+ 	
  private:
 +	Set* secondarySet;
- 	HashSetOrderElement *elementTable;
+ 	HashsetOrderElement *elementTable;
  };
  
  #endif /* INTEGERENCODINGRECORD_H */
diff --cc src/ASTTransform/transformer.cc
index 03a6841,0000000..b22b87d
mode 100644,000000..100644
--- a/src/ASTTransform/transformer.cc
+++ b/src/ASTTransform/transformer.cc
@@@ -1,85 -1,0 +1,85 @@@
 +#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);
- 		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) {
- 			//solver pair of analysis is also optional
- 			if (order->type == PARTIAL) {
++			//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 9850955,ab2ef79..07913c9
--- a/src/Backend/orderelement.h
+++ b/src/Backend/orderelement.h
@@@ -15,13 -15,9 +15,13 @@@
  class OrderElement {
  public:
  	OrderElement(uint64_t item, Element *elem);
 +	inline uint getHash() {return (uint) item;}
 +	inline bool equals(OrderElement* oe){ return item == oe->item;}
 +	inline Element* getElement() { return elem; }
- 	MEMALLOC;
++	CMEMALLOC;
 +private:
  	uint64_t item;
  	Element *elem;
 -	CMEMALLOC;
  };
  
  
diff --cc src/Collections/structs.h
index b9fa704,d0c9185..c2ed0e9
--- a/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 0000000,fe2eab5..3769439
mode 000000,100644..100644
--- a/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/csolver.cc
index 707ac01,5ee5157..3d589b1
--- a/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 e28052a,85da23e..a067b2f
--- a/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();