From: bdemsky <bdemsky@uci.edu>
Date: Mon, 11 Sep 2017 21:04:25 +0000 (-0700)
Subject: Extend tuning framework
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=7ce425ac7ed2ff3b348d1d8be37df8a5e3db21f2

Extend tuning framework
---

diff --git a/src/AST/astops.h b/src/AST/astops.h
index cd2beaa..e3c5963 100644
--- a/src/AST/astops.h
+++ b/src/AST/astops.h
@@ -16,4 +16,11 @@ typedef enum Polarity Polarity;
 enum BooleanValue {BV_UNDEFINED=0, BV_MUSTBETRUE=1, BV_MUSTBEFALSE=2, BV_UNSAT=3};
 typedef enum BooleanValue BooleanValue;
 
+enum ElementEncodingType {
+	ELEM_UNASSIGNED, ONEHOT, UNARY, BINARYINDEX, ONEHOTBINARY, BINARYVAL
+};
+
+typedef enum ElementEncodingType ElementEncodingType;
+
+
 #endif
diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index 8779975..f01958b 100644
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -4,6 +4,8 @@
 #include "function.h"
 #include "predicate.h"
 #include "set.h"
+#include "csolver.h"
+#include "tunable.h"
 
 EncodingGraph::EncodingGraph(CSolver * _solver) :
 	solver(_solver) {
@@ -106,6 +108,14 @@ uint EncodingNode::getSize() {
 	return s->getSize();
 }
 
+VarType EncodingNode::getType() {
+	return s->getType();
+}
+
+//ELEM_UNASSIGNED, ONEHOT, UNARY, BINARYINDEX, ONEHOTBINARY, BINARYVAL
+
+static TunableDesc NodeEncodingType(ELEM_UNASSIGNED, BINARYVAL, ELEM_UNASSIGNED);
+
 EncodingNode * EncodingGraph::createNode(Element *e) {
 	if (e->type == ELEMCONST)
 		return NULL;
@@ -113,6 +123,7 @@ EncodingNode * EncodingGraph::createNode(Element *e) {
 	EncodingNode *n = encodingMap.get(s);
 	if (n == NULL) {
 		n = new EncodingNode(s);
+		n->setEncoding((ElementEncodingType)solver->getTuner()->getVarTunable(n->getType(), NODEENCODING, &NodeEncodingType));
 		encodingMap.put(s, n);
 	}
 	n->addElement(e);
diff --git a/src/ASTAnalyses/Encoding/encodinggraph.h b/src/ASTAnalyses/Encoding/encodinggraph.h
index 7f7b8b4..62e3b8f 100644
--- a/src/ASTAnalyses/Encoding/encodinggraph.h
+++ b/src/ASTAnalyses/Encoding/encodinggraph.h
@@ -31,11 +31,15 @@ class EncodingNode {
 	EncodingNode(Set *_s);
 	void addElement(Element *e);
 	uint getSize();
+	VarType getType();
+	void setEncoding(ElementEncodingType e) {encoding=e;}
+	
 	CMEMALLOC;
  private:
 	Set *s;
 	HashsetElement elements;
 	uint numElements;
+	ElementEncodingType encoding;
 	friend class EncodingGraph;
 };
 
diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h
index d7585f4..6797c66 100644
--- a/src/Encoders/elementencoding.h
+++ b/src/Encoders/elementencoding.h
@@ -4,12 +4,6 @@
 #include "naiveencoder.h"
 #include "constraint.h"
 
-enum ElementEncodingType {
-	ELEM_UNASSIGNED, ONEHOT, UNARY, BINARYINDEX, ONEHOTBINARY, BINARYVAL
-};
-
-typedef enum ElementEncodingType ElementEncodingType;
-
 class ElementEncoding {
 public:
 	ElementEncoding(Element *element);
diff --git a/src/Tuner/searchtuner.cc b/src/Tuner/searchtuner.cc
index 52c7a70..3e95860 100644
--- a/src/Tuner/searchtuner.cc
+++ b/src/Tuner/searchtuner.cc
@@ -2,19 +2,29 @@
 
 TunableSetting::TunableSetting(VarType _type, TunableParam _param) :
 	hasVar(true),
-	type(_type),
+	type1(_type),
+	type2(0),
+	param(_param) {
+}
+
+TunableSetting::TunableSetting(VarType _type1, VarType _type2, TunableParam _param) :
+	hasVar(true),
+	type1(_type1),
+	type2(_type2),
 	param(_param) {
 }
 
 TunableSetting::TunableSetting(TunableParam _param) :
 	hasVar(false),
-	type(0),
+	type1(0),
+	type2(0),
 	param(_param) {
 }
 
 TunableSetting::TunableSetting(TunableSetting *ts) :
 	hasVar(ts->hasVar),
-	type(ts->type),
+	type1(ts->type1),
+	type2(ts->type2),
 	param(ts->param),
 	lowValue(ts->lowValue),
 	highValue(ts->highValue),
@@ -32,19 +42,21 @@ void TunableSetting::setDecision(int _low, int _high, int _default, int _selecti
 
 void TunableSetting::print() {
 	if (hasVar) {
-		model_print("Type %" PRIu64 ", ", type);
+		model_print("Type1 %" PRIu64 ", ", type1);
+		model_print("Type2 %" PRIu64 ", ", type2);
 	}
 	model_print("Param %u = %u\n", param, selectedValue);
 }
 
 unsigned int tunableSettingHash(TunableSetting *setting) {
-	return setting->hasVar ^ setting->type ^ setting->param;
+	return setting->hasVar ^ setting->type1 ^ setting->type2 ^ setting->param;
 }
 
 bool tunableSettingEquals(TunableSetting *setting1, TunableSetting *setting2) {
 	return setting1->hasVar == setting2->hasVar &&
-				 setting1->type == setting2->type &&
-				 setting1->param == setting2->param;
+		setting1->type1 == setting2->type1 &&
+		setting1->type2 == setting2->type2 &&
+		setting1->param == setting2->param;
 }
 
 SearchTuner::SearchTuner() {
@@ -88,12 +100,17 @@ int SearchTuner::getTunable(TunableParam param, TunableDesc *descriptor) {
 }
 
 int SearchTuner::getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor) {
-	TunableSetting setting(vartype, param);
+	return getVarTunable(vartype, 0, param, descriptor);
+}
+
+int SearchTuner::getVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor) {
+	TunableSetting setting(vartype1, vartype2, param);
 	TunableSetting *result = usedSettings.get(&setting);
 	if (result == NULL) {
 		result = settings.get(&setting);
 		if ( result == NULL) {
-			result = new TunableSetting(vartype, param);
+			result = new
+				TunableSetting(vartype1, vartype2, param);
 			uint value = descriptor->lowValue + (random() % (1 + descriptor->highValue - descriptor->lowValue));
 			result->setDecision(descriptor->lowValue, descriptor->highValue, descriptor->defaultValue, value);
 			settings.add(result);
diff --git a/src/Tuner/searchtuner.h b/src/Tuner/searchtuner.h
index 20edb7d..1464849 100644
--- a/src/Tuner/searchtuner.h
+++ b/src/Tuner/searchtuner.h
@@ -7,6 +7,7 @@
 class TunableSetting {
 public:
 	TunableSetting(VarType type, TunableParam param);
+	TunableSetting(VarType type1, VarType type2, TunableParam param);
 	TunableSetting(TunableParam param);
 	TunableSetting(TunableSetting *ts);
 	void setDecision(int _low, int _high, int _default, int _selection);
@@ -14,7 +15,8 @@ public:
 	CMEMALLOC;
 private:
 	bool hasVar;
-	VarType type;
+	VarType type1;
+	VarType type2;
 	TunableParam param;
 	int lowValue;
 	int highValue;
@@ -37,6 +39,7 @@ public:
 	~SearchTuner();
 	int getTunable(TunableParam param, TunableDesc *descriptor);
 	int getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor);
+	int getVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor);
 	SearchTuner *copyUsed();
 	void randomMutate();
 	uint getSize() { return usedSettings.getSize();}
diff --git a/src/Tuner/tunable.cc b/src/Tuner/tunable.cc
index 1401b24..eeba3a2 100644
--- a/src/Tuner/tunable.cc
+++ b/src/Tuner/tunable.cc
@@ -6,6 +6,11 @@ DefaultTuner::DefaultTuner() {
 int DefaultTuner::getTunable(TunableParam param, TunableDesc *descriptor) {
 	return descriptor->defaultValue;
 }
+
 int DefaultTuner::getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor) {
 	return descriptor->defaultValue;
 }
+
+int DefaultTuner::getVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor) {
+	return descriptor->defaultValue;
+}
diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h
index 660c77d..050d46f 100644
--- a/src/Tuner/tunable.h
+++ b/src/Tuner/tunable.h
@@ -7,6 +7,7 @@ class Tuner {
 public:
 	virtual int getTunable(TunableParam param, TunableDesc *descriptor) {ASSERT(0); return 0;}
 	virtual int getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor) {ASSERT(0); return 0;}
+	virtual int getVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor) {ASSERT(0); return 0;}
 	virtual ~Tuner() {}
 	CMEMALLOC;
 };
@@ -16,6 +17,7 @@ public:
 	DefaultTuner();
 	int getTunable(TunableParam param, TunableDesc *descriptor);
 	int getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor);
+	int getVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor);
 	CMEMALLOC;
 };
 
@@ -37,6 +39,6 @@ public:
 static TunableDesc onoff(0, 1, 1);
 static TunableDesc offon(0, 1, 0);
 
-enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS};
+enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING};
 typedef enum Tunables Tunables;
 #endif