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

Program cnfsize

parent 4979f95f
......@@ -31,6 +31,7 @@ su_add_exec(cnfcanon true true)
su_add_exec(cnfprime true true)
su_add_exec(cnfcomp true true)
su_add_exec(cnfdiff false false)
su_add_exec(cnfsize false false)
su_add_exec_x(cnfgraph false false cnfgraphx.cpp)
......
/*
* Project SUBool
* Petr Kucera, 2022
*/
/**@file cnfsize.cpp
* Program for printing size statistics of CNF formulas.
*/
#include <string>
#include <vector>
#include "dimacs.h"
#include "normalform.h"
#include "prgutil.h"
const std::string SUBool::kPrgName = "cnfsize";
const std::string SUBool::kPrgDesc = "Determining the sizes of CNF formulas";
struct config_t : public SUBool::PrgConfigBase
{
std::vector<std::string> input_files{};
bool print_vars{false};
bool print_size{false};
bool print_length{false};
bool print_head{false};
virtual void InnerDump(unsigned level) const override;
};
void
config_t::InnerDump(unsigned level) const
{
SUBool::logs.TLog(level) << "input files:";
for (const auto &fname : input_files)
{
SUBool::logs.Log(level) << ' ' << fname;
}
SUBool::logs.Log(level) << '\n';
SUBool::logs.DumpValue("\t", level, "print_vars", print_vars);
SUBool::logs.DumpValue("\t", level, "print_size", print_size);
SUBool::logs.DumpValue("\t", level, "print_length", print_length);
SUBool::logs.DumpValue("\t", level, "print_head", print_head);
}
std::optional<config_t>
parse_arguments(int argc, char *argv[])
{
config_t conf;
SUBool::PrgOptions opts;
opts.SetMultipleInputs(&conf.input_files);
po::options_description desc("Configuration options");
desc.add_options() //
("print-head,H", po::bool_switch(&conf.print_head),
"Print the header line") //
("print-vars,n", po::bool_switch(&conf.print_vars),
"Print column with the number of variables (var)") //
("print-size,m", po::bool_switch(&conf.print_size),
"Print column with the number of clauses (cls)") //
("print-length,l", po::bool_switch(&conf.print_length),
"Print column with the length of the formula (len)");
opts.Add(desc);
if (!opts.Parse(argc, argv, conf))
{
return {};
}
if (!conf.print_vars && !conf.print_size && !conf.print_length)
{
conf.print_vars = conf.print_size = conf.print_length = true;
}
return conf;
}
int
process_cnf(const config_t &conf [[maybe_unused]], const SUBool::CNF &cnf,
const std::string &fname)
{
if (conf.print_vars)
{
std::cout << std::setw(8) << cnf.MaxVariable();
}
if (conf.print_size)
{
std::cout << std::setw(8) << cnf.Size();
}
if (conf.print_length)
{
std::cout << std::setw(8) << cnf.Length();
}
std::cout << ' ' << fname << '\n';
return 0;
}
int
process_file(const config_t &conf, const std::string &fname)
{
auto cnf = SUBool::input_or_die<SUBool::CNF>(fname);
return process_cnf(conf, cnf, fname);
}
void
print_head(const config_t &conf)
{
if (!conf.print_head)
{
return;
}
if (conf.print_vars)
{
std::cout << std::setw(8) << "var";
}
if (conf.print_size)
{
std::cout << std::setw(8) << "cls";
}
if (conf.print_length)
{
std::cout << std::setw(8) << "len";
}
std::cout << '\n';
}
int
process(const config_t &conf)
{
print_head(conf);
if (conf.input_files.empty())
{
return process_file(conf, "");
}
int retcode = 0;
for (const auto &fname : conf.input_files)
{
retcode = process_file(conf, fname);
if (retcode != 0)
{
break;
}
}
return retcode;
}
int
main(int argc, char *argv[])
{
auto conf = parse_arguments(argc, argv);
if (!conf)
{
return 1;
}
conf->Dump(SUBool::LogStream::kDumpShortConfigLevel);
return process(*conf);
}
......@@ -38,6 +38,9 @@ namespace SUBool
static const size_t kMinLogCNFSize = 10000;
static const size_t kLogStep = 1000;
static const unsigned kDumpConfigLevel = 1;
// kDumpShortConfigLevel is for utilities that do not have an
// "interesting" config
static const unsigned kDumpShortConfigLevel = 4;
std::atomic<unsigned> mVerbLevel;
......
......@@ -89,6 +89,15 @@ SUBool::PrgOptions::InputPair(
mPositionalHelp += "[" + first.desc + " [" + second.desc + "]]";
}
void
SUBool::PrgOptions::SetMultipleInputs(std::vector<std::string> *input_files)
{
mHidden.add_options()(
"input", po::value<std::vector<std::string>>(input_files), "input");
mPositional.add("input", -1);
mPositionalHelp += kMultipleInputsHelp;
}
void
SUBool::PrgOptions::SinglePositional(const PositFileDesc &file_desc)
{
......
......@@ -183,6 +183,7 @@ namespace SUBool
inline static const std::string kCommonOptsLabel = "Common options";
inline static const std::string kInputOutputHelp = "[input [output]]";
inline static const std::string kCfgSuffix = ".cfg";
inline static const std::string kMultipleInputsHelp = "[input ...]";
PrgOptions(bool use_config_file = false,
const std::string &common_opts_label = kCommonOptsLabel)
......@@ -199,6 +200,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 SetMultipleInputs(std::vector<std::string> *input_files);
void SinglePositional(const PositFileDesc &file_desc);
bool Parse(int argc, char *argv[], PrgConfigBase &conf);
......
Supports Markdown
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