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

[satune.git] / src / Backend / satencoder.cc

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);