checking the the variable isn't constant in generating proxy variables + making its...

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index dde77c14e4b938118dcfc855a54a1915a2504f57..52cc8dc82edd279501a60fcd6bfd573a75e50be0 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -74,8 +74,8 @@ Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) {
        }
        Polarity p = constraint->polarity;
        uint pSize = constraint->parents.getSize();
-       if (solver->getTuner()->getTunable(PROXYVARIABLE, &offon) == 1) {
-//     if ((pSize > 1 && p != P_BOTHTRUEFALSE ) || pSize > 2) {
+
+       if ( !edgeIsVarConst(result) && pSize > (uint)solver->getTuner()->getTunable(PROXYVARIABLE, &proxyparameter) ) {
                Edge e = getNewVarSATEncoder();
                generateProxy(cnf, result, e, p);
                booledgeMap.put(constraint, e.node_ptr);

diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc
index 0c9067ad98cfa2d7877789995d57b0ec31bbc2ba..9e6087ec3db4b492b9ebaa52bdf40f964cd54b50 100644 (file)
--- a/src/Backend/satfunctableencoder.cc
+++ b/src/Backend/satfunctableencoder.cc
@@ -49,17 +49,17 @@ Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *con
                        row = constraintAND(cnf, inputNum, carray);
                        break;
                case SATC_FLAGFORCEUNDEFINED: {
-                       if(solver->getTuner()->getTunable(PROXYVARIABLE, &offon) == 1){
+                       row = constraintAND(cnf, inputNum, carray);
+                       uint pSize = constraint->parents.getSize();
+                       if(!edgeIsVarConst(row) && pSize > (uint)solver->getTuner()->getTunable(PROXYVARIABLE, &proxyparameter)){
                                Edge proxy = constraintNewVar(cnf);
-                               generateProxy(cnf, constraintAND(cnf, inputNum, carray), proxy, P_BOTHTRUEFALSE);
+                               generateProxy(cnf, row, 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);
                        }
                        break;
                }

diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h
index 7e81340b5d43d9227729ca13625656c86c885962..94646b79bed7d9defd79b3cd8e4d0f5c84751b7b 100644 (file)
--- a/src/Tuner/tunable.h
+++ b/src/Tuner/tunable.h
@@ -38,6 +38,7 @@ public:
 
 static TunableDesc onoff(0, 1, 1);
 static TunableDesc offon(0, 1, 0);
+static TunableDesc proxyparameter(1, 20, 2);
 
 enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT, ELEMENTOPTSETS, PROXYVARIABLE};
 typedef enum Tunables Tunables;