From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Sun, 21 Oct 2018 00:53:05 +0000 (-0700)
Subject: Fixing the anyvalue heuristic for binaryIndex
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=5bddd9119cc04c910a2cc47b69d3606a90bad3b3

Fixing the anyvalue heuristic for binaryIndex
---

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index 2f93d21..3cd2c1c 100644
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -7,6 +7,7 @@
 #include "predicate.h"
 #include "csolver.h"
 #include "tunable.h"
+#include <cmath>
 
 void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool &memo) {
 	uint numParents = elem->parents.getSize();
@@ -226,7 +227,8 @@ void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
 	if (encoding->element->anyValue) {
 		uint setSize = encoding->element->getRange()->getSize();
 		uint encArraySize = encoding->encArraySize;
-		if (setSize < encArraySize * (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex) / 10) {
+		double metric = encArraySize == setSize?setSize:setSize/(encArraySize-setSize);
+		if ( log(metric) <  pow(1.9, (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex) - 4)) {
 			generateAnyValueBinaryIndexEncodingPositive(encoding);
 		} else {
 			generateAnyValueBinaryIndexEncoding(encoding);
diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h
index a7ab4e9..22660fb 100644
--- a/src/Tuner/tunable.h
+++ b/src/Tuner/tunable.h
@@ -39,9 +39,9 @@ public:
 static TunableDesc onoff(0, 1, 1);
 static TunableDesc offon(0, 1, 0);
 static TunableDesc proxyparameter(1, 5, 2);
-static TunableDesc mustValueBinaryIndex(5, 9, 8);
+static TunableDesc mustValueBinaryIndex(0, 6, 3);
 static TunableDesc NodeEncodingDesc(ELEM_UNASSIGNED, BINARYINDEX, ELEM_UNASSIGNED);
-static TunableDesc NaiveEncodingDesc(ONEHOT, BINARYINDEX, ONEHOT);
+static TunableDesc NaiveEncodingDesc(ONEHOT, BINARYINDEX, BINARYINDEX);
 static TunableDesc boolVarOrderingDesc(CONSTRAINTORDERING, REVERSEORDERING, REVERSEORDERING);
 
 enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT,