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

cnfcomp using PrgOptions

parent 7be28e9d
......@@ -67,7 +67,7 @@ parse_arguments(int argc, char *argv[])
conf.process = SUBool::enum_of_name<PROCESS>(process, process_names);
conf.verbosity = opts.Verbosity();
}
catch (std::exception &e)
catch (const std::exception &e)
{
std::cerr << "Error parsing options: " << e.what() << std::endl;
return {};
......
......@@ -6,8 +6,6 @@
* Program for comparing two functions represented by CNFs.
*/
#include <cxxopts.hpp>
#include "cnfcompare.h"
#include "cnfutil.h"
#include "cpuutil.h"
......@@ -23,9 +21,8 @@ enum class RELATION
Last = GEQ
};
const std::map<std::string, RELATION> relation_names = {{"eq", RELATION::EQUAL},
{"le", RELATION::LEQ}, {"ge", RELATION::GEQ}, {"equal", RELATION::EQUAL},
{"leq", RELATION::LEQ}, {"geq", RELATION::GEQ}};
const std::array<std::string, static_cast<size_t>(RELATION::Last) + 1>
relation_names = {"eq", "le", "ge"};
const std::string SUBool::kPrgName = "cnfcomp";
const std::string SUBool::kPrgDesc =
......@@ -58,97 +55,64 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level) << "\tfile_left: " << conf.file_left << std::endl;
SUBool::logs.TLog(level) << "\tfile_right: " << conf.file_right << std::endl;
SUBool::logs.TLog(level) << "\tverbosity: " << conf.verbosity << std::endl;
SUBool::logs.TLog(level)
<< "\trelation: " << static_cast<unsigned>(conf.relation) << std::endl;
SUBool::dump_enum_value(
"\t", level, "relation", conf.relation, relation_names);
SUBool::dump_enum_value(
"\t", level, "compare_kind", conf.compare_kind, compare_kind_names);
}
RELATION
parse_relation(const std::string &rel)
std::optional<config_t>
parse_arguments(int argc, char *argv[])
{
config_t conf;
std::string relation;
std::string compare_kind;
try
{
return relation_names.at(rel);
// options.positional_help("[input-left [input-right]]");
SUBool::PrgOptions opts;
opts.InputPair(
{&conf.file_left, "input-left"}, {&conf.file_right, "input-right"});
po::options_description desc("Configuration options");
desc.add_options()("relation,r",
po::value<std::string>(&relation)->default_value(
relation_names.at(static_cast<size_t>(conf.relation))),
"Relation to check. eq=equality, le=less than or equal, ge=greater "
"than or equal.")("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).");
opts.Add(desc);
if (!opts.Parse(argc, argv))
{
return {};
}
}
catch (std::out_of_range &e)
catch (const std::exception &e)
{
throw SUBool::BadParameterException(
"relation", "Unknown relation specification");
std::cerr << "Error parsing options: " << e.what() << std::endl;
return {};
}
}
int
parse_arguments(int argc, char *argv[], config_t &conf)
{
try
{
cxxopts::Options options(SUBool::kPrgName, SUBool::kPrgDesc);
options.positional_help("[input-left [input-right]]");
std::string relation;
std::string compare_kind;
options.add_options()("h,help", "Print help")(
"v,version", "Print version info")("b,verbosity",
"Verbosity level of the log which is written to standard output."
" 0 means no log is written, however messages of glucose can still "
"appear.",
cxxopts::value<unsigned>(conf.verbosity)
->default_value(SUBool::LogStream::kMaxLogLevels))("input-left",
"The left hand input file",
cxxopts::value<std::string>(conf.file_left))("input-right",
"The right hand input file",
cxxopts::value<std::string>(conf.file_right))("r,relation",
"Relation to check. eq=equality, le=less than or equal, ge=greater "
"than or equal.",
cxxopts::value<std::string>(relation)->default_value(
"eq"))("k,compare-kind",
"how the CNFs should be compared. Possible values: "
"implicate -- check if the clauses of one CNF are implicates of the "
"other (semantical comparison), "
"one_provable -- check if the clauses of one CNF are 1-provable in "
"the other, "
"absorbed -- check if the clauses in one CNF are absorbed by the "
"other (not empowering).",
cxxopts::value<std::string>(compare_kind)
->default_value("implicate"));
options.parse_positional({"input-left", "input-right", "positional"});
auto result = options.parse(argc, argv);
if (result.count("help"))
{
std::cout << options.help() << std::endl;
return 1;
}
if (result.count("version"))
{
SUBool::print_version(std::cout);
return 1;
}
if (result.count("positional"))
{
SUBool::logs.TLog(0) << "Multiple files passed as parameters, ";
SUBool::logs.TLog(0) << "only two input files allowed" << std::endl;
SUBool::logs.TLog(0) << options.help() << std::endl;
return 1;
}
try
{
conf.relation = parse_relation(relation);
conf.compare_kind = SUBool::enum_of_name<COMPARE_KIND>(
compare_kind, compare_kind_names);
}
catch (SUBool::BadParameterException &e)
{
SUBool::logs.TLog(0)
<< "Error parsing the parameters: " << e.what() << std::endl;
return 1;
}
conf.relation = SUBool::enum_of_name<RELATION>(relation, relation_names);
conf.compare_kind =
SUBool::enum_of_name<COMPARE_KIND>(compare_kind, compare_kind_names);
}
catch (const cxxopts::OptionException &e)
catch (SUBool::BadParameterException &e)
{
std::cerr << "Error parsing options: " << e.what() << std::endl;
return 1;
SUBool::logs.TLog(0) << "Error parsing the parameters: " << e.what()
<< std::endl;
return {};
}
return 0;
return conf;
}
std::string
......@@ -350,20 +314,19 @@ check(config_t &conf, const SUBool::CNF &left_cnf, const SUBool::CNF &right_cnf)
int
main(int argc, char *argv[])
{
config_t conf;
int r = parse_arguments(argc, argv, conf);
if (r != 0)
auto conf = parse_arguments(argc, argv);
if (!conf)
{
return r;
return 1;
}
SUBool::logs.mVerbLevel = conf.verbosity;
dump_config(conf, 0);
SUBool::logs.mVerbLevel = conf->verbosity;
dump_config(*conf, 0);
auto left_cnf =
SUBool::input_or_die<SUBool::CNF>(conf.file_left, SUBool::logs);
SUBool::input_or_die<SUBool::CNF>(conf->file_left, SUBool::logs);
auto right_cnf =
SUBool::input_or_die<SUBool::CNF>(conf.file_right, SUBool::logs);
SUBool::input_or_die<SUBool::CNF>(conf->file_right, SUBool::logs);
SUBool::CPUTime cpu_time;
auto ret = !check(conf, left_cnf, right_cnf);
auto ret = !check(*conf, left_cnf, right_cnf);
SUBool::logs.TLog(2) << "Time " << cpu_time << std::endl;
return ret;
}
......@@ -125,6 +125,19 @@ SUBool::PrgOptions::InputOutput(
"output", po::value<std::string>(&output_file));
mPositional.add("input", 1);
mPositional.add("output", 1);
mPositionalHelp += "[input [output]]";
}
void
SUBool::PrgOptions::InputPair(
const PositFileDesc &first, const PositFileDesc &second)
{
mHidden.add_options()(
first.desc.c_str(), po::value<std::string>(first.fname))(
second.desc.c_str(), po::value<std::string>(second.fname));
mPositional.add(first.desc.c_str(), 1);
mPositional.add(second.desc.c_str(), 1);
mPositionalHelp += "[" + first.desc + " [" + second.desc + "]]";
}
bool
......
......@@ -199,6 +199,14 @@ namespace SUBool
class PrgOptions
{
public:
struct PositFileDesc
{
std::string *fname;
std::string desc;
};
private:
std::string mPrgName{};
std::string mPrgDesc{};
std::string mPrgHelpDesc{};
......@@ -243,6 +251,7 @@ namespace SUBool
void SetPrgDesc(std::string prg_desc);
void SetHelpDesc(std::string prg_help_desc);
void InputOutput(std::string &input_file, std::string &output_file);
void InputPair(const PositFileDesc &first, const PositFileDesc &second);
bool Parse(int argc, char *argv[]);
unsigned Verbosity() const;
......
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