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

Small fixes in dpelim options

parent d59a1ebe
......@@ -30,7 +30,6 @@ struct config_t
{
std::string input_file{};
std::string output_file{};
unsigned verbosity{3}; // 0 means no output
unsigned max_input_var{0};
bool elim_minimize{false};
bool final_minimize{false};
......@@ -56,7 +55,7 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level) << "Configuration:" << std::endl;
SUBool::logs.DumpValue("\t", level, "input_file", conf.input_file);
SUBool::logs.DumpValue("\t", level, "output_file", conf.output_file);
SUBool::logs.DumpValue("\t", level, "verbosity", conf.verbosity);
SUBool::logs.DumpValue("\t", level, "verbosity", SUBool::logs.mVerbLevel);
SUBool::logs.DumpValue("\t", level, "max_input_var", conf.max_input_var);
SUBool::logs.DumpValue("\t", level, "elim_minimize", conf.elim_minimize);
SUBool::CNFEncoding::kBlockPrimeAnnotation.DumpValue(
......@@ -311,6 +310,7 @@ main(int argc, char *argv[])
std::signal(SIGQUIT, term_func);
std::signal(SIGINT, term_func);
dump_config(*conf, 3);
#if 0
auto cnf = SUBool::input_or_die<SUBool::CNF>(conf->input_file, SUBool::logs);
SUBool::PCEncoding enc(cnf, conf->max_input_var, false);
eliminate(enc, *conf);
......@@ -319,5 +319,6 @@ main(int argc, char *argv[])
enc.Minimize();
}
SUBool::output(conf->output_file, enc);
#endif
return 0;
}
......@@ -76,7 +76,7 @@ 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.",
"increase-policy,C", "How the size bound should be checked.",
kDefaultIncreasePolicy),
mOptionsDesc("Elimination options")
{
......@@ -85,12 +85,12 @@ SUBool::DPElimEliminationOptions::DPElimEliminationOptions()
("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",
("max-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",
("factor,f",
po::value<long double>(&mFactor)->default_value(
kDefaultFactor, kDefaultFactorString),
"Stop the elimination when the number of clauses increases by the "
......
Markdown is supported
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