Now the Tuner decides about creating proxy variables
authorHamed Gorjiara <hgorjiar@uci.edu>
Fri, 27 Jul 2018 02:01:48 +0000 (19:01 -0700)
committerHamed Gorjiara <hgorjiar@uci.edu>
Fri, 27 Jul 2018 02:01:48 +0000 (19:01 -0700)
src/Backend/satencoder.cc
src/Backend/satfunctableencoder.cc
src/Tuner/tunable.h

index 8dab3ab..dde77c1 100644 (file)
@@ -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;
index 3510d11..0c9067a 100644 (file)
@@ -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:
index 2e526d3..7e81340 100644 (file)
@@ -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);