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

Partial switch to boost::program_options

parent 96cc3f8e
cmake_minimum_required (VERSION 3.0.2)
function(su_add_exec name use_glucose use_kissat)
set(ATE_LIBS ${name} subool)
set(ATE_SRC ${name}.cpp)
function(su_add_exec_x name use_glucose use_kissat)
set(ATE_LIBS subool)
if (${use_glucose})
su_add_glucose_lib(ATE_LIBS)
endif()
if (${use_kissat})
su_add_kissat_lib(ATE_LIBS)
endif()
add_executable (${name} ${ATE_SRC} ${ARGN})
target_link_libraries (${ATE_LIBS})
add_executable (${name} ${ARGN})
target_link_libraries (${name} ${ATE_LIBS})
target_link_libraries (${name} ${Boost_LIBRARIES})
endfunction(su_add_exec_x)
function(su_add_exec name use_glucose use_kissat)
su_add_exec_x(${name} ${use_glucose} ${use_kissat} ${name}.cpp)
endfunction(su_add_exec)
add_executable (rhornsplit rhornsplit.cpp)
......@@ -23,16 +27,12 @@ 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)
su_add_exec(cnfdiff false false)
add_executable (cnfdiff cnfdiff.cpp)
target_link_libraries (cnfdiff subool)
add_executable (cnfgraph cnfgraphx.cpp)
target_link_libraries (cnfgraph subool)
su_add_exec_x(cnfgraph false false cnfgraphx.cpp)
su_add_exec(nnfencode true true)
su_add_exec(dpelim true true)
......@@ -40,11 +40,8 @@ su_add_exec(nnfsmooth true false)
su_add_exec(rhbdmc_compile true true)
su_add_pthread (rhbdmc_compile)
add_executable (triple_cnf triple_cnf.cpp)
target_link_libraries (triple_cnf subool)
add_executable (gdbasis gdbasis.cpp)
target_link_libraries (gdbasis subool)
su_add_exec(triple_cnf false false)
su_add_exec(gdbasis false false)
# add_executable (horn_uniform_pcgen horn_uniform_pcgen.cpp)
# target_link_libraries (horn_uniform_pcgen subool ${GLUCOSE_LIB})
......@@ -9,11 +9,9 @@
#include <fstream>
#include <iostream>
#include <optional>
#include <string>
#include <boost/optional.hpp>
#include <boost/program_options.hpp>
#include "canon.h"
#include "cnfutil.h"
#include "cpuutil.h"
......@@ -22,8 +20,6 @@
#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";
......@@ -31,82 +27,54 @@ const std::string SUBool::kPrgDesc =
enum class PROCESS
{
NONE,
SAT,
Last = SAT
PRIME,
Last = PRIME
};
const std::array<std::string, static_cast<size_t>(PROCESS::Last) + 1>
process_names{"none", "prime"};
const char *kProcessOptDesc = "Clause inprocessing and preprocessing level.\n"
"none = No inprocessing,\n"
"prime = use SAT to find a prime subimplicate.";
struct config_t
{
std::string input_file{};
std::string output_file{};
PROCESS process{PROCESS::SAT};
PROCESS process{PROCESS::PRIME};
unsigned verbosity{3};
};
boost::optional<config_t>
std::optional<config_t>
parse_arguments(int argc, char *argv[])
{
config_t conf;
try
{
po::options_description visible("Allowed options");
//"cnfcanon", "cnfcanon - construct the canonical CNF for a given CNF.");
// options.positional_help("[input [output]]");
unsigned process = 0;
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.");
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));
std::string process;
auto visible = SUBool::prg_common_opts("Allowed options", conf.verbosity);
visible.add_options()("process,p",
po::value<std::string>(&process)->default_value(
process_names.at(static_cast<unsigned>(conf.process))),
kProcessOptDesc);
auto [hidden, positional] =
SUBool::prg_input_output_opts(conf.input_file, 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(),
po::store(po::command_line_parser(argc, argv)
.options(desc)
.positional(positional)
.run(),
vm);
po::notify(vm);
if (vm.count("help"))
if (!SUBool::prg_process_common_opts(
std::cout, visible, "[input [output]]", vm))
{
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;
return 1;
}
if (result.count("positional"))
{
std::cerr << "Multiple files passed as parameters, ";
std::cerr << "only input and output are allowed" << std::endl;
std::cerr << options.help() << std::endl;
return 1;
}
conf->process = SUBool::enum_of_int<PROCESS>(process);
#endif
conf.process = SUBool::enum_of_name<PROCESS>(process, process_names);
}
catch (std::exception &e)
{
......@@ -124,7 +92,8 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level)
<< "\toutput_file: " << conf.output_file << std::endl;
SUBool::logs.TLog(level)
<< "\tprocess: " << static_cast<unsigned>(conf.process) << std::endl;
<< "\tprocess: " << process_names.at(static_cast<unsigned>(conf.process))
<< std::endl;
SUBool::logs.TLog(level) << "\tverbosity: " << conf.verbosity << std::endl;
}
......@@ -160,7 +129,7 @@ canon_procedure(const config_t &conf, const SUBool::CNF &cnf)
{
case PROCESS::NONE:
return std::unique_ptr<SUBool::AbsCanon>(new SUBool::CanonBase(cnf));
case PROCESS::SAT:
case PROCESS::PRIME:
return std::unique_ptr<SUBool::AbsCanon>(new SUBool::CanonSAT(cnf));
}
throw SUBool::BadParameterException(
......
......@@ -24,12 +24,12 @@ enum class CheckKind
};
const std::map<std::string, CheckKind> check_kind_names = {
{"eq", CheckKind::EQUAL}, {"le", CheckKind::LEQ},
{"ge", CheckKind::GEQ}, {"equal", CheckKind::EQUAL},
{"leq", CheckKind::LEQ}, {"geq", CheckKind::GEQ}};
{"eq", CheckKind::EQUAL}, {"le", CheckKind::LEQ}, {"ge", CheckKind::GEQ},
{"equal", CheckKind::EQUAL}, {"leq", CheckKind::LEQ},
{"geq", CheckKind::GEQ}};
const std::string prg_name = "cnfcomp";
const std::string prg_desc =
const std::string SUBool::kPrgName = "cnfcomp";
const std::string SUBool::kPrgDesc =
"compare two functions represented by CNF formulas";
enum class CompareKind
......@@ -62,8 +62,8 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level)
<< "\tcheck_kind: " << static_cast<unsigned>(conf.check_kind)
<< std::endl;
SUBool::dump_enum_value("\t", level, "compare_kind", conf.compare_kind,
compare_kind_names);
SUBool::dump_enum_value(
"\t", level, "compare_kind", conf.compare_kind, compare_kind_names);
}
CheckKind
......@@ -75,8 +75,8 @@ parse_check_kind(const std::string &check_kind)
}
catch (std::out_of_range &e)
{
throw SUBool::BadParameterException("parse_check_kind",
"Unknown check kind specification");
throw SUBool::BadParameterException(
"parse_check_kind", "Unknown check kind specification");
}
}
......@@ -85,27 +85,25 @@ 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-left [input-right]]");
std::string check_kind;
std::string compare_kind;
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))(
"l,input-left", "The left hand input file",
cxxopts::value<std::string>(conf.file_left))(
"r,input-right", "The right hand input file",
cxxopts::value<std::string>(conf.file_right))(
"c,check-kind",
->default_value(SUBool::LogStream::kMaxLogLevels))("l,input-left",
"The left hand input file",
cxxopts::value<std::string>(conf.file_left))("r,input-right",
"The right hand input file",
cxxopts::value<std::string>(conf.file_right))("c,check-kind",
"What to check. eq=equality, le=less than or equal, ge=greater than "
"or equal.",
cxxopts::value<std::string>(check_kind)->default_value("eq"))(
"k,compare-kind",
cxxopts::value<std::string>(check_kind)
->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), "
......@@ -124,7 +122,7 @@ parse_arguments(int argc, char *argv[], config_t &conf)
}
if (result.count("version"))
{
SUBool::print_version(prg_name, prg_desc);
SUBool::print_version(std::cout);
return 1;
}
if (result.count("positional"))
......@@ -171,15 +169,15 @@ eq_to_string(config_t &conf)
ss << "Each formula absorbs the other one.";
break;
default:
throw SUBool::BadParameterException("eq_to_string",
"unknown compare kind");
throw SUBool::BadParameterException(
"eq_to_string", "unknown compare kind");
}
return ss.str();
}
std::string
implies_to_string(config_t &conf, const std::string &l, const std::string &r,
bool strict)
implies_to_string(
config_t &conf, const std::string &l, const std::string &r, bool strict)
{
std::stringstream ss;
switch (conf.compare_kind)
......@@ -209,15 +207,15 @@ implies_to_string(config_t &conf, const std::string &l, const std::string &r,
<< l << ".";
break;
default:
throw SUBool::BadParameterException("eq_to_string",
"unknown compare kind");
throw SUBool::BadParameterException(
"eq_to_string", "unknown compare kind");
}
return ss.str();
}
std::string
not_implies_to_string(config_t &conf, const std::string &l,
const std::string &r)
not_implies_to_string(
config_t &conf, const std::string &l, const std::string &r)
{
std::stringstream ss;
switch (conf.compare_kind)
......@@ -234,15 +232,15 @@ not_implies_to_string(config_t &conf, const std::string &l,
<< " are not all absorbed (some are empowering) by the " << l << ".";
break;
default:
throw SUBool::BadParameterException("eq_to_string",
"unknown compare kind");
throw SUBool::BadParameterException(
"eq_to_string", "unknown compare kind");
}
return ss.str();
}
bool
check_equality(config_t &conf, const SUBool::CNF &left_cnf,
const SUBool::CNF &right_cnf)
check_equality(
config_t &conf, const SUBool::CNF &left_cnf, const SUBool::CNF &right_cnf)
{
SUBool::CompareResult result = SUBool::CompareResult::INCOMPARABLE;
switch (conf.compare_kind)
......@@ -257,8 +255,8 @@ check_equality(config_t &conf, const SUBool::CNF &left_cnf,
result = SUBool::cnf_compare_absorb(left_cnf, right_cnf);
break;
default:
throw SUBool::BadParameterException("check_equality",
"unknown compare kind");
throw SUBool::BadParameterException(
"check_equality", "unknown compare kind");
}
switch (result)
{
......@@ -268,14 +266,14 @@ check_equality(config_t &conf, const SUBool::CNF &left_cnf,
break;
case SUBool::CompareResult::LESS:
SUBool::logs.TLog(1) << "(L<R)" << std::endl;
SUBool::logs.TLog(2) << implies_to_string(conf, "first formula (L)",
"second one (R)", true)
SUBool::logs.TLog(2) << implies_to_string(
conf, "first formula (L)", "second one (R)", true)
<< std::endl;
break;
case SUBool::CompareResult::GREATER:
SUBool::logs.TLog(1) << "(L>R)" << std::endl;
SUBool::logs.TLog(2) << implies_to_string(conf, "second formula (R)",
"first one (L)", true)
SUBool::logs.TLog(2) << implies_to_string(
conf, "second formula (R)", "first one (L)", true)
<< std::endl;
break;
case SUBool::CompareResult::EQUAL:
......@@ -287,7 +285,7 @@ check_equality(config_t &conf, const SUBool::CNF &left_cnf,
bool
check_implication(config_t &conf, const SUBool::CNF &left_cnf,
const SUBool::CNF &right_cnf, bool swapped)
const SUBool::CNF &right_cnf, bool swapped)
{
bool result = false;
switch (conf.compare_kind)
......@@ -302,8 +300,8 @@ check_implication(config_t &conf, const SUBool::CNF &left_cnf,
result = SUBool::cnf_absorbed(left_cnf, right_cnf);
break;
default:
throw SUBool::BadParameterException("check_equality",
"unknown compare kind");
throw SUBool::BadParameterException(
"check_equality", "unknown compare kind");
}
std::string first, second, l, r;
if (swapped)
......
......@@ -11,9 +11,10 @@
#include "normalform.h"
#include "prgutil.h"
const std::string prg_name = "cnfdiff";
const std::string prg_desc = "Program for comparing two CNFs as sets of "
"clauses (not as representations of * functions).";
const std::string SUBool::kPrgName = "cnfdiff";
const std::string SUBool::kPrgDesc =
"Program for comparing two CNFs as sets of "
"clauses (not as representations of * functions).";
struct config_t
{
......@@ -42,26 +43,27 @@ 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-left [input-right]]");
std::string check_kind;
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))(
"l,input-left", "The left hand input file",
cxxopts::value<std::string>(conf.file_left))(
"r,input-right", "The right hand input file",
cxxopts::value<std::string>(conf.file_right))(
"1", "Suppress printing the clauses unique to the first CNF.",
cxxopts::value<bool>(conf.suppress_first)->default_value("false"))(
"2", "Suppress printing the clauses unique to the second CNF.",
cxxopts::value<bool>(conf.suppress_second)->default_value("false"))(
"3", "Suppress printing the clauses which are in both CNF formulas.",
->default_value(SUBool::LogStream::kMaxLogLevels))("l,input-left",
"The left hand input file",
cxxopts::value<std::string>(conf.file_left))("r,input-right",
"The right hand input file",
cxxopts::value<std::string>(conf.file_right))("1",
"Suppress printing the clauses unique to the first CNF.",
cxxopts::value<bool>(conf.suppress_first)
->default_value("false"))("2",
"Suppress printing the clauses unique to the second CNF.",
cxxopts::value<bool>(conf.suppress_second)
->default_value("false"))("3",
"Suppress printing the clauses which are in both CNF formulas.",
cxxopts::value<bool>(conf.suppress_third)->default_value("false"));
options.parse_positional({"input-left", "input-right", "positional"});
auto result = options.parse(argc, argv);
......@@ -72,7 +74,7 @@ parse_arguments(int argc, char *argv[], config_t &conf)
}
if (result.count("version"))
{
SUBool::print_version(prg_name, prg_desc);
SUBool::print_version(std::cout);
return 1;
}
if (result.count("positional"))
......@@ -156,7 +158,6 @@ main(int argc, char *argv[])
return r;
}
compare(SUBool::input_or_die<SUBool::CNF>(conf.file_left, SUBool::logs),
SUBool::input_or_die<SUBool::CNF>(conf.file_right, SUBool::logs),
conf);
SUBool::input_or_die<SUBool::CNF>(conf.file_right, SUBool::logs), conf);
return 0;
}
......@@ -159,7 +159,7 @@ parse_arguments(int argc, char *argv[], config_t &conf)
}
if (result.count("version"))
{
SUBool::print_version();
SUBool::print_version(std::cout);
return 1;
}
if (result.count("positional"))
......
......@@ -19,8 +19,8 @@
#include "prgutil.h"
#include "sbexception.h"
const std::string prg_name = "cnfprime";
const std::string prg_desc = "Making a CNF prime";
const std::string SUBool::kPrgName = "cnfprime";
const std::string SUBool::kPrgDesc = "Making a CNF prime";
const std::string prg_help =
"Makes a given CNF prime, possibly only with respect to 1-provability.";
......@@ -38,27 +38,24 @@ parse_arguments(int argc, char *argv[])
config_t conf;
try
{
cxxopts::Options options(
"cnfprime", "cnfprime - construct a prime CNF for a given CNF.");
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",
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",
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",
->default_value(SUBool::LogStream::kMaxLogLevels))("positional",
"Positional arguments: these are the arguments that are entered "
"without an option",
cxxopts::value<std::vector<std::string>>());
......@@ -71,7 +68,7 @@ parse_arguments(int argc, char *argv[])
}
if (result.count("version"))
{
SUBool::print_version(prg_name, prg_desc);
SUBool::print_version(std::cout);
exit(1);
}
if (result.count("positional"))
......
......@@ -15,8 +15,8 @@
#include "logstream.h"
#include "prgutil.h"
const std::string prg_name = "dpelim";
const std::string prg_desc = "DP elimination of variables";
const std::string SUBool::kPrgName = "dpelim";
const std::string SUBool::kPrgDesc = "DP elimination of variables";
const std::string prg_help =
"DP elimination of variables. By default it aims to eliminate all "
"variables, use -f, -s options to limit the extent of elimination. You can "
......@@ -36,24 +36,20 @@ enum class ELIMINATE
const std::unordered_map<ELIMINATE, std::string, SUBool::EnumClassHash>
eliminate_names = {{ELIMINATE::ALL, "all"},
{ELIMINATE::MAX_INCREASE, "max_increase"},
{ELIMINATE::FACTOR, "factor"}};
{ELIMINATE::MAX_INCREASE, "max_increase"},
{ELIMINATE::FACTOR, "factor"}};
const std::array<std::string,
static_cast<size_t>(SUBool::DPEliminator::IGNORE_POLICY::Last)
+ 1>
static_cast<size_t>(SUBool::DPEliminator::IGNORE_POLICY::Last) + 1>
elim_ignore_policy_names{"none", "implicate", "absorbed"};
const std::array<std::string,
static_cast<size_t>(SUBool::DPEliminator::INPROCESSING::Last)
+ 1>
static_cast<size_t>(SUBool::DPEliminator::INPROCESSING::Last) + 1>
elim_inprocessing_names{"none", "prime"};
const std::array<std::string, static_cast<size_t>(
SUBool::DPEliminator::INCREASE_POLICY::Last)
+ 1>
const std::array<std::string,
static_cast<size_t>(SUBool::DPEliminator::INCREASE_POLICY::Last) + 1>
elim_increase_policy_names{"estimate", "bound", "new", "new_total"};
const std::array<std::string,
static_cast<size_t>(SUBool::CNFEncoding::BLOCK_PRIME::Last)
+ 1>
static_cast<size_t>(SUBool::CNFEncoding::BLOCK_PRIME::Last) + 1>
block_prime_names{"none", "up_prime", "prime"};
struct elim_config_t
......@@ -70,7 +66,8 @@ struct elim_config_t
SUBool::DPEliminator::INCREASE_POLICY::AFTER_BOUND};
size_t minimize_size_step{5000};
double minimize_size_factor{0.6};
union {
union
{
size_t max_increase;
long double factor;
};
......@@ -95,24 +92,23 @@ dump_config(const config_t &conf, unsigned level)
SUBool::dump_value("\t", level, "verbosity", conf.verbosity);
SUBool::dump_value("\t", level, "max_input_var", conf.max_input_var);
SUBool::dump_value("\t", level, "elim.use_minimize", conf.elim.use_minimize);
SUBool::dump_value(
"\t", level, "elim.block_prime",
SUBool::dump_value("\t", level, "elim.block_prime",
block_prime_names.at(static_cast<unsigned>(conf.elim.block_prime)));
SUBool::dump_value("\t", level, "elim.eliminate",
eliminate_names.at(conf.elim.eliminate));
SUBool::dump_value(
"\t", level, "elim.eliminate", eliminate_names.at(conf.elim.eliminate));
SUBool::dump_value("\t", level, "elim.ignore_policy",
elim_ignore_policy_names.at(
static_cast<unsigned>(conf.elim.ignore_policy)));
elim_ignore_policy_names.at(
static_cast<unsigned>(conf.elim.ignore_policy)));
SUBool::dump_value("\t", level, "elim.inprocessing",
elim_inprocessing_names.at(
static_cast<unsigned>(conf.elim.inprocessing)));