checking the the variable isn't constant in generating proxy variables + making its...
authorHamed Gorjiara <hgorjiar@uci.edu>
Fri, 27 Jul 2018 02:48:54 +0000 (19:48 -0700)
committerHamed Gorjiara <hgorjiar@uci.edu>
Fri, 27 Jul 2018 02:48:54 +0000 (19:48 -0700)
src/Backend/satencoder.cc
src/Backend/satfunctableencoder.cc
src/Tuner/tunable.h

index dde77c1..52cc8dc 100644 (file)
@@ -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);
index 0c9067a..9e6087e 100644 (file)
@@ -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;
                }
index 7e81340..94646b7 100644 (file)
@@ -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;