From 555df540fc4fce65ef773ff1f9515ce3dd6800c4 Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Thu, 26 Jul 2018 19:48:54 -0700 Subject: [PATCH] checking the the variable isn't constant in generating proxy variables + making its tuner more fine-grained --- src/Backend/satencoder.cc | 4 ++-- src/Backend/satfunctableencoder.cc | 8 ++++---- src/Tuner/tunable.h | 1 + 3 files changed, 7 insertions(+), 6 deletions(-) diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc index dde77c1..52cc8dc 100644 --- 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 0c9067a..9e6087e 100644 --- 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 7e81340..94646b7 100644 --- 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; -- 2.34.1