Skip to content

GitLab

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

cnfcanon uses boost::program_options, code cleaning

parent 1aaaf8a6
Hide whitespace changes
Inline Side-by-side
CMakeLists.txt
View file @ 96cc3f8e
......@@ -36,7 +36,7 @@ function(su_add_pthread name)
endfunction(su_add_pthread)
find_package(Boost 1.64.0 REQUIRED)
find_package(Boost 1.64.0 COMPONENTS program_options REQUIRED)
# Glucose related part
if(DEFINED ENV{GLUCOSE_HOME})
......
bin/CMakeLists.txt
View file @ 96cc3f8e
......@@ -23,6 +23,8 @@ su_add_pthread (pcminimize)
su_add_exec(pccheck true true)
su_add_pthread (pccheck )
su_add_exec(cnfcanon true true)
target_link_libraries (cnfcanon ${Boost_LIBRARIES})
su_add_exec(cnfprime true true)
su_add_exec(cnfcomp true true)
......
bin/cnfcanon.cpp
View file @ 96cc3f8e
......@@ -7,11 +7,13 @@
* can use SAT calls to find prime implicates.
*/
#include <cxxopts.hpp>
#include <fstream>
#include <iostream>
#include <string>
#include <boost/optional.hpp>
#include <boost/program_options.hpp>
#include "canon.h"
#include "cnfutil.h"
#include "cpuutil.h"
......@@ -20,6 +22,12 @@
#include "prgutil.h"
#include "sbexception.h"
namespace po = boost::program_options;
const std::string SUBool::kPrgName = "cnfcanon";
const std::string SUBool::kPrgDesc =
"constructs the canonical CNF for a given CNF";
enum class PROCESS
{
NONE,
......@@ -35,42 +43,56 @@ struct config_t
unsigned verbosity{3};
};
int
parse_arguments(int argc, char *argv[], config_t *conf)
boost::optional<config_t>
parse_arguments(int argc, char *argv[])
{
if (conf == nullptr)
{
throw SUBool::NullPointerException("parse_arguments", "conf == nullptr");
}
config_t conf;
try
{
cxxopts::Options options(
"cnfcanon",
"cnfcanon - construct the canonical CNF for a given CNF.");
options.positional_help("[input [output]]");
po::options_description visible("Allowed options");
//"cnfcanon", "cnfcanon - construct the canonical CNF for a given CNF.");
// options.positional_help("[input [output]]");
unsigned process = 0;
options.add_options()("h,help", "Print help")(
"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))(
"p,process",
"Clause inprocessing and preprocessing level. "
"0 = No inprocessing, "
"1 = use SAT.",
cxxopts::value<unsigned>(process)->default_value("1"))(
"b,verbosity",
visible.add_options()("help,h", "Print help")("process,p",
po::value<unsigned>(&process)->default_value(
static_cast<unsigned>(conf.process)),
"Clause inprocessing and preprocessing level.\n"
"0 = No inprocessing,\n"
"1 = use SAT.")("verbosity,b",
po::value<unsigned>(&conf.verbosity)->default_value(conf.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);
"appear.");
po::options_description hidden("Hidden options");
hidden.add_options()("input", po::value<std::string>(&conf.input_file))(
"output", po::value<std::string>(&conf.output_file));
po::options_description desc;
desc.add(visible).add(hidden);
po::positional_options_description p;
p.add("input", 1);
p.add("output", 1);
// po::positional_options_description pos_desc;
// pos_desc.add("input", 1);
// pos_desc.add("output", 1);
//("positional",
//"Positional arguments: these are the arguments that are entered "
//"without an option",
// po::value<std::vector<std::string>>());
po::variables_map vm;
po::store(
po::command_line_parser(argc, argv).options(desc).positional(p).run(),
vm);
po::notify(vm);
if (vm.count("help"))
{
std::cout << visible << std::endl;
return {};
}
#if 0
desc.parse_positional({"input", "output", "positional"});
auto result = desc.parse(argc, argv);
if (result.count("help"))
{
std::cout << options.help() << std::endl;
......@@ -84,13 +106,14 @@ parse_arguments(int argc, char *argv[], config_t *conf)
return 1;
}
conf->process = SUBool::enum_of_int<PROCESS>(process);
#endif
}
catch (const cxxopts::OptionException &e)
catch (std::exception &e)
{
std::cerr << "Error parsing options: " << e.what() << std::endl;
return 1;
return {};
}
return 0;
return conf;
}
void
......@@ -140,8 +163,8 @@ canon_procedure(const config_t &conf, const SUBool::CNF &cnf)
case PROCESS::SAT:
return std::unique_ptr<SUBool::AbsCanon>(new SUBool::CanonSAT(cnf));
}
throw SUBool::BadParameterException("canon_procedure",
"Bad method specification");
throw SUBool::BadParameterException(
"canon_procedure", "Bad method specification");
}
template <class T>
......@@ -172,25 +195,25 @@ output(const config_t &conf, const T &t)
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, 1);
SUBool::logs.mVerbLevel = conf->verbosity;
dump_config(*conf, 1);
#if 0
SUBool::CNF cnf;
int ret = input(conf, &cnf);
int ret = input(*conf, &cnf);
if (ret != 0)
{
return ret;
}
auto canon = canon_procedure(conf, cnf);
auto canon = canon_procedure(*conf, cnf);
SUBool::CPUTime cpu_time;
canon->Compute();
canon->PrintStatistics(2);
output(conf, canon->Cnf());
output(*conf, canon->Cnf());
#endif
return 0;
}
bin/cnfgraphx.cpp
View file @ 96cc3f8e
......@@ -20,8 +20,8 @@ enum class OUTPUT
Last = DOT
};
const std::string prg_name = "cnfgraph";
const std::string prg_desc = "export a CNF as a graph";
const std::string SUBool::kPrgName = "cnfgraph";
const std::string SUBool::kPrgDesc = "export a CNF as a graph";
const std::string incidence_graph_var_color = "red";
const std::string incidence_graph_clause_color = "blue";
......@@ -34,8 +34,7 @@ enum class GRAPH_KIND
Last = DINCIDENCE
};
const std::map<std::string, GRAPH_KIND> graph_kind_names = {
{"primal", GRAPH_KIND::PRIMAL},
{"dual", GRAPH_KIND::DUAL},
{"primal", GRAPH_KIND::PRIMAL}, {"dual", GRAPH_KIND::DUAL},
{"incidence", GRAPH_KIND::INCIDENCE},
{"dincidence", GRAPH_KIND::DINCIDENCE}};
......@@ -74,14 +73,6 @@ dump_config(const config_t &conf, unsigned level)
<< "\tclause_color: " << conf.clause_color << std::endl;
}
void
print_version()
{
std::cout << prg_name << " - " << prg_desc << std::endl;
std::cout << SUBool::author_year_info() << '\n';
std::cout << SUBool::version_info() << std::endl;
}
GRAPH_KIND
parse_graph_kind(const std::string &kind)
{
......@@ -91,8 +82,8 @@ parse_graph_kind(const std::string &kind)
}
catch (std::out_of_range &e)
{
throw SUBool::BadParameterException("parse_graph_kind",
"Unknown graph kind " + kind);
throw SUBool::BadParameterException(
"parse_graph_kind", "Unknown graph kind " + kind);
}
}
......@@ -107,8 +98,8 @@ parse_output_type(const std::string &output_type)
{
return OUTPUT::DOT;
}
throw SUBool::BadParameterException("parse_output_type",
"Unknown output type " + output_type);
throw SUBool::BadParameterException(
"parse_output_type", "Unknown output type " + output_type);
}
int
......@@ -116,47 +107,44 @@ parse_arguments(int argc, char *argv[], config_t &conf)
{
try
{
cxxopts::Options options(prg_name, prg_desc);
cxxopts::Options options(SUBool::kPrgName, SUBool::kPrgDesc);
options.positional_help("[input [output]]");
std::string graph_kind;
std::string output_type;
options.add_options()("h,help", "Print help")("v,version",
"Print version info")(
"b,verbosity",
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))(
"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))(
"t,output-type",
->default_value(SUBool::LogStream::kMaxLogLevels))("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))("t,output-type",
"Type of the output. "
"graphml = GraphML, "
"dot = GraphViz DOT. ",
cxxopts::value<std::string>(output_type)->default_value("graphml"))(
"g,graph-kind",
cxxopts::value<std::string>(output_type)
->default_value("graphml"))("g,graph-kind",
"Kind of the graph to be exported. "
"primal = primal graph, "
"dual = dual graph, "
"incidence = incidence graph."
"dincidence = directed incidence graph.",
cxxopts::value<std::string>(graph_kind)->default_value("primal"))(
"var-prefix",
cxxopts::value<std::string>(graph_kind)
->default_value("primal"))("var-prefix",
"Prefix of a name of a vertex corresponding to a variable.",
cxxopts::value<std::string>(conf.var_prefix)->default_value("x"))(
"clause-prefix",
cxxopts::value<std::string>(conf.var_prefix)
->default_value("x"))("clause-prefix",
"Prefix of a name of a vertex corresponding to a clause.",
cxxopts::value<std::string>(conf.clause_prefix)->default_value("c"))(
"var-color",
cxxopts::value<std::string>(conf.clause_prefix)
->default_value("c"))("var-color",
"Color of a vertex corresponding to a variable. "
"The default depends on the graph kind. In case of primal and "
"dual graph, it is no color, in case of an incidence graph, it is "
+ incidence_graph_var_color + ". Empty string means no color.",
cxxopts::value<std::string>(conf.var_color))(
"clause-color",
cxxopts::value<std::string>(conf.var_color))("clause-color",
"Color of a vertex corresponding to a clause. "
"The default depends on the graph kind. In case of primal and "
"dual graph, it is no color, in case of an incidence graph, it is "
......@@ -171,7 +159,7 @@ parse_arguments(int argc, char *argv[], config_t &conf)
}
if (result.count("version"))
{
print_version();
SUBool::print_version();
return 1;
}
if (result.count("positional"))
......@@ -225,7 +213,7 @@ parse_arguments(int argc, char *argv[], config_t &conf)
template <typename T, typename... Args>
int
write_graph(std::ostream &os, OUTPUT output_type, T &g, const Args &... args)
write_graph(std::ostream &os, OUTPUT output_type, T &g, const Args &...args)
{
switch (output_type)
{
......@@ -236,8 +224,8 @@ write_graph(std::ostream &os, OUTPUT output_type, T &g, const Args &... args)
g.WriteGraphViz(os, args...);
break;
default:
throw SUBool::InvariantFailedException("write_graph",
"Unknown output type");
throw SUBool::InvariantFailedException(
"write_graph", "Unknown output type");
}
return 0;
}
......@@ -257,26 +245,26 @@ do_graph(const config_t &conf, const SUBool::CNF &cnf)
case GRAPH_KIND::PRIMAL:
{
SUBool::PrimalGraph g(cnf);
return write_graph(os, conf.output_type, g, conf.var_prefix,
conf.var_color);
return write_graph(
os, conf.output_type, g, conf.var_prefix, conf.var_color);
}
case GRAPH_KIND::DUAL:
{
SUBool::DualGraph g(cnf);
return write_graph(os, conf.output_type, g, conf.clause_prefix,
conf.clause_color);
return write_graph(
os, conf.output_type, g, conf.clause_prefix, conf.clause_color);
}
case GRAPH_KIND::INCIDENCE:
{
SUBool::IncidenceGraph g(cnf);
return write_graph(os, conf.output_type, g, conf.var_prefix,
conf.var_color, conf.clause_prefix, conf.clause_color);
conf.var_color, conf.clause_prefix, conf.clause_color);
}
case GRAPH_KIND::DINCIDENCE:
{
SUBool::DIncidenceGraph g(cnf);
return write_graph(os, conf.output_type, g, conf.var_prefix,
conf.var_color, conf.clause_prefix, conf.clause_color);
conf.var_color, conf.clause_prefix, conf.clause_color);
}
default:
throw SUBool::InvariantFailedException("do_graph", "Unknown graph kind");
......
bin/pccheck.cpp
View file @ 96cc3f8e
......@@ -628,7 +628,7 @@ main(int argc, char *argv[])
std::signal(SIGINT, terminate);
SUBool::logs.TLog(SUBool::LogStream::LOG_LEVEL::MINLINES)
<< "PCCompile " << SUBool::version_info() << std::endl;
<< "PCCompile " << SUBool::kVersionInfo << std::endl;
dump_config(
conf, static_cast<unsigned>(SUBool::LogStream::LOG_LEVEL::MINLINES));
......
bin/pccompile.cpp
View file @ 96cc3f8e
......@@ -194,8 +194,8 @@ print_version(std::ostream &os, bool comment = false)
<< " Implements an incremental algorithm based on adding "
"empowering implicates\n";
os << c << " and a learning algorithm\n";
os << c << SUBool::author_year_info() << '\n';
os << c << SUBool::version_info();
os << c << SUBool::kAuthorYearInfo << '\n';
os << c << SUBool::kVersionInfo;
}
std::vector<std::string> log_enc_opt_strings = {"amf", "cex", "flm", "cml"};
......@@ -857,7 +857,7 @@ main(int argc, char *argv[])
std::signal(SIGINT, terminate);
SUBool::logs.TLog(SUBool::LogStream::LOG_LEVEL::MINLINES)
<< "PCCompile " << SUBool::version_info() << std::endl;
<< "PCCompile " << SUBool::kVersionInfo << std::endl;
dump_config(
the_conf, static_cast<unsigned>(SUBool::LogStream::LOG_LEVEL::MINLINES));
......
bin/pcminimize.cpp
View file @ 96cc3f8e
......@@ -50,7 +50,7 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level)
<< "\toutput_file: " << conf.output_file << std::endl;
SUBool::dump_enum_value("\t", level, "minimize_method", conf.minimize_method,
SUBool::kMinimizeMethodNames);
SUBool::kMinimizeMethodNames);
SUBool::logs.TLog(level) << "\tbackbones: " << conf.backbones << std::endl;
SUBool::logs.TLog(level) << "\tprime: " << conf.prime << std::endl;
SUBool::logs.TLog(level) << "\tverbosity: " << conf.verbosity << std::endl;
......@@ -65,8 +65,8 @@ print_version(std::ostream &os, bool comment = false)
os << c
<< "pcminimize - minimizing a CNF with respect to propagation "
"completeness by iterative removing of absorbed clauses.\n";
os << c << SUBool::author_year_info() << '\n';
os << c << SUBool::version_info();
os << c << SUBool::kAuthorYearInfo << '\n';
os << c << SUBool::kVersionInfo;
}
int
......@@ -74,19 +74,17 @@ parse_arguments(int argc, char *argv[], config_t &conf)
{
try
{
cxxopts::Options options(
"pcminimize",
cxxopts::Options options("pcminimize",
"pcminimize - minimizing a CNF with respect to propagation "
"completeness by iterative removing of absorbed clauses.");
options.positional_help("[input [output]]");
std::string minimize_method;
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))(
"minimize-method",
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))("minimize-method",
"Minimization method. Possible values: "
"full -- full minimization (with the full CNF) "
"simple_incremental -- sort in increasing order by sizes and then "
......@@ -100,28 +98,24 @@ parse_arguments(int argc, char *argv[], config_t &conf)
"simple_incremental.",
cxxopts::value<std::string>(minimize_method)
->default_value(SUBool::kMinimizeMethodNames.at(
static_cast<unsigned>(conf.minimize_method))))(
"B,backbones",
static_cast<unsigned>(conf.minimize_method))))("B,backbones",
"Use backbone propagation before the minimization is executed",
cxxopts::value<bool>(conf.backbones)->default_value("false"))(
"p,prime",
cxxopts::value<bool>(conf.backbones)
->default_value("false"))("p,prime",
"Make CNF prime before running the minimization (this implies using "
"backbone propagation)",
cxxopts::value<bool>(conf.prime)->default_value("false"))(
"t,timeout",
cxxopts::value<bool>(conf.prime)->default_value("false"))("t,timeout",
"Timeout for compilation in seconds as a fractional number. "
"After this amount of seconds, the process finishes. Value "
"t<=0.0 means no timeout. The timer uses CLOCK_REALTIME.",
cxxopts::value<double>(conf.timeout)
->default_value(std::to_string(conf.timeout)))(
"b,verbosity",
->default_value(std::to_string(conf.timeout)))("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(std::to_string(conf.verbosity)))(
"positional",
->default_value(std::to_string(conf.verbosity)))("positional",
"Positional arguments: these are the arguments that are entered "
"without an option",
cxxopts::value<std::vector<std::string>>());
......@@ -264,8 +258,7 @@ minimize(const config_t &conf, SUBool::CNF cnf)
{
SUBool::CPUTime cpu_time;
SUBool::CompHypothesis hyp(conf.minimize_method,
SUBool::LIT_IMPL_SYSTEM::NONE, SUBool::CNF(),
std::move(cnf), false);
SUBool::LIT_IMPL_SYSTEM::NONE, SUBool::CNF(), std::move(cnf), false);
if (conf.backbones
&& !run_with_timeout(
conf.timeout < 0.0f, conf.timeout - cpu_time.TimeSpan(),
......@@ -323,10 +316,10 @@ main(int argc, char *argv[])
std::signal(SIGINT, terminate);
SUBool::logs.TLog(SUBool::LogStream::LOG_LEVEL::MINLINES)
<< "PCMinimize" << SUBool::version_info() << std::endl;
<< "PCMinimize" << SUBool::kVersionInfo << std::endl;
dump_config(conf,
static_cast<unsigned>(SUBool::LogStream::LOG_LEVEL::MINLINES));
dump_config(
conf, static_cast<unsigned>(SUBool::LogStream::LOG_LEVEL::MINLINES));
auto ret = minimize(conf, std::move(cnf));
return ret;
}
lib/logstream.h
View file @ 96cc3f8e
......@@ -32,6 +32,7 @@ namespace SUBool
ALL
};
static const char *kMaxLogLevels;
static const unsigned kDefaultLogLevel = 3;
static const size_t kMinLogCNFSize = 10000;
static const size_t kLogStep = 1000;
......
lib/prgutil.cpp
View file @ 96cc3f8e
......@@ -9,17 +9,8 @@
#include "prgutil.h"
#include "version.h"
std::string
SUBool::version_info()
{
return SUBOOL_VERSION;
}
std::string
SUBool::author_year_info()
{
return SUBOOL_AUTHORYEAR;
}
const std::string SUBool::kVersionInfo = SUBOOL_VERSION;
const std::string SUBool::kAuthorYearInfo = SUBOOL_AUTHORYEAR;
SUBool::OutputStream::OutputStream(const std::string &fname)
: mFile(), mOk(true), mOut(&std::cout)
......@@ -39,6 +30,6 @@ void
SUBool::print_version(const std::string &prg_name, const std::string &prg_desc)
{
std::cout << prg_name << " - " << prg_desc << std::endl;
std::cout << SUBool::author_year_info() << '\n';
std::cout << SUBool::version_info() << std::endl;
std::cout << kAuthorYearInfo << '\n';
std::cout << kVersionInfo << std::endl;
}
lib/prgutil.h
View file @ 96cc3f8e
......@@ -68,7 +68,7 @@ namespace SUBool
template <class T>
T
input_or_die(const std::string &fname, LogStream &logs, unsigned level = 0,
int errcode = 2, const std::string &msg = "")
int errcode = 2, const std::string &msg = "")
{
try
{
......@@ -84,8 +84,8 @@ namespace SUBool
template <class T>
void
output(const std::string &fname, const T &t,
const std::string &preamble = "")
output(
const std::string &fname, const T &t, const std::string &preamble = "")
{
OutputStream os(fname);
if (!os)
......@@ -134,14 +134,22 @@ namespace SUBool
}
};
std::string version_info();
std::string author_year_info();
extern const std::string kAuthorYearInfo;
extern const std::string kVersionInfo;
extern const std::string kPrgName;
extern const std::string kPrgDesc;
void print_version(const std::string &prg_name, const std::string &prg_desc);
inline void
print_version()
{
print_version(kPrgName, kPrgDesc);
}
template <class T>
void
dump_value(const std::string &line_prefix, unsigned level,
const std::string &name, const T &value)
const std::string &name, const T &value)
{
logs.TLog(level) << line_prefix << name << ": " << value << std::endl;
}
......@@ -149,7 +157,7 @@ namespace SUBool
template <>
inline void
dump_value<bool>(const std::string &line_prefix, unsigned level,
const std::string &name, const bool &value)
const std::string &name, const bool &value)
{
logs.TLog(level) << line_prefix << name << ": " << bool_to_string(value)
<< std::endl;
......@@ -158,8 +166,7 @@ namespace SUBool
template <class Enum, class Names>
void
dump_enum_value(const std::string &line_prefix, unsigned level,
const std::string &name, const Enum &enum_value,
const Names &names)
const std::string &name, const Enum &enum_value, const Names &names)
{
logs.TLog(level) << line_prefix << name << ": "