Now the Tuner decides about creating proxy variables

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index 8dab3ab9d089936eb0ae7a8c5ff1accfe78c000e..dde77c14e4b938118dcfc855a54a1915a2504f57 100644 (file)
--- 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 3510d118175d5fa5494381e7ee6b2c64c68cd155..0c9067ad98cfa2d7877789995d57b0ec31bbc2ba 100644 (file)
--- 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 2e526d376380a24fad6c994153b5dc9108c68cfc..7e81340b5d43d9227729ca13625656c86c885962 100644 (file)
--- 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);