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

cnfprime using PrgOptions

parent 84c0c5e5
......@@ -6,11 +6,12 @@
* Program for constructing a prime CNF for a given CNF.
*/
#include <cxxopts.hpp>
#include <fstream>
#include <iostream>
#include <string>
#include <boost/optional.hpp>
#include "cnfutil.h"
#include "cpuutil.h"
#include "empower.h"
......@@ -29,60 +30,24 @@ struct config_t
std::string input_file{};
std::string output_file{};
bool unitprop{false};
unsigned verbosity{3};
};
config_t
std::optional<config_t>
parse_arguments(int argc, char *argv[])
{
config_t conf;
try
{
cxxopts::Options options(SUBool::kPrgName, SUBool::kPrgDesc);
options.positional_help("[input [output]]");
options.add_options()("h,help", "Print help")(
"v,version", "Print version info")("i,input",
"Input file with a CNF in DIMACS format",
cxxopts::value<std::string>(conf.input_file))("o,output",
"Output file with the encoding CNF in DIMACS format",
cxxopts::value<std::string>(conf.output_file))("u,unitprop",
"Use only unit propagation instead of SAT. It means "
"that the result is not necessarily prime, but it is prime with "
"respect to 1-provability",
cxxopts::value<bool>(conf.unitprop)
->default_value("false"))("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))("positional",
"Positional arguments: these are the arguments that are entered "
"without an option",
cxxopts::value<std::vector<std::string>>());
options.parse_positional({"input", "output", "positional"});
auto result = options.parse(argc, argv);
if (result.count("help"))
{
std::cout << options.help() << std::endl;
exit(1);
}
if (result.count("version"))
{
SUBool::print_version(std::cout);
exit(1);
}
if (result.count("positional"))
{
std::cerr << "Multiple files passed as parameters, "
<< "only input and output files are allowed" << std::endl
<< options.help() << std::endl;
exit(1);
}
SUBool::logs.mVerbLevel = conf.verbosity;
}
catch (const cxxopts::OptionException &e)
SUBool::PrgOptions opts;
opts.InputOutput(&conf.input_file, &conf.output_file);
po::options_description desc("Configuration options");
desc.add_options()("unitprop,u", po::bool_switch(&conf.unitprop),
"Use only unit propagation instead of SAT. It means "
"that the result is not necessarily prime, but it is prime with "
"respect to 1-provability (although not fully as only one round of "
"prime subimplicate finding is performed");
opts.Add(desc);
if (!opts.Parse(argc, argv))
{
throw SUBool::ParseException("parse_arguments", e.what());
return {};
}
return conf;
}
......@@ -95,7 +60,8 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level)
<< "\toutput_file: " << conf.output_file << std::endl;
SUBool::logs.TLog(level) << "\tunitprop: " << conf.unitprop << std::endl;
SUBool::logs.TLog(level) << "\tverbosity: " << conf.verbosity << std::endl;
SUBool::logs.TLog(level)
<< "\tverbosity: " << SUBool::logs.mVerbLevel << std::endl;
}
SUBool::CNF
......@@ -114,19 +80,23 @@ process(const config_t &conf, SUBool::CNF input)
int
main(int argc, char *argv[])
{
config_t conf = parse_arguments(argc, argv);
if (conf.unitprop)
auto conf = parse_arguments(argc, argv);
if (!conf)
{
return 1;
}
if (conf->unitprop)
{
SUBool::logs.TLog(1) << "Using only unit propagation" << std::endl;
}
SUBool::logs.TLog(2) << "Reading input" << std::endl;
auto in_cnf = SUBool::input<SUBool::CNF>(conf.input_file);
auto in_cnf = SUBool::input<SUBool::CNF>(conf->input_file);
SUBool::logs.TLog(1) << "Starting computation" << std::endl;
SUBool::CPUTime cpu_time;
auto out_cnf = process(conf, in_cnf);
auto out_cnf = process(*conf, in_cnf);
SUBool::logs.TLog(1) << "Computation finished, proc time: " << cpu_time
<< std::endl;
SUBool::output(conf.output_file, out_cnf);
SUBool::output(conf->output_file, out_cnf);
SUBool::logs.Log(2) << std::endl;
SUBool::logs.TLog(2) << "Output written" << std::endl;
}
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