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

pcminimize program options

parent e3a41c34
......@@ -119,8 +119,8 @@ dump_config(const config_t &conf, unsigned level)
<< "\toutput_file: " << conf.output_file << std::endl;
SUBool::logs.TLog(level)
<< "\tminimize: " << SUBool::bool_to_string(conf.minimize) << std::endl;
SUBool::dump_enum_value("\t", level, "minimize_method",
conf.comp_base_config.minimize_method, SUBool::kMinimizeMethodNames);
SUBool::kMinimizeMethodAnnotation.DumpValue(
"\t", level, "minimize_method", conf.comp_base_config.minimize_method);
SUBool::logs.TLog(level)
<< "\talgorithm: "
<< algorithm_names.at(static_cast<unsigned>(conf.algorithm))
......@@ -335,9 +335,8 @@ parse_arguments(int argc, char *argv[], config_t &conf)
"minimized, but it can be significantly smaller than in case of "
"simple_incremental.",
cxxopts::value<std::string>(minimize_method)
->default_value(
SUBool::kMinimizeMethodNames.at(static_cast<unsigned>(
conf.comp_base_config.minimize_method))))("a,algorithm",
->default_value(SUBool::kMinimizeMethodAnnotation.Name(
conf.comp_base_config.minimize_method)))("a,algorithm",
"The compilation algorithm. "
"'incremental' -- a heuristic algorithm based on incremental "
"adding "
......@@ -573,8 +572,7 @@ parse_arguments(int argc, char *argv[], config_t &conf)
conf.exone_encoding =
SUBool::ExOneEncoder::kKindAnnotation.Parse(exone_encoding);
conf.comp_base_config.minimize_method =
SUBool::enum_of_name<SUBool::MINIMIZE_METHOD>(
minimize_method, SUBool::kMinimizeMethodNames);
SUBool::kMinimizeMethodAnnotation.Parse(minimize_method);
conf.comp_base_config.impl_system =
SUBool::enum_of_name<SUBool::LIT_IMPL_SYSTEM>(
impl_system, SUBool::kImplSystemNames);
......
......@@ -15,12 +15,11 @@
#include <future>
#include <iostream>
#include <cxxopts.hpp>
#include "cardinal.h"
#include "cnfcompress.h"
#include "logstream.h"
#include "normalform.h"
#include "pc_opt.h"
#include "pccomp.h"
#include "pcenc.h"
#include "pclearncomp.h"
......@@ -43,7 +42,6 @@ struct config_t
SUBool::MINIMIZE_METHOD minimize_method{SUBool::MINIMIZE_METHOD::FULL};
bool backbones{false}; // Whether backbones should be propagated
bool prime{false}; // make prime before minimization
unsigned verbosity{3}; // 0 means no output
double timeout{-1.0};
};
......@@ -51,107 +49,44 @@ void
dump_config(const config_t &conf, unsigned level)
{
SUBool::logs.TLog(level) << "Configuration:" << std::endl;
SUBool::logs.TLog(level) << "\tinput_file: " << conf.input_file << std::endl;
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::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;
SUBool::logs.TLog(level) << "\ttimeout: " << conf.timeout << std::endl;
SUBool::logs.DumpVerbosity("\t", level);
SUBool::logs.DumpValue("\t", level, "input_file", conf.input_file);
SUBool::logs.DumpValue("\t", level, "output_file", conf.output_file);
SUBool::kMinimizeMethodAnnotation.DumpValue(
"\t", level, "minimize_method", conf.minimize_method);
SUBool::logs.DumpValue("\t", level, "backbones", conf.backbones);
SUBool::logs.DumpValue("\t", level, "prime", conf.prime);
SUBool::logs.DumpValue("\t", level, "timeout", conf.timeout);
SUBool::logs.TLog(level) << "END" << 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("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",
"Minimization method. Possible values: "
"full -- full minimization (with the full CNF) "
"simple_incremental -- sort in increasing order by sizes and then "
"add nonabsorbed clauses in this sequence, starting with the empty "
"CNF, the result is not necessarily fully minimized. "
"full_incremental -- same as simple_incremental, in addition, now "
"after a specific length of clauses is processed, they are "
"reprocessed again as in full minimization. Only after then longer "
"clauses are considered. The result is not necessarily fully "
"minimized, but it can be significantly smaller than in case of "
"simple_incremental.",
cxxopts::value<std::string>(minimize_method)
->default_value(SUBool::kMinimizeMethodNames.at(
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",
"Make CNF prime before running the minimization (this implies using "
"backbone propagation)",
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",
"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",
"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;
return 1;
}
if (result.count("version"))
{
SUBool::print_version(std::cout);
std::cout << 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;
}
try
{
conf.minimize_method = SUBool::enum_of_name<SUBool::MINIMIZE_METHOD>(
minimize_method, SUBool::kMinimizeMethodNames);
}
catch (SUBool::BadParameterException &e)
{
std::cerr << "Error parsing parameter values: " << e.what()
<< std::endl;
return 1;
}
conf.backbones |= conf.prime;
}
catch (const cxxopts::OptionException &e)
{
std::cerr << "Error parsing options: " << e.what() << std::endl;
return 1;
}
return 0;
config_t conf;
auto minimize_method = SUBool::minimize_method_opt();
SUBool::PrgOptions opts(true);
opts.InputOutput(&conf.input_file, &conf.output_file);
po::options_description desc("Configuration options");
desc.add(minimize_method);
desc.add_options() //
("backbones,B", po::bool_switch(&conf.backbones),
"Use backbone propagation before the minimization is executed") //
("prime,p", po::bool_switch(&conf.prime),
"Make CNF prime before running the minimization (this implies using "
"backbone propagation)") //
("timeout,t", po::value<double>(&conf.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.");
opts.Add(desc);
if (!opts.Parse(argc, argv)
|| !minimize_method.GetValue(conf.minimize_method))
{
return {};
}
conf.backbones |= conf.prime;
return conf;
}
int
......@@ -291,15 +226,15 @@ terminate(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 {};
}
SUBool::logs.mVerbLevel = conf.verbosity;
SUBool::logs.TLog(3) << "PCMinimize" << SUBool::kVersionInfo << std::endl;
dump_config(*conf, 3);
SUBool::CNF cnf;
r = input(conf, &cnf);
auto r = input(*conf, &cnf);
if (r != 0)
{
return r;
......@@ -309,11 +244,6 @@ main(int argc, char *argv[])
std::signal(SIGQUIT, terminate);
std::signal(SIGINT, terminate);
SUBool::logs.TLog(SUBool::LogStream::LOG_LEVEL::MINLINES)
<< "PCMinimize" << SUBool::kVersionInfo << std::endl;
dump_config(
conf, static_cast<unsigned>(SUBool::LogStream::LOG_LEVEL::MINLINES));
auto ret = minimize(conf, std::move(cnf));
auto ret = minimize(*conf, std::move(cnf));
return ret;
}
......@@ -11,10 +11,24 @@
#include "cnfutil.h"
#include "logstream.h"
const std::array<std::string,
static_cast<size_t>(SUBool::MINIMIZE_METHOD::Last) + 1>
SUBool::kMinimizeMethodNames{"full", "simple_incremental",
"full_incremental"};
const SUBool::EnumAnnotation<SUBool::MINIMIZE_METHOD>
SUBool::kMinimizeMethodAnnotation("MINIMIZE_METHOD",
{
//
{SUBool::MINIMIZE_METHOD::FULL, "full", "full minimization"}, //
{SUBool::MINIMIZE_METHOD::SIMPLE_INCREMENTAL, "simple_incremental",
"sort the clauses in increasing order by sizes and then add "
"nonabsorbed clauses in this sequence, starting with the empty "
"CNF, the result is not necessarily fully minimized."}, //
{SUBool::MINIMIZE_METHOD::FULL_INCREMENTAL, "full_incremental",
"same as simple_incremental, in addition, now after a specific "
"length of clauses is processed, they are reprocessed again as "
"in "
"full minimization. Only after then longer clauses are "
"considered. "
"The result is not necessarily fully minimized, but it can be "
"significantly smaller than in case of simple_incremental."} //
});
bool
SUBool::OneProve::IsOneProvable(const Clause &clause)
......@@ -47,8 +61,8 @@ SUBool::OneProve::AllEmpoweredLiterals(const Clause &clause)
}
std::optional<std::vector<SUBool::Literal>>
SUBool::OneProve::CollectEmpoweredLiterals(const Clause &clause,
bool collect_all)
SUBool::OneProve::CollectEmpoweredLiterals(
const Clause &clause, bool collect_all)
{
auto alpha = clause_falsifying(clause, mUP.MaxVariable());
// Check if the clause is 1-provable
......@@ -109,8 +123,8 @@ SUBool::OneProve::Propagate(const PartialAssignment &alpha)
}
SUBool::Clause
SUBool::OneProve::MinOneProvableSubClause(const Clause &clause,
unsigned ignore_var)
SUBool::OneProve::MinOneProvableSubClause(
const Clause &clause, unsigned ignore_var)
{
auto alpha = clause_falsifying(clause, mUP.MaxVariable());
if (mUP.Propagate(alpha, nullptr) < 0)
......@@ -142,8 +156,8 @@ SUBool::op_is_empowering(const CNF &cnf, const Clause &clause)
}
bool
SUBool::op_is_empowering_with_mask(const CNF &cnf, const Clause &clause,
const std::vector<bool> &mask)
SUBool::op_is_empowering_with_mask(
const CNF &cnf, const Clause &clause, const std::vector<bool> &mask)
{
OneProve op(&cnf, [&mask](unsigned i) { return mask[i]; });
return op.IsEmpowering(clause);
......@@ -185,8 +199,7 @@ namespace SUBool
{
unsigned
reprocess(const CNF &cnf, OneProve &op, std::vector<bool> &mask,
const unsigned size, const unsigned clause_size,
std::queue<unsigned> &q)
const unsigned size, const unsigned clause_size, std::queue<unsigned> &q)
{
unsigned new_size = size;
logs.TLog(3) << "reprocessing clause size" << clause_size
......@@ -276,7 +289,7 @@ SUBool::empower_minimize(CNF cnf, MINIMIZE_METHOD method, size_t log_step)
case MINIMIZE_METHOD::FULL_INCREMENTAL:
return empower_minimize_inc(std::move(cnf), true, log_step);
default:
throw BadParameterException("empower_minimize",
"Bad minimization method");
throw BadParameterException(
"empower_minimize", "Bad minimization method");
};
}
......@@ -12,6 +12,7 @@
#include <array>
#include "enum.h"
#include "logstream.h"
#include "unitprop.h"
#include "util.h"
......@@ -62,20 +63,20 @@ namespace SUBool
bool IsOneProvable(const Clause &clause);
bool IsEmpowering(const Clause &clause);
// Returns an empty clause if the clause is not 1-provable
Clause MinOneProvableSubClause(const Clause &clause,
unsigned ignore_var = 0);
std::optional<std::vector<Literal>>
AllEmpoweredLiterals(const Clause &clause);
Clause MinOneProvableSubClause(
const Clause &clause, unsigned ignore_var = 0);
std::optional<std::vector<Literal>> AllEmpoweredLiterals(
const Clause &clause);
std::optional<Literal> EmpoweredLiteral(const Clause &clause);
std::optional<std::vector<Literal>>
CollectEmpoweredLiterals(const Clause &clause, bool collect_all);
std::optional<PartialAssignment>
Propagate(const PartialAssignment &alpha);
std::optional<std::vector<Literal>> CollectEmpoweredLiterals(
const Clause &clause, bool collect_all);
std::optional<PartialAssignment> Propagate(
const PartialAssignment &alpha);
};
bool op_is_empowering(const CNF &cnf, const Clause &clause);
bool op_is_empowering_with_mask(const CNF &cnf, const Clause &clause,
const std::vector<bool> &mask);
bool op_is_empowering_with_mask(
const CNF &cnf, const Clause &clause, const std::vector<bool> &mask);
bool is_one_provable(const CNF &cnf, const Clause &clause);
......@@ -84,8 +85,8 @@ namespace SUBool
inline CNF
up_prime_cnf(CNF cnf)
{
return up_prime_cnf_with_ignore(std::move(cnf),
[](auto) { return false; });
return up_prime_cnf_with_ignore(
std::move(cnf), [](auto) { return false; });
}
enum class MINIMIZE_METHOD
......@@ -96,9 +97,8 @@ namespace SUBool
Last = FULL_INCREMENTAL
};
extern const std::array<std::string,
static_cast<size_t>(MINIMIZE_METHOD::Last) + 1>
kMinimizeMethodNames;
extern const EnumAnnotation<MINIMIZE_METHOD> kMinimizeMethodAnnotation;
inline const MINIMIZE_METHOD kDefaultMinimizeMethod = MINIMIZE_METHOD::FULL;
CNF empower_minimize_full(CNF cnf, size_t log_step = 0);
CNF empower_minimize_inc(CNF cnf, bool reprocessing, size_t log_step = 0);
......
/*
* Project SUBool
* Petr Kucera, 2021
*/
/**@file pc_opt.h
* Common options of programs related to propagation completeness.
*/
#include "pc_opt.h"
auto
SUBool::minimize_method_opt() -> EnumOption<MINIMIZE_METHOD>
{
return make_enum_option(kMinimizeMethodAnnotation, "minimize-method",
"Minimization method", kDefaultMinimizeMethod);
}
/*
* Project SUBool
* Petr Kucera, 2021
*/
/**@file pc_opt.h
* Common options of programs related to propagation completeness.
*/
#ifndef __PC_OPT_H
#define __PC_OPT_H
#include "empower.h"
#include "enum_opt.h"
namespace SUBool
{
// "Minimization method", "minimize-method"
EnumOption<MINIMIZE_METHOD> minimize_method_opt();
} // namespace SUBool
#endif
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