From c9df82de0310e76de1f3b9b24e1d78115705a5f1 Mon Sep 17 00:00:00 2001
From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Thu, 26 Jul 2018 19:01:48 -0700
Subject: [PATCH] Now the Tuner decides about creating proxy variables

---
 src/Backend/satencoder.cc          |  6 +++++-
 src/Backend/satfunctableencoder.cc | 20 +++++++++++++-------
 src/Tuner/tunable.h                |  2 +-
 3 files changed, 19 insertions(+), 9 deletions(-)

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index 8dab3ab..dde77c1 100644
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -11,6 +11,7 @@
 #include "order.h"
 #include "predicate.h"
 #include "set.h"
+#include "tunable.h"
 
 SATEncoder::SATEncoder(CSolver *_solver) :
 	cnf(createCNF()),
@@ -73,11 +74,14 @@ Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) {
 	}
 	Polarity p = constraint->polarity;
 	uint pSize = constraint->parents.getSize();
-	if ((pSize > 1 && p != P_BOTHTRUEFALSE ) || pSize > 2) {
+	if (solver->getTuner()->getTunable(PROXYVARIABLE, &offon) == 1) {
+//	if ((pSize > 1 && p != P_BOTHTRUEFALSE ) || pSize > 2) {
 		Edge e = getNewVarSATEncoder();
 		generateProxy(cnf, result, e, p);
 		booledgeMap.put(constraint, e.node_ptr);
 		result = e;
+	} else{
+		booledgeMap.put(constraint, result.node_ptr);
 	}
 
 	return c.isNegated() ? constraintNegate(result) : result;
diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc
index 3510d11..0c9067a 100644
--- a/src/Backend/satfunctableencoder.cc
+++ b/src/Backend/satfunctableencoder.cc
@@ -9,6 +9,8 @@
 #include "set.h"
 #include "element.h"
 #include "common.h"
+#include "tunable.h"
+#include "csolver.h"
 
 Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *constraint) {
 	ASSERT(constraint->predicate->type == TABLEPRED);
@@ -47,14 +49,18 @@ Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *con
 			row = constraintAND(cnf, inputNum, carray);
 			break;
 		case SATC_FLAGFORCEUNDEFINED: {
-			Edge proxy = constraintNewVar(cnf);
-			generateProxy(cnf, constraintAND(cnf, inputNum, carray), proxy, P_BOTHTRUEFALSE);
-			Edge undefConst = encodeConstraintSATEncoder(constraint->undefStatus);
-			addConstraintCNF(cnf, constraintIMPLIES(cnf, proxy,  constraintNegate(undefConst)));
-			if (generateNegation == (entry->output != 0)) {
-				continue;
+			if(solver->getTuner()->getTunable(PROXYVARIABLE, &offon) == 1){
+				Edge proxy = constraintNewVar(cnf);
+				generateProxy(cnf, constraintAND(cnf, inputNum, carray), proxy, P_BOTHTRUEFALSE);
+				Edge undefConst = encodeConstraintSATEncoder(constraint->undefStatus);
+				addConstraintCNF(cnf, constraintIMPLIES(cnf, proxy,  constraintNegate(undefConst)));
+				if (generateNegation == (entry->output != 0)) {
+					continue;
+				}
+				row = proxy;
+			}else {
+				row = constraintAND(cnf, inputNum, carray);
 			}
-			row = proxy;
 			break;
 		}
 		default:
diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h
index 2e526d3..7e81340 100644
--- a/src/Tuner/tunable.h
+++ b/src/Tuner/tunable.h
@@ -39,7 +39,7 @@ public:
 static TunableDesc onoff(0, 1, 1);
 static TunableDesc offon(0, 1, 0);
 
-enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT, ELEMENTOPTSETS};
+enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT, ELEMENTOPTSETS, PROXYVARIABLE};
 typedef enum Tunables Tunables;
 
 const char* tunableParameterToString(Tunables tunable);
-- 
2.34.1