Commit d59a1ebe authored by Kučera Petr RNDr. Ph.D.'s avatar Kučera Petr RNDr. Ph.D.
Browse files

dpelim program options

parent 2447decf
...@@ -19,12 +19,12 @@ const std::string SUBool::kPrgName = "dpelim"; ...@@ -19,12 +19,12 @@ const std::string SUBool::kPrgName = "dpelim";
const std::string SUBool::kPrgDesc = "DP elimination of variables"; const std::string SUBool::kPrgDesc = "DP elimination of variables";
const std::string prg_help = const std::string prg_help =
"DP elimination of variables. By default it aims to eliminate all " "DP elimination of variables. By default it aims to eliminate all "
"variables, use -f, -s options to limit the extent of elimination. You can " "variables, use -e, -f, and -s options to limit the extent of elimination. "
"also limit the maximum input variables (up to which no variable should be " "You can also limit the maximum input variables (up to which no variable "
"eliminated). Note that the input is considered to be an encoding. Thus " "should be eliminated) with -x option. Note that the input is considered "
"the variables which are allowed to be eliminated may have different " "to be an encoding. Thus the variables which are allowed to be eliminated "
"indices in the output (they are considered auxiliary in that their names " "may have different indices in the output (they are considered auxiliary "
"do not matter)."; "in that their names do not matter).";
struct config_t struct config_t
{ {
...@@ -36,7 +36,8 @@ struct config_t ...@@ -36,7 +36,8 @@ struct config_t
bool final_minimize{false}; bool final_minimize{false};
SUBool::CNFEncoding::BLOCK_PRIME block_prime{ SUBool::CNFEncoding::BLOCK_PRIME block_prime{
SUBool::CNFEncoding::BLOCK_PRIME::NONE}; SUBool::CNFEncoding::BLOCK_PRIME::NONE};
SUBool::ELIMINATE_POLICY eliminate{SUBool::ELIMINATE_POLICY::ALL}; SUBool::DPElimEliminationOptions::ELIMINATE_POLICY eliminate{
SUBool::DPElimEliminationOptions::kDefaultEliminatePolicy};
SUBool::DPEliminator::IGNORE_POLICY ignore_policy{ SUBool::DPEliminator::IGNORE_POLICY ignore_policy{
SUBool::DPEliminator::IGNORE_POLICY::ABSORBED}; SUBool::DPEliminator::IGNORE_POLICY::ABSORBED};
SUBool::DPEliminator::INPROCESSING inprocessing{ SUBool::DPEliminator::INPROCESSING inprocessing{
...@@ -60,7 +61,7 @@ dump_config(const config_t &conf, unsigned level) ...@@ -60,7 +61,7 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.DumpValue("\t", level, "elim_minimize", conf.elim_minimize); SUBool::logs.DumpValue("\t", level, "elim_minimize", conf.elim_minimize);
SUBool::CNFEncoding::kBlockPrimeAnnotation.DumpValue( SUBool::CNFEncoding::kBlockPrimeAnnotation.DumpValue(
"\t", level, "block_prime", conf.block_prime); "\t", level, "block_prime", conf.block_prime);
SUBool::kEliminatePolicyAnnotation.DumpValue( SUBool::DPElimEliminationOptions::kEliminatePolicyAnnotation.DumpValue(
"\t", level, "eliminate", conf.eliminate); "\t", level, "eliminate", conf.eliminate);
SUBool::DPEliminator::kIgnorePolicyAnnotation.DumpValue( SUBool::DPEliminator::kIgnorePolicyAnnotation.DumpValue(
"\t", level, "ignore_policy", conf.ignore_policy); "\t", level, "ignore_policy", conf.ignore_policy);
...@@ -85,15 +86,31 @@ parse_arguments(int argc, char *argv[]) ...@@ -85,15 +86,31 @@ parse_arguments(int argc, char *argv[])
SUBool::PrgOptions opts(true); SUBool::PrgOptions opts(true);
opts.InputOutput(&conf.input_file, &conf.output_file); opts.InputOutput(&conf.input_file, &conf.output_file);
opts.SetHelpDesc(prg_help);
SUBool::DPElimEliminationOptions elim_opts;
SUBool::DPElimClauseManipOptions clause_manip_opts;
SUBool::DPElimMinimizeOptions minimize_opts; SUBool::DPElimMinimizeOptions minimize_opts;
opts.Add(elim_opts.Desc());
opts.Add(clause_manip_opts.Desc());
opts.Add(minimize_opts.Desc()); opts.Add(minimize_opts.Desc());
if (!opts.Parse(argc, argv) || !minimize_opts.GetValues()) if (!opts.Parse(argc, argv) || !elim_opts.GetValues()
|| !clause_manip_opts.GetValues() || !minimize_opts.GetValues())
{ {
return {}; return {};
} }
conf.max_input_var = elim_opts.MaxInputVar();
conf.eliminate = elim_opts.EliminatePolicy();
conf.increase_policy = elim_opts.IncreasePolicy();
conf.max_increase = elim_opts.MaxIncrease();
conf.factor = elim_opts.Factor();
conf.block_prime = clause_manip_opts.BlockPrime();
conf.inprocessing = clause_manip_opts.Inprocessing();
conf.ignore_policy = clause_manip_opts.IgnorePolicy();
conf.elim_minimize = minimize_opts.ElimMinimize(); conf.elim_minimize = minimize_opts.ElimMinimize();
conf.final_minimize = minimize_opts.FinalMinimize(); conf.final_minimize = minimize_opts.FinalMinimize();
conf.minimize_size_step = minimize_opts.SizeStep(); conf.minimize_size_step = minimize_opts.SizeStep();
...@@ -237,7 +254,7 @@ eliminate(SUBool::CNFEncoding &enc, const config_t &conf) ...@@ -237,7 +254,7 @@ eliminate(SUBool::CNFEncoding &enc, const config_t &conf)
conf.increase_policy, conf.block_prime); conf.increase_policy, conf.block_prime);
switch (conf.eliminate) switch (conf.eliminate)
{ {
case SUBool::ELIMINATE_POLICY::ALL: case SUBool::DPElimEliminationOptions::ELIMINATE_POLICY::ALL:
if (conf.elim_minimize) if (conf.elim_minimize)
{ {
enc.EliminateAuxVariablesWithMaxIncMinimize( enc.EliminateAuxVariablesWithMaxIncMinimize(
...@@ -250,7 +267,7 @@ eliminate(SUBool::CNFEncoding &enc, const config_t &conf) ...@@ -250,7 +267,7 @@ eliminate(SUBool::CNFEncoding &enc, const config_t &conf)
SUBool::CNFEncoding::kEliminateAll); SUBool::CNFEncoding::kEliminateAll);
} }
break; break;
case SUBool::ELIMINATE_POLICY::MAX_INCREASE: case SUBool::DPElimEliminationOptions::ELIMINATE_POLICY::MAX_INCREASE:
if (conf.elim_minimize) if (conf.elim_minimize)
{ {
enc.EliminateAuxVariablesWithMaxIncMinimize(conf.max_increase, enc.EliminateAuxVariablesWithMaxIncMinimize(conf.max_increase,
...@@ -261,7 +278,7 @@ eliminate(SUBool::CNFEncoding &enc, const config_t &conf) ...@@ -261,7 +278,7 @@ eliminate(SUBool::CNFEncoding &enc, const config_t &conf)
enc.EliminateAuxVariablesWithMaxInc(conf.max_increase); enc.EliminateAuxVariablesWithMaxInc(conf.max_increase);
} }
break; break;
case SUBool::ELIMINATE_POLICY::FACTOR: case SUBool::DPElimEliminationOptions::ELIMINATE_POLICY::FACTOR:
if (conf.elim_minimize) if (conf.elim_minimize)
{ {
enc.EliminateAuxVariablesWithFactorMinimize( enc.EliminateAuxVariablesWithFactorMinimize(
......
...@@ -8,8 +8,8 @@ ...@@ -8,8 +8,8 @@
#include "dpelim_opt.h" #include "dpelim_opt.h"
const SUBool::EnumAnnotation<SUBool::ELIMINATE_POLICY> const SUBool::EnumAnnotation<SUBool::DPElimEliminationOptions::ELIMINATE_POLICY>
SUBool::kEliminatePolicyAnnotation("ELIMINATE", SUBool::DPElimEliminationOptions::kEliminatePolicyAnnotation("ELIMINATE",
{// {//
{ELIMINATE_POLICY::ALL, "all", {ELIMINATE_POLICY::ALL, "all",
"Eliminate all auxiliary variables."}, "Eliminate all auxiliary variables."},
...@@ -42,3 +42,65 @@ SUBool::DPElimMinimizeOptions::GetValues() ...@@ -42,3 +42,65 @@ SUBool::DPElimMinimizeOptions::GetValues()
{ {
return true; return true;
} }
SUBool::DPElimClauseManipOptions::DPElimClauseManipOptions()
: mBlockPrimeOption(CNFEncoding::kBlockPrimeAnnotation, "block-prime,P",
"Make new clauses prime after each block of DP "
"elimination.",
kDefaultBlockPrime),
mInprocessingOption(DPEliminator::kInprocessingAnnotation, "process,p",
"how to inprocess the resolvent during auxiliary variable "
"elimination.",
kDefaultInprocessing),
mIgnorePolicyOption(DPEliminator::kIgnorePolicyAnnotation,
"ignore-policy,g",
"Which resolvents should be discarded during auxiliary variable "
"elimination.",
kDefaultIgnorePolicy),
mOptionsDesc("Clause manipulation")
{
mOptionsDesc.add(mBlockPrimeOption);
mOptionsDesc.add(mInprocessingOption);
mOptionsDesc.add(mIgnorePolicyOption);
}
bool
SUBool::DPElimClauseManipOptions::GetValues()
{
return mBlockPrimeOption.GetValue(mBlockPrime)
&& mInprocessingOption.GetValue(mInprocessing)
&& mIgnorePolicyOption.GetValue(mIgnorePolicy);
}
SUBool::DPElimEliminationOptions::DPElimEliminationOptions()
: mEliminatePolicyOption(kEliminatePolicyAnnotation, "eliminate,e",
"When to stop elimination", kDefaultEliminatePolicy),
mIncreasePolicyOption(DPEliminator::kIncreasePolicyAnnotation,
"increase-policy,c", "How the size bound should be checked.",
kDefaultIncreasePolicy),
mOptionsDesc("Elimination options")
{
mOptionsDesc.add(mEliminatePolicyOption);
mOptionsDesc.add_options() //
("max-input-var,x", po::value<unsigned>(&mMaxInputVar)->default_value(0),
"Maximum input variable. All variables with higher index are "
"considered auxiliary and possibly eliminated.") //
("size-increase,s",
po::value<unsigned>(&mMaxIncrease)
->default_value(kDefaultMaxIncrease),
"Stop the elimination after the number of clauses increases by the "
"given amount") //
("eliminate-factor,f",
po::value<long double>(&mFactor)->default_value(
kDefaultFactor, kDefaultFactorString),
"Stop the elimination when the number of clauses increases by the "
"given factor");
mOptionsDesc.add(mIncreasePolicyOption);
}
bool
SUBool::DPElimEliminationOptions::GetValues()
{
return mEliminatePolicyOption.GetValue(mEliminatePolicy)
&& mIncreasePolicyOption.GetValue(mIncreasePolicy);
}
...@@ -20,16 +20,7 @@ namespace po = boost::program_options; ...@@ -20,16 +20,7 @@ namespace po = boost::program_options;
namespace SUBool namespace SUBool
{ {
enum class ELIMINATE_POLICY #if 0
{
ALL,
MAX_INCREASE,
FACTOR,
Last = FACTOR
};
extern const EnumAnnotation<ELIMINATE_POLICY> kEliminatePolicyAnnotation;
struct elim_config_t struct elim_config_t
{ {
unsigned max_input_var{0}; unsigned max_input_var{0};
...@@ -52,6 +43,7 @@ namespace SUBool ...@@ -52,6 +43,7 @@ namespace SUBool
// unsigned minimize_size_step{5000}; // unsigned minimize_size_step{5000};
// double minimize_size_factor{0.6}; // double minimize_size_factor{0.6};
}; };
#endif
class DPElimMinimizeOptions class DPElimMinimizeOptions
{ {
...@@ -83,6 +75,86 @@ namespace SUBool ...@@ -83,6 +75,86 @@ namespace SUBool
double SizeFactor() const; double SizeFactor() const;
}; };
class DPElimClauseManipOptions
{
public:
static const CNFEncoding::BLOCK_PRIME kDefaultBlockPrime =
CNFEncoding::BLOCK_PRIME::NONE;
static const DPEliminator::INPROCESSING kDefaultInprocessing =
DPEliminator::INPROCESSING::NONE;
static const DPEliminator::IGNORE_POLICY kDefaultIgnorePolicy =
DPEliminator::IGNORE_POLICY::ABSORBED;
private:
EnumOption<CNFEncoding::BLOCK_PRIME> mBlockPrimeOption;
EnumOption<DPEliminator::INPROCESSING> mInprocessingOption;
EnumOption<DPEliminator::IGNORE_POLICY> mIgnorePolicyOption;
CNFEncoding::BLOCK_PRIME mBlockPrime{kDefaultBlockPrime};
DPEliminator::INPROCESSING mInprocessing{kDefaultInprocessing};
DPEliminator::IGNORE_POLICY mIgnorePolicy{kDefaultIgnorePolicy};
po::options_description mOptionsDesc;
public:
DPElimClauseManipOptions();
bool GetValues();
const po::options_description &Desc() const;
CNFEncoding::BLOCK_PRIME BlockPrime() const;
DPEliminator::INPROCESSING Inprocessing() const;
DPEliminator::IGNORE_POLICY IgnorePolicy() const;
};
class DPElimEliminationOptions
{
public:
enum class ELIMINATE_POLICY
{
ALL,
MAX_INCREASE,
FACTOR,
Last = FACTOR
};
static const EnumAnnotation<ELIMINATE_POLICY> kEliminatePolicyAnnotation;
static const ELIMINATE_POLICY kDefaultEliminatePolicy =
ELIMINATE_POLICY::ALL;
static const DPEliminator::INCREASE_POLICY kDefaultIncreasePolicy =
DPEliminator::INCREASE_POLICY::AFTER_BOUND;
static constexpr unsigned kDefaultMaxIncrease = 1;
static constexpr long double kDefaultFactor = 1.2l;
inline static const std::string kDefaultFactorString{"1.2"};
private:
EnumOption<ELIMINATE_POLICY> mEliminatePolicyOption;
EnumOption<DPEliminator::INCREASE_POLICY> mIncreasePolicyOption;
unsigned mMaxInputVar{0};
ELIMINATE_POLICY mEliminatePolicy{kDefaultEliminatePolicy};
DPEliminator::INCREASE_POLICY mIncreasePolicy{kDefaultIncreasePolicy};
unsigned mMaxIncrease{kDefaultMaxIncrease};
long double mFactor{kDefaultFactor};
po::options_description mOptionsDesc;
public:
DPElimEliminationOptions();
bool GetValues();
const po::options_description &Desc() const;
ELIMINATE_POLICY EliminatePolicy() const;
DPEliminator::INCREASE_POLICY IncreasePolicy() const;
unsigned MaxIncrease() const;
long double Factor() const;
unsigned MaxInputVar() const;
};
} // namespace SUBool } // namespace SUBool
inline SUBool::DPElimMinimizeOptions::DPElimMinimizeOptions() inline SUBool::DPElimMinimizeOptions::DPElimMinimizeOptions()
...@@ -121,4 +193,63 @@ SUBool::DPElimMinimizeOptions::SizeFactor() const ...@@ -121,4 +193,63 @@ SUBool::DPElimMinimizeOptions::SizeFactor() const
return mSizeFactor; return mSizeFactor;
} }
inline const po::options_description &
SUBool::DPElimClauseManipOptions::Desc() const
{
return mOptionsDesc;
}
inline SUBool::CNFEncoding::BLOCK_PRIME
SUBool::DPElimClauseManipOptions::BlockPrime() const
{
return mBlockPrime;
}
inline SUBool::DPEliminator::INPROCESSING
SUBool::DPElimClauseManipOptions::Inprocessing() const
{
return mInprocessing;
}
inline SUBool::DPEliminator::IGNORE_POLICY
SUBool::DPElimClauseManipOptions::IgnorePolicy() const
{
return mIgnorePolicy;
}
inline const po::options_description &
SUBool::DPElimEliminationOptions::Desc() const
{
return mOptionsDesc;
}
inline SUBool::DPElimEliminationOptions::ELIMINATE_POLICY
SUBool::DPElimEliminationOptions::EliminatePolicy() const
{
return mEliminatePolicy;
}
inline SUBool::DPEliminator::INCREASE_POLICY
SUBool::DPElimEliminationOptions::IncreasePolicy() const
{
return mIncreasePolicy;
}
inline unsigned
SUBool::DPElimEliminationOptions::MaxIncrease() const
{
return mMaxIncrease;
}
inline unsigned
SUBool::DPElimEliminationOptions::MaxInputVar() const
{
return mMaxInputVar;
}
inline long double
SUBool::DPElimEliminationOptions::Factor() const
{
return mFactor;
}
#endif #endif
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment