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

cnfcomp parameters

parent 2c4ec6c7
......@@ -38,8 +38,16 @@ enum class COMPARE_KIND
Last = ABSORBED
};
const std::array<std::string, static_cast<size_t>(COMPARE_KIND::Last) + 1>
compare_kind_names = {"implicate", "one_provable", "absorbed"};
const SUBool::EnumAnnotation<COMPARE_KIND> kCompareKindAnnotation(
"COMPARE_KIND",
{{COMPARE_KIND::IMPLICATE, "implicate",
"check if the clauses of one CNF are implicates of the "
"other (semantical comparison)"},
{COMPARE_KIND::ONE_PROVABLE, "one_provable",
"check if the clauses of one CNF are 1-provable in the other"},
{COMPARE_KIND::ABSORBED, "absorbed",
"check if the clauses in one CNF are absorbed by the other (not "
"empowering)"}});
struct config_t
{
......@@ -58,8 +66,8 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level) << "\tfile_right: " << conf.file_right << std::endl;
SUBool::logs.TLog(level) << "\tverbosity: " << conf.verbosity << std::endl;
kRelationAnnotation.DumpValue("\t", level, "relation", conf.relation);
SUBool::dump_enum_value(
"\t", level, "compare_kind", conf.compare_kind, compare_kind_names);
kCompareKindAnnotation.DumpValue(
"\t", level, "compare_kind", conf.compare_kind);
}
std::optional<config_t>
......@@ -69,7 +77,9 @@ parse_arguments(int argc, char *argv[])
std::string relation;
std::string compare_kind;
auto opt_relation = SUBool::make_enum_option(
kRelationAnnotation, "relation,r", "Relation to check", conf.relation);
kRelationAnnotation, "relation,r", "Relation to check.", conf.relation);
auto opt_compare_kind = SUBool::make_enum_option(kCompareKindAnnotation,
"compare-kind,k", "How the CNFs should be compared.", conf.compare_kind);
try
{
......@@ -79,17 +89,7 @@ parse_arguments(int argc, char *argv[])
{&conf.file_left, "input-left"}, {&conf.file_right, "input-right"});
po::options_description desc("Configuration options");
desc.add(opt_relation);
desc.add_options()("compare-kind,k",
po::value<std::string>(&compare_kind)
->default_value(compare_kind_names.at(
static_cast<size_t>(conf.compare_kind))),
"How the CNFs should be compared. Possible values:\n"
"implicate = check if the clauses of one CNF are implicates of the "
"other (semantical comparison),\n"
"one_provable = check if the clauses of one CNF are 1-provable in "
"the other,\n"
"absorbed = check if the clauses in one CNF are absorbed by the "
"other (not empowering).");
desc.add(opt_compare_kind);
opts.Add(desc);
if (!opts.Parse(argc, argv))
{
......@@ -104,8 +104,7 @@ parse_arguments(int argc, char *argv[])
try
{
conf.relation = opt_relation.Value();
conf.compare_kind =
SUBool::enum_of_name<COMPARE_KIND>(compare_kind, compare_kind_names);
conf.compare_kind = opt_compare_kind.Value();
}
catch (SUBool::BadParameterException &e)
{
......
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