From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Fri, 12 Oct 2018 21:54:56 +0000 (-0700)
Subject: Boolean Variable Ordering optimizations
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=c64cf3c2712780c3898523039fcfc49f7b306432

Boolean Variable Ordering optimizations
---

diff --git a/src/AST/astops.h b/src/AST/astops.h
index 97d2c28..a451c5f 100644
--- a/src/AST/astops.h
+++ b/src/AST/astops.h
@@ -25,6 +25,9 @@ enum ElementEncodingType {
 
 typedef enum ElementEncodingType ElementEncodingType;
 
+enum BooleanVarOrdering {CONSTRAINTORDERING=0, CHORONOLOGICALORDERING=1, REVERSEORDERING=2};
+typedef enum BooleanVarOrdering BooleanVarOrdering;
+
 Polarity negatePolarity(Polarity This);
 bool impliesPolarity(Polarity curr, Polarity goal);
 
diff --git a/src/ASTTransform/varorderingopt.cc b/src/ASTTransform/varorderingopt.cc
new file mode 100644
index 0000000..41f3edb
--- /dev/null
+++ b/src/ASTTransform/varorderingopt.cc
@@ -0,0 +1,52 @@
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+/* 
+ * File:   VarOrderingOpt.cpp
+ * Author: hamed
+ * 
+ * Created on October 11, 2018, 5:31 PM
+ */
+
+#include "varorderingopt.h"
+#include "csolver.h"
+#include "tunable.h"
+#include "satencoder.h"
+#include "elementencoding.h"
+#include "element.h"
+
+VarOrderingOpt::VarOrderingOpt(CSolver *_solver, SATEncoder *_satencoder): Transform(_solver){
+	satencoder = _satencoder;
+}
+
+VarOrderingOpt::~VarOrderingOpt() {
+}
+
+void VarOrderingOpt::doTransform(){
+	BooleanVarOrdering direction = (BooleanVarOrdering)solver->getTuner()->getTunable(VARIABLEORDER, &boolVarOrderingDesc);
+	if ( direction == CONSTRAINTORDERING ){
+		return;
+	}
+	
+	uint size = solver->allElements.getSize();
+	if(direction == CHORONOLOGICALORDERING){
+		for (uint i = 0; i < size; i++) {
+			Element *el = solver->allElements.get(i);
+			ElementEncoding *encoding = el->getElementEncoding();
+			if (encoding->getElementEncodingType() == ELEM_UNASSIGNED)
+				continue;
+			satencoder->encodeElementSATEncoder(el);
+		}
+	}else{
+		for (int i = size-1; i>0; i--) {
+			Element *el = solver->allElements.get(i);
+			ElementEncoding *encoding = el->getElementEncoding();
+			if (encoding->getElementEncodingType() == ELEM_UNASSIGNED)
+				continue;
+			satencoder->encodeElementSATEncoder(el);
+		}
+	}
+}
diff --git a/src/ASTTransform/varorderingopt.h b/src/ASTTransform/varorderingopt.h
new file mode 100644
index 0000000..efb0152
--- /dev/null
+++ b/src/ASTTransform/varorderingopt.h
@@ -0,0 +1,30 @@
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+/* 
+ * File:   VarOrderingOpt.h
+ * Author: hamed
+ *
+ * Created on October 11, 2018, 5:31 PM
+ */
+
+#ifndef VARORDERINGOPT_H
+#define VARORDERINGOPT_H
+
+#include "transform.h"
+
+
+class VarOrderingOpt :Transform {
+public:
+        VarOrderingOpt(CSolver *_solver, SATEncoder *_satencoder);
+        void doTransform();
+        virtual ~VarOrderingOpt();
+private:
+        SATEncoder* satencoder;
+};
+
+#endif /* VARORDERINGOPT_H */
+
diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 56be737..827a904 100644
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -69,6 +69,7 @@ private:
 	CSolver *solver;
 	BooleanToEdgeMap booledgeMap;
 	VectorEdge *vector;
+        friend class VarOrderingOpt;
 };
 
 void allocElementConstraintVariables(ElementEncoding *ee, uint numVars);
diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h
index c2a70b0..d838547 100644
--- a/src/Tuner/tunable.h
+++ b/src/Tuner/tunable.h
@@ -42,9 +42,10 @@ static TunableDesc proxyparameter(1, 5, 2);
 static TunableDesc mustValueBinaryIndex(5, 9, 8);
 static TunableDesc NodeEncodingDesc(ELEM_UNASSIGNED, BINARYINDEX, ELEM_UNASSIGNED);
 static TunableDesc NaiveEncodingDesc(ONEHOT, BINARYINDEX, ONEHOT);
+static TunableDesc boolVarOrderingDesc(CONSTRAINTORDERING, REVERSEORDERING, REVERSEORDERING);
 
 enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT, 
-        ENCODINGGRAPHOPT, ELEMENTOPTSETS, PROXYVARIABLE, MUSTVALUE, NAIVEENCODER};
+        ENCODINGGRAPHOPT, ELEMENTOPTSETS, PROXYVARIABLE, MUSTVALUE, NAIVEENCODER, VARIABLEORDER};
 typedef enum Tunables Tunables;
 
 const char *tunableParameterToString(Tunables tunable);
diff --git a/src/csolver.cc b/src/csolver.cc
index 9f374cc..983333b 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -26,6 +26,7 @@
 #include "orderedge.h"
 #include "orderanalysis.h"
 #include "elementopt.h"
+#include "varorderingopt.h"
 #include <time.h>
 #include <stdarg.h>
 
@@ -622,9 +623,12 @@ int CSolver::solve() {
 	naiveEncodingDecision(this);
 //	eg.validate();
 
+	VarOrderingOpt bor(this, satEncoder);
+	bor.doTransform();
+	
 	time2 = getTimeNano();
 	model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
-
+	
 	satEncoder->encodeAllSATEncoder(this);
 	time1 = getTimeNano();
 
diff --git a/src/csolver.h b/src/csolver.h
index 60e7c68..58484bd 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -222,6 +222,7 @@ private:
 	long long elapsedTime;
         long satsolverTimeout;
 	friend class ElementOpt;
+        friend class VarOrderingOpt;
 };
 
 inline CompOp flipOp(CompOp op) {