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

nnfencode program options

parent dfa11a29
......@@ -8,197 +8,134 @@
#include <array>
#include <csignal>
#include <cxxopts.hpp>
#include <iostream>
#include "cardinal.h"
#include "dnnf.h"
#include "dnnf_enc.h"
#include "enum_opt.h"
#include "logstream.h"
#include "prgutil.h"
const std::string SUBool::kPrgName = "nnfencode";
const std::string SUBool::kPrgDesc =
"Construct a CNF encoding of a given (smooth) DNNF.";
const std::string kPrgHelp =
"Constructs a consistency checker (CC), domain consistent encoding (DC), "
"unit refutation complete (URC), or propagation complete (PC) encoding";
enum class ENCODING_TYPE
{
I_URC,
I_PC,
CC,
DC,
URC,
PC,
Last = PC
};
const std::array<std::string, static_cast<size_t>(SUBool::LEVEL_FUNC::Last) + 1>
level_func_names{"from_root", "from_leaves"};
const SUBool::EnumAnnotation<ENCODING_TYPE> kEncodingTypeAnnotation(
"ENCODING_TYPE",
{//
{ENCODING_TYPE::CC, "cc",
"consistency checker (CC), requires a DNNF"}, //
{ENCODING_TYPE::DC, "dc",
"domain consistent (DC) encoding, requires a smooth DNNF"}, //
{ENCODING_TYPE::URC, "urc",
"unit refutation complete (URC) encoding, requires a smooth "
"DNNF"}, //
{ENCODING_TYPE::PC, "pc",
"unit refutation complete (PC) encoding, requires a smooth "
"DNNF"}});
const ENCODING_TYPE kDefaultEncodingType = ENCODING_TYPE::CC;
const SUBool::LEVEL_FUNC kDefaultLevelFunc = SUBool::LEVEL_FUNC::FROM_LEAVES;
struct config_t
{
std::string input_file{};
std::string output_file{};
unsigned verbosity{3}; // 0 means no output
ENCODING_TYPE encoding_type{ENCODING_TYPE::I_URC};
ENCODING_TYPE encoding_type{kDefaultEncodingType};
bool final_minimize{false};
SUBool::LEVEL_FUNC level_func{SUBool::LEVEL_FUNC::FROM_LEAVES};
SUBool::LEVEL_FUNC level_func{kDefaultLevelFunc};
bool check_smooth{false};
SUBool::AmoEncoder::KIND amo_encoding{SUBool::AmoEncoder::KIND::REPR};
SUBool::ExOneEncoder::KIND exone_encoding{SUBool::ExOneEncoder::KIND::REPR};
SUBool::AmoEncoder::KIND amo_encoding{
SUBool::AmoEncoder::kDefaultGlobalKind};
SUBool::ExOneEncoder::KIND exone_encoding{
SUBool::ExOneEncoder::kDefaultGlobalKind};
};
const std::map<std::string, ENCODING_TYPE> encoding_type_names = {
{"i-urc", ENCODING_TYPE::I_URC}, {"i-pc", ENCODING_TYPE::I_PC},
{"urc", ENCODING_TYPE::URC}, {"pc", ENCODING_TYPE::PC}};
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::logs.TLog(level) << "\tverbosity: " << conf.verbosity << std::endl;
SUBool::logs.TLog(level)
<< "\tencoding_type: " << static_cast<unsigned>(conf.encoding_type)
<< 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);
kEncodingTypeAnnotation.DumpValue(
"\t", level, "encoding_type", conf.encoding_type);
SUBool::logs.DumpValue("\t", level, "final_minimize", conf.final_minimize);
SUBool::logs.TLog(level)
<< "\tlevel_func: "
<< level_func_names.at(static_cast<unsigned>(conf.level_func))
<< std::endl;
SUBool::kLevelFuncAnnotation.DumpValue(
"\t", level, "level_func", conf.level_func);
SUBool::logs.TLog(level)
<< "\tcheck_smooth: " << SUBool::bool_to_string(conf.check_smooth)
<< std::endl;
SUBool::logs.DumpValue("\t", level, "amo_encoding",
SUBool::AmoEncoder::kEncodingNames.at(
static_cast<unsigned>(conf.amo_encoding)));
SUBool::logs.DumpValue("\t", level, "exone_encoding",
SUBool::ExOneEncoder::kEncodingNames.at(
static_cast<unsigned>(conf.exone_encoding)));
SUBool::AmoEncoder::kKindAnnotation.DumpValue(
"\t", level, "amo_encoding", conf.amo_encoding);
SUBool::ExOneEncoder::kKindAnnotation.DumpValue(
"\t", level, "exone_encoding", conf.exone_encoding);
SUBool::logs.TLog(level) << "END" << std::endl;
}
ENCODING_TYPE
parse_encoding_type(const std::string &enc_type)
{
try
{
return encoding_type_names.at(enc_type);
}
catch (std::out_of_range &e)
{
throw SUBool::BadParameterException(
"parse_encoding_type", "Unknown encoding type" + enc_type);
}
}
bool
needs_smooth(ENCODING_TYPE enc_type)
{
return enc_type != ENCODING_TYPE::I_URC;
return enc_type != ENCODING_TYPE::CC;
}
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]]");
std::string encoding_type;
std::string level_func;
std::string amo_encoding;
std::string exone_encoding;
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))("e,encoding",
"Type of the encoding. "
"i-urc = input URC encoding (needs a DNNF), "
"i-pc = input PC encoding (needs a smooth DNNF), "
"urc = URC encoding (needs a smooth DNNF), "
"pc = PC encoding (needs a smooth DNNF).",
cxxopts::value<std::string>(encoding_type)
->default_value("i-urc"))("m,minimize",
"Perform minimization of the constructed encoding.",
cxxopts::value<bool>(conf.final_minimize)
->default_value("false"))("L,level-func",
"How to compute levels in case of URC or PC compilation. Possible "
"values: \"from_root\" -- compute from root, \"from_leaves\" -- "
"compute from leaves with leaves having level equalt to their "
"maximum distance from the root",
cxxopts::value<std::string>(level_func)
->default_value(level_func_names[static_cast<unsigned>(
conf.level_func)]))("S,smooth",
"Check for smoothness and make DNNF smooth before constructing "
"the "
"encoding if necessary",
cxxopts::value<bool>(conf.check_smooth)
->default_value("false"))("amo",
"Which encoding to use for the at-most-one constraint. "
"repr = use the representation, "
"seq = use the sequential encoding.",
cxxopts::value<std::string>(amo_encoding)
->default_value(
SUBool::AmoEncoder::kEncodingNames[static_cast<unsigned>(
conf.amo_encoding)]))("exactly-one",
"Which encoding to use for the exactly-one constraint. "
"repr = use the representation, "
"split = use the splitting encoding.",
cxxopts::value<std::string>(exone_encoding)
->default_value(
SUBool::ExOneEncoder::kEncodingNames[static_cast<unsigned>(
conf.exone_encoding)]));
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;
}
try
{
conf.encoding_type = parse_encoding_type(encoding_type);
conf.level_func = SUBool::enum_of_name<SUBool::LEVEL_FUNC>(
level_func, level_func_names);
conf.amo_encoding = SUBool::enum_of_name<SUBool::AmoEncoder::KIND>(
amo_encoding, SUBool::AmoEncoder::kEncodingNames);
conf.exone_encoding = SUBool::enum_of_name<SUBool::ExOneEncoder::KIND>(
exone_encoding, SUBool::ExOneEncoder::kEncodingNames);
}
catch (SUBool::BadParameterException &e)
{
SUBool::logs.TLog(0)
<< "Error parsing parameter value: " << e.what() << std::endl;
return 1;
}
}
catch (const cxxopts::OptionException &e)
config_t conf;
auto opt_encoding_type = SUBool::make_enum_option(kEncodingTypeAnnotation,
"encoding,e", "Type of the encoding.", kDefaultEncodingType);
auto opt_level_func = SUBool::make_enum_option(SUBool::kLevelFuncAnnotation,
"level-func,L",
"How to compute levels in case of construction of URC or PC encoding.",
kDefaultLevelFunc);
auto opt_amo_encoding =
SUBool::make_enum_option(SUBool::AmoEncoder::kKindAnnotation, "amo",
"Which encoding to use for the at-most-one constraint.",
SUBool::AmoEncoder::kDefaultGlobalKind);
auto opt_exone_encoding = SUBool::make_enum_option(
SUBool::ExOneEncoder::kKindAnnotation, "exactly-one",
"Which encoding to use for the exactly-one constraint.",
SUBool::ExOneEncoder::kDefaultGlobalKind);
SUBool::PrgOptions opts(true);
opts.SetHelpDesc(kPrgHelp);
opts.InputOutput(&conf.input_file, &conf.output_file);
po::options_description desc("Configuration options");
desc.add(opt_encoding_type);
desc.add(opt_level_func);
desc.add_options() //
("minimize,m", po::bool_switch(&conf.final_minimize),
"Perform minimization of the constructed encoding.") //
("smooth,S", po::bool_switch(&conf.check_smooth),
"Check for smoothness and make DNNF smooth before constructing the "
"encoding if necessary");
desc.add(opt_amo_encoding);
desc.add(opt_exone_encoding);
opts.Add(desc);
if (!opts.Parse(argc, argv)
|| !opt_encoding_type.GetValue(conf.encoding_type)
|| !opt_level_func.GetValue(conf.level_func)
|| !opt_amo_encoding.GetValue(conf.amo_encoding)
|| !opt_exone_encoding.GetValue(conf.exone_encoding))
{
std::cerr << "Error parsing options: " << e.what() << std::endl;
return 1;
return {};
}
return 0;
return conf;
}
std::unique_ptr<SUBool::CNFEncoding>
......@@ -206,13 +143,13 @@ construct_encoding(const SUBool::Nnf &nnf, const config_t &conf)
{
switch (conf.encoding_type)
{
case ENCODING_TYPE::I_URC:
case ENCODING_TYPE::CC:
{
return std::unique_ptr<SUBool::CNFEncoding>(
new SUBool::URCEncoding(SUBool::DnnfInputUrcEncoder::URCEncode(nnf)));
}
break;
case ENCODING_TYPE::I_PC:
case ENCODING_TYPE::DC:
{
return std::unique_ptr<SUBool::CNFEncoding>(new SUBool::PCEncoding(
SUBool::SmoothDnnfInputPcEncoder::PCEncode(nnf)));
......@@ -246,30 +183,28 @@ 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);
SUBool::AmoEncoder::sGlobalKind = conf.amo_encoding;
SUBool::ExOneEncoder::sGlobalKind = conf.exone_encoding;
auto nnf = SUBool::input_or_die<SUBool::Nnf>(conf.input_file, SUBool::logs);
if (needs_smooth(conf.encoding_type) && conf.check_smooth)
dump_config(*conf, 3);
SUBool::AmoEncoder::sGlobalKind = conf->amo_encoding;
SUBool::ExOneEncoder::sGlobalKind = conf->exone_encoding;
auto nnf = SUBool::input_or_die<SUBool::Nnf>(conf->input_file, SUBool::logs);
if (needs_smooth(conf->encoding_type) && conf->check_smooth)
{
SUBool::logs.TLog(3) << "Checking smoothness" << std::endl;
nnf = SUBool::nnf_smooth(std::move(nnf));
}
auto enc = construct_encoding(nnf, conf);
if (conf.final_minimize)
auto enc = construct_encoding(nnf, *conf);
if (conf->final_minimize)
{
enc->Minimize();
}
SUBool::output(conf.output_file, *enc);
SUBool::output(conf->output_file, *enc);
return 0;
}
......@@ -9,21 +9,28 @@
#include "cardinal.h"
SUBool::AmoEncoder::KIND SUBool::AmoEncoder::sGlobalKind =
SUBool::AmoEncoder::kGlobalDefaultKind;
SUBool::AmoEncoder::kDefaultGlobalKind;
SUBool::ExOneEncoder::KIND SUBool::ExOneEncoder::sGlobalKind =
SUBool::ExOneEncoder::kGlobalDefaultKind;
SUBool::ExOneEncoder::kDefaultGlobalKind;
const std::array<std::string,
static_cast<size_t>(SUBool::AmoEncoder::KIND::Last) + 1>
SUBool::AmoEncoder::kEncodingNames{"repr", "seq"};
const std::array<std::string,
static_cast<size_t>(SUBool::ExOneEncoder::KIND::Last) + 1>
SUBool::ExOneEncoder::kEncodingNames{"repr", "split"};
const SUBool::EnumAnnotation<SUBool::AmoEncoder::KIND>
SUBool::AmoEncoder::kKindAnnotation("AmoEncoder::KIND",
{
//
{KIND::REPR, "repr", "the canonical representation"}, //
{KIND::SEQ, "seq", "the sequential encoding"},
});
const SUBool::EnumAnnotation<SUBool::ExOneEncoder::KIND>
SUBool::ExOneEncoder::kKindAnnotation("ExOneEncoder::KIND",
{
//
{KIND::REPR, "repr", "the canonical representation"}, //
{KIND::SPLIT, "split", "the splitting encoding"} //
});
void
SUBool::amo_representation(const std::vector<Literal> &inputs,
std::vector<Clause> &clauses)
SUBool::amo_representation(
const std::vector<Literal> &inputs, std::vector<Clause> &clauses)
{
for (unsigned a = 0; a < inputs.size(); ++a)
{
......@@ -36,38 +43,38 @@ SUBool::amo_representation(const std::vector<Literal> &inputs,
}
void
SUBool::exone_representation(const std::vector<Literal> &inputs,
std::vector<Clause> &clauses)
SUBool::exone_representation(
const std::vector<Literal> &inputs, std::vector<Clause> &clauses)
{
amo_representation(inputs, clauses);
clauses.emplace_back(inputs);
}
std::vector<SUBool::Clause>
SUBool::ConstraintEncoder::Encode(const std::vector<Literal> &inputs,
std::vector<Clause> clauses)
SUBool::ConstraintEncoder::Encode(
const std::vector<Literal> &inputs, std::vector<Clause> clauses)
{
EncodeAppend(inputs, clauses);
return clauses;
}
void
SUBool::AmoRepresentation::EncodeAppend(const std::vector<Literal> &inputs,
std::vector<Clause> &clauses)
SUBool::AmoRepresentation::EncodeAppend(
const std::vector<Literal> &inputs, std::vector<Clause> &clauses)
{
amo_representation(inputs, clauses);
}
void
SUBool::ExOneRepresentation::EncodeAppend(const std::vector<Literal> &inputs,
std::vector<Clause> &clauses)
SUBool::ExOneRepresentation::EncodeAppend(
const std::vector<Literal> &inputs, std::vector<Clause> &clauses)
{
exone_representation(inputs, clauses);
}
void
SUBool::AmoSequential::EncodeAppend(const std::vector<Literal> &inputs,
std::vector<Clause> &clauses)
SUBool::AmoSequential::EncodeAppend(
const std::vector<Literal> &inputs, std::vector<Clause> &clauses)
{
if (inputs.size() <= mReprLimit)
{
......@@ -79,8 +86,7 @@ SUBool::AmoSequential::EncodeAppend(const std::vector<Literal> &inputs,
void
SUBool::AmoSequential::InnerEncode(std::vector<Literal> inputs,
std::vector<Clause> &clauses,
unsigned next_aux_index)
std::vector<Clause> &clauses, unsigned next_aux_index)
{
if (inputs.size() <= mBaseSize)
{
......@@ -98,8 +104,8 @@ SUBool::AmoSequential::InnerEncode(std::vector<Literal> inputs,
}
void
SUBool::ExOneSplitting::EncodeAppend(const std::vector<Literal> &inputs,
std::vector<Clause> &clauses)
SUBool::ExOneSplitting::EncodeAppend(
const std::vector<Literal> &inputs, std::vector<Clause> &clauses)
{
if (inputs.size() <= mReprLimit)
{
......@@ -112,8 +118,7 @@ SUBool::ExOneSplitting::EncodeAppend(const std::vector<Literal> &inputs,
void
SUBool::ExOneSplitting::InnerEncode(std::vector<Literal> inputs,
std::vector<Clause> &clauses,
unsigned &next_aux_index)
std::vector<Clause> &clauses, unsigned &next_aux_index)
{
if (inputs.size() <= mBaseSize)
{
......@@ -165,8 +170,8 @@ SUBool::AmoEncoder::NewEncoder(KIND kind, VarStore &var_store)
case KIND::SEQ:
return std::unique_ptr<AmoEncoder>(new AmoSequential(var_store));
default:
throw BadParameterException("AmoEncoder::NewEncoder",
"Uknown encoding kind");
throw BadParameterException(
"AmoEncoder::NewEncoder", "Uknown encoding kind");
};
}
......@@ -180,8 +185,8 @@ SUBool::ExOneEncoder::NewEncoder(KIND kind, VarStore &var_store)
case KIND::SPLIT:
return std::unique_ptr<ExOneEncoder>(new ExOneSplitting(var_store));
default:
throw BadParameterException("ExOneEncoder::NewEncoder",
"Uknown encoding kind");
throw BadParameterException(
"ExOneEncoder::NewEncoder", "Uknown encoding kind");
};
}
......@@ -193,30 +198,30 @@ SUBool::AmoRepresentation::Size(const size_t input_size, unsigned max_input_var)
}
SUBool::NFSize
SUBool::AmoRepresentation::CountClauses(const size_t input_size,
unsigned max_input_var) const
SUBool::AmoRepresentation::CountClauses(
const size_t input_size, unsigned max_input_var) const
{
return Size(input_size, max_input_var);
}
SUBool::NFSize
SUBool::ExOneRepresentation::Size(const size_t input_size,
unsigned max_input_var)
SUBool::ExOneRepresentation::Size(
const size_t input_size, unsigned max_input_var)
{
auto c = (input_size * (input_size - 1)) / 2;
return NFSize{max_input_var, c + 1, 2 * c + input_size};
}
SUBool::NFSize
SUBool::ExOneRepresentation::CountClauses(const size_t input_size,
unsigned max_input_var) const
SUBool::ExOneRepresentation::CountClauses(
const size_t input_size, unsigned max_input_var) const
{
return Size(input_size, max_input_var);
}
SUBool::NFSize
SUBool::AmoSequential::CountClauses(const size_t input_size,
unsigned max_input_var) const
SUBool::AmoSequential::CountClauses(
const size_t input_size, unsigned max_input_var) const
{
if (input_size <= mReprLimit || input_size <= mBaseSize)
{
......@@ -228,8 +233,8 @@ SUBool::AmoSequential::CountClauses(const size_t input_size,
}
SUBool::NFSize
SUBool::ExOneSplitting::CountClauses(const size_t input_size,
unsigned max_input_var) const
SUBool::ExOneSplitting::CountClauses(
const size_t input_size, unsigned max_input_var) const
{
if (input_size <= mReprLimit)
{
......
......@@ -13,6 +13,7 @@
#include <memory>
#include <vector>
#include "enum.h"
#include "nfliteralset.h"
#include "normalform.h"
#include "varstore.h"
......@@ -24,16 +25,15 @@ namespace SUBool
public:
virtual ~ConstraintEncoder() = default;
virtual std::vector<Clause>
Encode(const std::vector<Literal> &inputs,
std::vector<Clause> clauses = std::vector<Clause>());
virtual void EncodeAppend(const std::vector<Literal> &inputs,
std::vector<Clause> &clauses) = 0;
virtual std::vector<Clause> Encode(const std::vector<Literal> &inputs,
std::vector<Clause> clauses = std::vector<Clause>());
virtual void EncodeAppend(
const std::vector<Literal> &inputs, std::vector<Clause> &clauses) = 0;
virtual std::string Description() const = 0;
virtual NFSize CountClauses(const size_t input_size,
unsigned max_input_var = 0) const = 0;
virtual NFSize CountClauses(
const size_t input_size, unsigned max_input_var = 0) const = 0;
std::vector<Clause>
operator()(const std::vector<Literal> &inputs)
......@@ -52,13 +52,12 @@ namespace SUBool
Last = SEQ
};
static const std::array<std::string, static_cast<size_t>(KIND::Last) + 1>
kEncodingNames;
static const EnumAnnotation<KIND> kKindAnnotation;
static const KIND kGlobalDefaultKind{KIND::REPR};
inline static const KIND kDefaultGlobalKind{KIND::REPR};
static KIND sGlobalKind;
static std::unique_ptr<AmoEncoder> NewEncoder(KIND kind,
VarStore &var_store);
static std::unique_ptr<AmoEncoder> NewEncoder(
KIND kind, VarStore &var_store);
static std::unique_ptr<AmoEncoder>
NewGlobalEncoder(VarStore &var_store)
{
......@@ -72,9 +71,9 @@ namespace SUBool
virtual std::string Description() const override;
virtual void EncodeAppend(const std::vector<Literal> &inputs,
std::vector<Clause> &clauses) override;
virtual NFSize CountClauses(const size_t input_size,
unsigned max_input_var = 0) const override;
std::vector<Clause> &clauses) override;
virtual NFSize CountClauses(
const size_t input_size, unsigned max_input_var = 0) const override;
static NFSize Size(const size_t input_size, unsigned max_input_var);
};
......@@ -89,12 +88,11 @@ namespace SUBool
Last = SPLIT
};
static const std::array<std::string, static_cast<size_t>(KIND::Last) + 1>
kEncodingNames;
static const KIND kGlobalDefaultKind{KIND::REPR};
static const EnumAnnotation<KIND> kKindAnnotation;
inline static const KIND kDefaultGlobalKind{KIND::REPR};
static KIND sGlobalKind;
static std::unique_ptr<ExOneEncoder> NewEncoder(KIND kind,
VarStore &var_store);
static std::unique_ptr<ExOneEncoder> NewEncoder(
KIND kind, VarStore &var_store);
static std::unique_ptr<ExOneEncoder>
NewGlobalEncoder(VarStore &var_store)
{
......@@ -107,9 +105,9 @@ namespace SUBool
public:
virtual std::string Description() const override;
virtual void EncodeAppend(const std::vector<Literal> &inputs,
std::vector<Clause> &clauses) override;