From: bdemsky <bdemsky@uci.edu>
Date: Sun, 27 Aug 2017 07:08:54 +0000 (-0700)
Subject: towards cloning
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=919a30124bede022af832c5e33e42151f7c38533

towards cloning
---

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index 6ec1193..1eb2f00 100644
--- a/src/AST/boolean.cc
+++ b/src/AST/boolean.cc
@@ -3,6 +3,7 @@
 #include "csolver.h"
 #include "element.h"
 #include "order.h"
+#include "predicate.h"
 
 Boolean::Boolean(ASTNodeType _type) :
 	ASTNode(_type),
@@ -42,5 +43,36 @@ BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint a
 	inputs(array, asize) {
 }
 
-BooleanPredicate::~BooleanPredicate() {
+Boolean * BooleanVar::clone(CSolver *solver, CloneMap *map) {
+	if (map->boolean.contains(this)) {
+		return map->boolean.get(this);
+	} else {
+		Boolean * bvar=solver->getBooleanVar(type);
+		map->boolean.put(this, bvar);
+		return bvar;
+	}
+}
+
+Boolean * BooleanOrder::clone(CSolver * solver, CloneMap *map) {
+	Order * ordercopy=order->clone(map);
+	return solver->orderConstraint(ordercopy, first, second);
+}
+
+Boolean * BooleanLogic::clone(CSolver * solver, CloneMap *map) {
+	Boolean * array[inputs.getSize()];
+	for(uint i=0;i<inputs.getSize();i++) {
+		array[i]=inputs.get(i)->clone(solver, map);
+	}
+	return solver->applyLogicalOperation(op, array, inputs.getSize());
+}
+
+Boolean * BooleanPredicate::clone(CSolver * solver, CloneMap *map) {
+	Element * array[inputs.getSize()];
+	for(uint i=0;i<inputs.getSize();i++) {
+		array[i]=inputs.get(i)->clone(solver, map);
+	}
+	Predicate * pred=predicate->clone(map);
+	Boolean * defstatus=(undefStatus != NULL) ? undefStatus->clone(solver, map) : NULL;
+	
+	return solver->applyPredicateTable(pred, array, inputs.getSize(), defstatus);
 }
diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index c9722a9..2341fcf 100644
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -21,6 +21,7 @@ class Boolean : public ASTNode {
 public:
 	Boolean(ASTNodeType _type);
 	virtual ~Boolean() {}
+	virtual Boolean * clone(CSolver * solver, CloneMap *map);
 	Polarity polarity;
 	BooleanValue boolVal;
 	Vector<Boolean *> parents;
@@ -30,6 +31,8 @@ public:
 class BooleanVar : public Boolean {
 public:
 	BooleanVar(VarType t);
+	Boolean * clone(CSolver * solver, CloneMap *map);
+	
 	VarType vtype;
 	Edge var;
 	MEMALLOC;
@@ -38,6 +41,8 @@ public:
 class BooleanOrder : public Boolean {
 public:
 	BooleanOrder(Order *_order, uint64_t _first, uint64_t _second);
+	Boolean * clone(CSolver * solver, CloneMap *map);
+	
 	Order *order;
 	uint64_t first;
 	uint64_t second;
@@ -47,7 +52,8 @@ public:
 class BooleanPredicate : public Boolean {
 public:
 	BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, Boolean *_undefinedStatus);
-	~BooleanPredicate();
+	Boolean * clone(CSolver * solver, CloneMap *map);
+	
 	Predicate *predicate;
 	FunctionEncoding encoding;
 	Array<Element *> inputs;
@@ -59,6 +65,8 @@ public:
 class BooleanLogic : public Boolean {
 public:
 	BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint asize);
+	Boolean * clone(CSolver * solver, CloneMap *map);
+
 	LogicOp op;
 	Array<Boolean *> inputs;
 	MEMALLOC;
diff --git a/src/AST/element.cc b/src/AST/element.cc
index 32b372a..d6832f9 100644
--- a/src/AST/element.cc
+++ b/src/AST/element.cc
@@ -4,6 +4,7 @@
 #include "constraint.h"
 #include "function.h"
 #include "table.h"
+#include "csolver.h"
 
 Element::Element(ASTNodeType _type) :
 	ASTNode(_type),
@@ -25,9 +26,10 @@ ElementFunction::ElementFunction(Function *_function, Element **array, uint numA
 		GETELEMENTPARENTS(array[i])->push(this);
 }
 
-ElementConst::ElementConst(uint64_t _value, VarType _type) : Element(ELEMCONST), value(_value) {
-	uint64_t array[] = {value};
-	set = new Set(_type, array, 1);
+ElementConst::ElementConst(uint64_t _value, VarType _type, Set * _set) :
+	Element(ELEMCONST),
+	set(_set),
+	value(_value) {
 }
 
 Set *getElementSet(Element *This) {
@@ -54,12 +56,24 @@ Set *getElementSet(Element *This) {
 	return NULL;
 }
 
-ElementFunction::~ElementFunction() {
+Element * ElementConst::clone(CSolver *solver, CloneMap * map) {
+	return solver->getElementConst(type, value);
 }
-
-ElementConst::~ElementConst() {
-	delete set;
+		
+Element * ElementSet::clone(CSolver *solver, CloneMap * map) {
+	Element * e = map->element.get(this);
+	if (e != NULL)
+		return e;
+	e = solver->getElementVar(set->clone(solver, map));
+	map->element.put(e, e);
+	return e;
 }
 
-Element::~Element() {
+Element * ElementFunction::clone(CSolver *solver, CloneMap * map) {
+	Element * array[inputs.getSize()];
+	for(uint i=0; i<inputs.getSize(); i++) {
+		array[i]=inputs.get(i)->clone(solver, map);
+	}
+	Element * e = solver->applyFunction(function->clone(solver, map), array, inputs.getSize(), overflowstatus->clone(solver, map));
+	return e;
 }
diff --git a/src/AST/element.h b/src/AST/element.h
index f563586..a230055 100644
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -13,18 +13,19 @@
 class Element : public ASTNode {
 public:
 	Element(ASTNodeType type);
-	virtual ~Element();
+	virtual ~Element() {}
 	Vector<ASTNode *> parents;
 	ElementEncoding encoding;
+	virtual Element * clone(CSolver * solver, CloneMap * map);
 	MEMALLOC;
 };
 
 class ElementConst : public Element {
 public:
-	ElementConst(uint64_t value, VarType type);
-	~ElementConst();
+	ElementConst(uint64_t value, VarType type, Set *_set);
 	Set *set;
 	uint64_t value;
+	Element * clone(CSolver * solver, CloneMap * map);
 	MEMALLOC;
 };
 
@@ -32,17 +33,18 @@ class ElementSet : public Element {
 public:
 	ElementSet(Set *s);
 	Set *set;
+	Element * clone(CSolver * solver, CloneMap * map);
 	MEMALLOC;
 };
 
 class ElementFunction : public Element {
 public:
 	ElementFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus);
-	~ElementFunction();
 	Function *function;
 	Array<Element *> inputs;
 	Boolean *overflowstatus;
 	FunctionEncoding functionencoding;
+	Element * clone(CSolver * solver, CloneMap * map);
 	MEMALLOC;
 };
 
diff --git a/src/AST/function.h b/src/AST/function.h
index 2cd5cca..e00afd3 100644
--- a/src/AST/function.h
+++ b/src/AST/function.h
@@ -11,8 +11,9 @@ class Function {
 public:
 	Function(FunctionType _type) : type(_type) {}
 	FunctionType type;
-	MEMALLOC;
 	virtual ~Function() {}
+	virtual Function * clone(CSolver * solver, CloneMap *map);
+	MEMALLOC;
 };
 
 class FunctionOperator : public Function {
@@ -24,6 +25,7 @@ public:
 	FunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range, OverFlowBehavior overflowbehavior);
 	uint64_t applyFunctionOperator(uint numVals, uint64_t *values);
 	bool isInRangeFunction(uint64_t val);
+	Function * clone(CSolver * solver, CloneMap *map);
 	MEMALLOC;
 };
 
@@ -32,6 +34,7 @@ public:
 	Table *table;
 	UndefinedBehavior undefBehavior;
 	FunctionTable (Table *table, UndefinedBehavior behavior);
+	Function * clone(CSolver * solver, CloneMap *map);
 	MEMALLOC;
 };
 
diff --git a/src/AST/mutableset.cc b/src/AST/mutableset.cc
index 19f6dec..d029f82 100644
--- a/src/AST/mutableset.cc
+++ b/src/AST/mutableset.cc
@@ -1,4 +1,5 @@
 #include "mutableset.h"
+#include "csolver.h"
 
 MutableSet::MutableSet(VarType t) : Set(t) {
 }
@@ -6,3 +7,15 @@ MutableSet::MutableSet(VarType t) : Set(t) {
 void MutableSet::addElementMSet(uint64_t element) {
 	members->push(element);
 }
+
+Set * MutableSet::clone(CSolver * solver, CloneMap *map) {
+	Set * s=map->set.get(this);
+	if (s != NULL)
+		return s;
+	s=solver->createMutableSet(type);
+	for(uint i=0; i<members->getSize();i++) {
+		solver->addItem((MutableSet *) s, members->get(i));
+	}
+	map->set.put(this, s);
+	return s;
+}
diff --git a/src/AST/mutableset.h b/src/AST/mutableset.h
index 3c2f937..36ce011 100644
--- a/src/AST/mutableset.h
+++ b/src/AST/mutableset.h
@@ -6,6 +6,7 @@ class MutableSet : public Set {
 public:
 	MutableSet(VarType t);
 	void addElementMSet(uint64_t element);
+	Set * clone(CSolver * solver, CloneMap *map);
 	MEMALLOC;
 };
 #endif
diff --git a/src/AST/order.h b/src/AST/order.h
index 8d21240..b4abd07 100644
--- a/src/AST/order.h
+++ b/src/AST/order.h
@@ -17,6 +17,7 @@ public:
 	HashTableOrderPair *orderPairTable;
 	HashSetOrderElement *elementTable;
 	OrderGraph *graph;
+	Order * clone(CloneMap *map);
 	Vector<BooleanOrder *> constraints;
 	OrderEncoding order;
 	void initializeOrderHashTable();
diff --git a/src/AST/predicate.h b/src/AST/predicate.h
index 46bc5af..c86c6c2 100644
--- a/src/AST/predicate.h
+++ b/src/AST/predicate.h
@@ -11,6 +11,7 @@ class Predicate {
 public:
 	Predicate(PredicateType _type) : type(_type) {}
 	virtual ~Predicate() {}
+	virtual Predicate * clone(CloneMap *map);
 	PredicateType type;
 	MEMALLOC;
 };
@@ -19,6 +20,7 @@ class PredicateOperator : public Predicate {
 public:
 	PredicateOperator(CompOp op, Set **domain, uint numDomain);
 	bool evalPredicateOperator(uint64_t *inputs);
+	Predicate * clone(CloneMap *map);
 	CompOp op;
 	Array<Set *> domains;
 	MEMALLOC;
@@ -27,6 +29,7 @@ public:
 class PredicateTable : public Predicate {
 public:
 	PredicateTable(Table *table, UndefinedBehavior undefBehavior);
+	Predicate * clone(CloneMap *map);
 	Table *table;
 	UndefinedBehavior undefinedbehavior;
 	MEMALLOC;
diff --git a/src/AST/set.cc b/src/AST/set.cc
index 4b66dfe..d5b9c34 100644
--- a/src/AST/set.cc
+++ b/src/AST/set.cc
@@ -1,5 +1,6 @@
 #include "set.h"
 #include <stddef.h>
+#include "csolver.h"
 
 Set::Set(VarType t) : type(t), isRange(false), low(0), high(0) {
 	members = new Vector<uint64_t>();
@@ -44,3 +45,16 @@ Set::~Set() {
 	if (!isRange)
 		delete members;
 }
+
+Set * Set::clone(CSolver * solver, CloneMap *map) {
+	Set * s=map->set.get(this);
+	if (s != NULL)
+		return s;
+	if (isRange) {
+		s=solver->createRangeSet(type, low, high);
+	} else {
+		s=solver->createSet(type, members->expose(), members->getSize());
+	}
+	map->set.put(this, s);
+	return s;
+}
diff --git a/src/AST/set.h b/src/AST/set.h
index bb246b6..3ff404a 100644
--- a/src/AST/set.h
+++ b/src/AST/set.h
@@ -17,11 +17,12 @@ public:
 	Set(VarType t);
 	Set(VarType t, uint64_t *elements, uint num);
 	Set(VarType t, uint64_t lowrange, uint64_t highrange);
-	~Set();
+	virtual ~Set();
 	bool exists(uint64_t element);
 	uint getSize();
 	uint64_t getElement(uint index);
-
+	virtual Set * clone(CSolver * solver, CloneMap *map);
+	
 	VarType type;
 	bool isRange;
 	uint64_t low;//also used to count unique items
diff --git a/src/Collections/structs.h b/src/Collections/structs.h
index 28d290f..73f5bf5 100644
--- a/src/Collections/structs.h
+++ b/src/Collections/structs.h
@@ -24,10 +24,22 @@ typedef HashSet<OrderEdge *, uintptr_t, 4, order_edge_hash_function, order_edge_
 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<Order *, Order *, uintptr_t, 4> OrderMap;
+typedef HashTable<Boolean *, Boolean *, uintptr_t, 4> BooleanMap;
+typedef HashTable<Element *, Element *, uintptr_t, 4> ElementMap;
+typedef HashTable<Set *, Set *, uintptr_t, 4> SetMap;
+
+typedef struct CloneMap {
+	OrderMap order;
+	BooleanMap boolean;
+	ElementMap element;
+	SetMap set;
+} CloneMap;
 
 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 --git a/src/csolver.cc b/src/csolver.cc
index d825df5..dec85e0 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -60,6 +60,18 @@ CSolver::~CSolver() {
 	delete tuner;
 }
 
+CSolver * CSolver::clone() {
+	CSolver * copy=new CSolver();
+	CloneMap map;
+	HSIteratorBoolean * it=getConstraints();
+	while(it->hasNext()) {
+		Boolean *b=it->next();
+		b->clone(copy, &map);
+	}
+	delete it;
+	return copy;
+}
+
 Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
 	Set *set = new Set(type, elements, numelements);
 	allSets.push(set);
@@ -95,7 +107,10 @@ Element *CSolver::getElementVar(Set *set) {
 }
 
 Element *CSolver::getElementConst(VarType type, uint64_t value) {
-	Element *element = new ElementConst(value, type);
+	uint64_t array[] = {value};
+	Set * set = new Set(type, array, 1);
+	allSets.push(set);
+	Element *element = new ElementConst(value, type, set);
 	allElements.push(element);
 	return element;
 }
diff --git a/src/csolver.h b/src/csolver.h
index c1fd90b..115006f 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -116,7 +116,7 @@ public:
 	void replaceBooleanWithTrue(Boolean *bexpr);
 	void replaceBooleanWithFalse(Boolean *bexpr);
 	void replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb);
-
+	CSolver * clone();
 
 	MEMALLOC;