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

DumpVerbosity, parametry triple_cnf, rhbdmc_compile

parent d3b0d684
......@@ -82,8 +82,7 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level)
<< "\tprocess: " << process_names.at(static_cast<unsigned>(conf.process))
<< std::endl;
SUBool::logs.TLog(level)
<< "\tverbosity: " << SUBool::logs.mVerbLevel << std::endl;
SUBool::logs.DumpVerbosity("\t", level);
}
int
......
......@@ -68,8 +68,7 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level) << "Configuration:" << std::endl;
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: " << SUBool::logs.mVerbLevel << std::endl;
SUBool::logs.DumpVerbosity("\t", level);
kRelationAnnotation.DumpValue("\t", level, "relation", conf.relation);
kCompareKindAnnotation.DumpValue(
"\t", level, "compare_kind", conf.compare_kind);
......
......@@ -33,7 +33,7 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level) << "Configuration:" << std::endl;
SUBool::logs.DumpValue("\t", level, "file_left", conf.file_left);
SUBool::logs.DumpValue("\t", level, "file_right", conf.file_right);
SUBool::logs.DumpValue("\t", level, "verbosity", SUBool::logs.mVerbLevel);
SUBool::logs.DumpVerbosity("\t", level);
SUBool::logs.DumpValue("\t", level, "suppress_first", conf.suppress_first);
SUBool::logs.DumpValue("\t", level, "suppress_second", conf.suppress_second);
SUBool::logs.DumpValue("\t", level, "suppress_third", conf.suppress_third);
......
......@@ -63,8 +63,7 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level) << "\tinput_file: " << conf.input_file << std::endl;
SUBool::logs.TLog(level)
<< "\toutput_file: " << conf.output_file << std::endl;
SUBool::logs.TLog(level)
<< "\tverbosity: " << SUBool::logs.mVerbLevel << std::endl;
SUBool::logs.DumpVerbosity("\t", level);
kGraphKindAnnotation.DumpValue("\t", level, "graph_kind", conf.graph_kind);
kOutputTypeAnnotation.DumpValue(
"\t", level, "output_type", conf.output_type);
......
......@@ -61,8 +61,7 @@ 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: " << SUBool::logs.mVerbLevel << std::endl;
SUBool::logs.DumpVerbosity("\t", level);
}
SUBool::CNF
......
......@@ -55,7 +55,7 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level) << "Configuration:" << std::endl;
SUBool::logs.DumpValue("\t", level, "input_file", conf.input_file);
SUBool::logs.DumpValue("\t", level, "output_file", conf.output_file);
SUBool::logs.DumpValue("\t", level, "verbosity", SUBool::logs.mVerbLevel);
SUBool::logs.DumpVerbosity("\t", level);
SUBool::logs.DumpValue("\t", level, "max_input_var", conf.max_input_var);
SUBool::logs.DumpValue("\t", level, "elim_minimize", conf.elim_minimize);
SUBool::CNFEncoding::kBlockPrimeAnnotation.DumpValue(
......
......@@ -75,7 +75,7 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level) << "Configuration:" << std::endl;
SUBool::logs.DumpValue("\t", level, "input_file", conf.input_file);
SUBool::logs.DumpValue("\t", level, "output_file", conf.output_file);
SUBool::logs.DumpValue("\t", level, "verbosity", SUBool::logs.mVerbLevel);
SUBool::logs.DumpVerbosity("\t", level);
kImplTypeAnnotation.DumpValue("\t", level, "impl_type", conf.impl_type);
kOutputTypeAnnotation.DumpValue(
"\t", level, "output_type", conf.output_type);
......
......@@ -71,7 +71,7 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level) << "Configuration:" << std::endl;
SUBool::logs.DumpValue("\t", level, "input_file", conf.input_file);
SUBool::logs.DumpValue("\t", level, "output_file", conf.output_file);
SUBool::logs.DumpValue("\t", level, "verbosity", SUBool::logs.mVerbLevel);
SUBool::logs.DumpVerbosity("\t", level);
kEncodingTypeAnnotation.DumpValue(
"\t", level, "encoding_type", conf.encoding_type);
SUBool::logs.DumpValue("\t", level, "final_minimize", conf.final_minimize);
......
......@@ -31,8 +31,7 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level) << "\tinput_file: " << conf.input_file << std::endl;
SUBool::logs.TLog(level)
<< "\toutput_file: " << conf.output_file << std::endl;
SUBool::logs.TLog(level)
<< "\tverbosity: " << SUBool::logs.mVerbLevel << std::endl;
SUBool::logs.DumpVerbosity("\t", level);
SUBool::logs.TLog(level)
<< "\tcheck_only: " << SUBool::bool_to_string(conf.check_only)
<< std::endl;
......
......@@ -8,7 +8,6 @@
*/
#include <csignal>
#include <cxxopts.hpp>
#include <iostream>
#include "cpuutil.h"
......@@ -19,13 +18,13 @@
const std::string SUBool::kPrgName = "rhbdmc_compile";
const std::string SUBool::kPrgDesc =
"Program which aims to compile a given CNF into a RH-BDMC (Renamable Horn "
"BDMC). The idea is based on construction of a RH backdoor tree. ";
"BDMC). The idea is based on construction of a RH backdoor tree. The "
"program is *EXPERIMENTAL* and most probably does not work correctly.";
struct config_t
{
std::string input_file{};
std::string output_file{};
unsigned verbosity{3}; // 0 means no output
};
void
......@@ -35,54 +34,20 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level) << "\tinput_file: " << conf.input_file << std::endl;
SUBool::logs.TLog(level)
<< "\toutput_file: " << conf.output_file << std::endl;
SUBool::logs.TLog(level) << "\tverbosity: " << conf.verbosity << std::endl;
SUBool::logs.DumpVerbosity("\t", level);
}
int
parse_arguments(int argc, char *argv[], config_t &conf)
std::optional<config_t>
parse_arguments(int argc, char *argv[])
{
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")("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));
options.parse_positional({"input", "output", "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 input and output are allowed" << std::endl;
SUBool::logs.TLog(0) << options.help() << std::endl;
return 1;
}
}
catch (const cxxopts::OptionException &e)
config_t conf;
SUBool::PrgOptions opts;
opts.InputOutput(&conf.input_file, &conf.output_file);
if (!opts.Parse(argc, argv))
{
std::cerr << "Error parsing options: " << e.what() << std::endl;
return 1;
return {};
}
return 0;
return conf;
}
void
......@@ -95,26 +60,24 @@ term_func(int signal)
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;
std::signal(SIGTERM, term_func);
std::signal(SIGQUIT, term_func);
std::signal(SIGINT, term_func);
dump_config(conf, 0);
dump_config(*conf, 3);
SUBool::RHBackdoorTree bt(
SUBool::input_or_die<SUBool::CNF>(conf.input_file, SUBool::logs));
SUBool::input_or_die<SUBool::CNF>(conf->input_file, SUBool::logs));
SUBool::logs.TLog(1) << "Start compilation" << std::endl;
SUBool::CPUTime cpu_time;
bt.Compute();
SUBool::logs.TLog(1) << "Compilation finished" << std::endl;
SUBool::logs.TLog(1) << "Total processor time: " << cpu_time << std::endl;
SUBool::logs.TLog(0) << "Number of leaves: " << bt.LeafSize() << std::endl;
SUBool::output(conf.output_file, std::move(bt).CurrentNnf());
SUBool::output(conf->output_file, std::move(bt).CurrentNnf());
SUBool::logs.Log(1) << std::endl;
SUBool::logs.TLog(1) << "Output written" << std::endl;
return 0;
......
......@@ -6,68 +6,71 @@
* Program for splitting a CNF into renamable horn parts.
*/
#include <iostream>
#include <fstream>
#include <iostream>
#include "rhorn.h"
#include "mrh.h"
#include "rhorn.h"
void
void
ProcessStream(std::istream &in, const std::string &name)
{
SUBool::CNF cnf;
in>>cnf;
std::cout<<"\""<<name<<"\";";
std::vector< std::pair<SUBool::CNF, SUBool::Assignment> > part_list;
in >> cnf;
std::cout << "\"" << name << "\";";
std::vector<std::pair<SUBool::CNF, SUBool::Assignment>> part_list;
SUBool::SplitToRenamableHornParts(cnf, &part_list);
std::cout<<cnf.MaxVariable()<<';'<<cnf.Size()<<';'<<part_list.size();
for(const auto &part : part_list)
std::cout << cnf.MaxVariable() << ';' << cnf.Size() << ';'
<< part_list.size();
for (const auto &part : part_list)
{
std::cout<<';'<<part.first.Size();
std::cout << ';' << part.first.Size();
}
for(unsigned i=part_list.size(); i<5; ++i)
for (unsigned i = part_list.size(); i < 5; ++i)
{
std::cout<<";0";
std::cout << ";0";
}
std::vector<unsigned> var_count(cnf.MaxVariable(), 0);
for(const auto &part : part_list)
for (const auto &part : part_list)
{
std::vector<bool> var_in_part(cnf.MaxVariable(), false);
for(const auto &clause : part.first)
for (const auto &clause : part.first)
{
for(const auto &lit : clause)
for (const auto &lit : clause)
{
if(!var_in_part[lit.mVariable-1])
if (!var_in_part[lit.mVariable - 1])
{
var_in_part[lit.mVariable-1]=true;
++var_count[lit.mVariable-1];
var_in_part[lit.mVariable - 1] = true;
++var_count[lit.mVariable - 1];
}
}
}
}
unsigned count=0;
for(const auto &c : var_count)
unsigned count = 0;
for (const auto &c : var_count)
{
if(c>1)
if (c > 1)
{
++count;
}
}
std::cout<<";"<<count;
std::cout<<std::endl;
std::cout << ";" << count;
std::cout << std::endl;
}
int
int
main(int argc, char *argv[])
{
std::cout<<"name;max_var;cnf_size;n_parts;p0_size;p1_size;p2_size;p3_size;p4_size;common_vars"<<std::endl;
if(argc==1)
std::cout << "name;max_var;cnf_size;n_parts;p0_size;p1_size;p2_size;p3_size;"
"p4_size;common_vars"
<< std::endl;
if (argc == 1)
{
ProcessStream(std::cin, "-");
}
else
{
for(int i=1; i<argc; ++i)
for (int i = 1; i < argc; ++i)
{
std::ifstream in(argv[i]);
ProcessStream(in, argv[i]);
......
......@@ -8,7 +8,6 @@
*/
#include <csignal>
#include <cxxopts.hpp>
#include <iostream>
#include "assign.h"
......@@ -24,7 +23,6 @@ const std::string SUBool::kPrgDesc =
struct config_t
{
std::string output_file{};
unsigned verbosity{3}; // 0 means no output
unsigned n{0};
};
......@@ -34,54 +32,26 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level) << "Configuration:" << std::endl;
SUBool::logs.TLog(level)
<< "\toutput_file: " << conf.output_file << std::endl;
SUBool::logs.TLog(level) << "\tverbosity: " << conf.verbosity << std::endl;
SUBool::logs.DumpVerbosity("\t", level);
SUBool::logs.TLog(level) << "\tn: " << conf.n << std::endl;
}
int
parse_arguments(int argc, char *argv[], config_t &conf)
std::optional<config_t>
parse_arguments(int argc, char *argv[])
{
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")("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))("o,output",
"Output file with the encoding CNF in DIMACS format",
cxxopts::value<std::string>(conf.output_file))("n",
"The number of variables is 3n",
cxxopts::value<unsigned>(conf.n)->default_value("2"));
options.parse_positional({"output", "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 output file is allowed" << std::endl;
SUBool::logs.TLog(0) << options.help() << std::endl;
return 1;
}
}
catch (const cxxopts::OptionException &e)
config_t conf;
SUBool::PrgOptions opts;
opts.SinglePositional({&conf.output_file, "output"});
po::options_description desc("Configuration options");
desc.add_options()("number-of-variables,n",
po::value<unsigned>(&conf.n)->default_value(2),
"The number of variables is 3n");
opts.Add(desc);
if (!opts.Parse(argc, argv))
{
std::cerr << "Error parsing options: " << e.what() << std::endl;
return 1;
return {};
}
return 0;
return conf;
}
void
......@@ -127,17 +97,15 @@ generate(unsigned n)
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;
std::signal(SIGTERM, term_func);
std::signal(SIGQUIT, term_func);
std::signal(SIGINT, term_func);
dump_config(conf, 0);
SUBool::output(conf.output_file, generate(conf.n));
dump_config(*conf, 0);
SUBool::output(conf->output_file, generate(conf->n));
return 0;
}
......@@ -89,6 +89,8 @@ namespace SUBool
<< std::endl;
}
}
void DumpVerbosity(const std::string &line_prefix, unsigned level);
};
extern LogStream logs;
......@@ -103,4 +105,10 @@ SUBool::LogStream::DumpValue<bool>(const std::string &line_prefix,
DumpValue<std::string>(line_prefix, level, name, bool_to_string(value));
}
inline void
SUBool::LogStream::DumpVerbosity(const std::string &line_prefix, unsigned level)
{
DumpValue(line_prefix, level, "verbosity", mVerbLevel);
}
#endif
......@@ -85,6 +85,15 @@ SUBool::PrgOptions::InputPair(
mPositionalHelp += "[" + first.desc + " [" + second.desc + "]]";
}
void
SUBool::PrgOptions::SinglePositional(const PositFileDesc &file_desc)
{
mHidden.add_options()(
file_desc.desc.c_str(), po::value<std::string>(file_desc.fname));
mPositional.add(file_desc.desc.c_str(), 1);
mPositionalHelp += "[" + file_desc.desc + "]";
}
bool
SUBool::PrgOptions::ProcessCommon() const
{
......
......@@ -178,6 +178,7 @@ namespace SUBool
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);
void SinglePositional(const PositFileDesc &file_desc);
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