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

pccheck options

parent 9ced1dc5
......@@ -16,6 +16,7 @@
#include <iostream>
#include "cardinal.h"
#include "cardinal_opt.h"
#include "cnfcompress.h"
#include "logstream.h"
#include "normalform.h"
......@@ -48,8 +49,8 @@ struct config_t
SUBool::AbsEncoder::AbsConfig enc_conf{};
SUBool::AbsCheckerSAT::Timeouts timeouts{};
SUBool::LIT_IMPL_SYSTEM impl_system{SUBool::LIT_IMPL_SYSTEM::Default};
SUBool::PCCheckGoalOptions::GOAL goal{
SUBool::PCCheckGoalOptions::kDefaultGoal};
SUBool::PCCheckGeneralOptions::GOAL goal{
SUBool::PCCheckGeneralOptions::kDefaultGoal};
SUBool::AmoEncoder::KIND amo_encoding{SUBool::AmoEncoder::KIND::REPR};
SUBool::ExOneEncoder::KIND exone_encoding{SUBool::ExOneEncoder::KIND::REPR};
SUBool::SOLVER_TYPE solver_type{SUBool::SOLVER_TYPE::GLUCOSE};
......@@ -78,7 +79,7 @@ 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.DumpVerbosity("\t", level);
SUBool::PCCheckGoalOptions::kGoalAnnotation.DumpValue(
SUBool::PCCheckGeneralOptions::kGoalAnnotation.DumpValue(
"\t", level, "goal", conf.goal);
SUBool::logs.TLog(level)
<< "\tencode_only: " << SUBool::bool_to_string(conf.encode_only)
......@@ -109,37 +110,6 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level) << "END" << std::endl;
}
std::vector<std::string> log_enc_opt_strings = {"amf", "cex", "flm", "cml"};
bool
parse_log_enc_opts(
const std::string &opt_string, SUBool::UPEncLogarithmic::Config &conf)
{
std::vector<bool> opt_values(log_enc_opt_strings.size(), false);
size_t start = 0;
size_t end = 0;
if (!opt_string.empty())
{
while (start != std::string::npos)
{
end = opt_string.find_first_of(',', start);
auto i = std::find(log_enc_opt_strings.begin(),
log_enc_opt_strings.end(), opt_string.substr(start, end - start));
if (i == log_enc_opt_strings.end())
{
return false;
}
opt_values[i - log_enc_opt_strings.begin()] = true;
start = end + static_cast<size_t>(end < std::string::npos);
}
}
conf.add_amo_on_fire_vars = opt_values[0];
conf.add_compare_exclusivity = opt_values[1];
conf.add_force_linear_order_on_max_level = opt_values[2];
conf.contradiction_has_max_level = opt_values[3];
return true;
}
std::optional<config_t>
parse_arguments(int argc, char *argv[])
{
......@@ -147,18 +117,34 @@ parse_arguments(int argc, char *argv[])
SUBool::PrgOptions opts(true);
opts.SetHelpDesc(prg_help);
opts.SinglePositional({&conf.input_file, "input"});
auto goal_opts = opts.MakeOptionsGroup<SUBool::PCCheckGoalOptions>();
auto general_opts = opts.MakeOptionsGroup<SUBool::PCCheckGeneralOptions>();
auto solver_opts = opts.MakeOptionsGroup<SUBool::PCSolverOptions>();
auto empower_opts = opts.MakeOptionsGroup<SUBool::PCEmpowerOptions>();
auto oneprove_opts = opts.MakeOptionsGroup<SUBool::PCOneProveOptions>();
auto timeout_opts = opts.MakeOptionsGroup<SUBool::PCTimeoutsOptions>(false);
auto cardinal_opt_group =
opts.MakeOptionsGroup<SUBool::CardinalOptionsGroup>();
if (!opts.Parse(argc, argv))
{
return {};
}
conf.goal = goal_opts->Goal();
if (goal_opts->EncodeFile())
conf.goal = general_opts->Goal();
if (general_opts->EncodeFile())
{
conf.encode_only = true;
conf.encoding_file = *(goal_opts->EncodeFile());
conf.encoding_file = *(general_opts->EncodeFile());
}
conf.enc_conf.use_backmap = goal_opts->Dump();
conf.enc_conf.use_backmap = general_opts->Dump();
conf.no_up_backbones = general_opts->NoUPBackbones();
conf.solver_type = solver_opts->SolverType();
conf.up_empower = empower_opts->Empower();
conf.enc_conf.up_one_prove = oneprove_opts->OneProve();
conf.enc_conf.up_level_bound = oneprove_opts->UPLevelBound();
conf.enc_conf.log_conf = oneprove_opts->EncLogarithmicConf();
conf.impl_system = oneprove_opts->ImplSystem();
conf.timeouts = timeout_opts->EmpTimeouts();
conf.amo_encoding = cardinal_opt_group->AmoEncoding();
conf.exone_encoding = cardinal_opt_group->ExOneEncoding();
return conf;
#if 0
try
......@@ -489,7 +475,7 @@ empower(const config_t &conf, SUBool::CompHypothesis &hyp,
return 1;
}
SUBool::logs.TLog(1) << "No empowering implicate found, formula is "
<< SUBool::PCCheckGoalOptions::kGoalAnnotation.Name(
<< SUBool::PCCheckGeneralOptions::kGoalAnnotation.Name(
conf.goal)
<< " complete" << std::endl;
return 0;
......@@ -528,9 +514,9 @@ checker_sat(const config_t &conf)
{
switch (conf.goal)
{
case SUBool::PCCheckGoalOptions::GOAL::PC:
case SUBool::PCCheckGeneralOptions::GOAL::PC:
return pc_checker_sat(conf);
case SUBool::PCCheckGoalOptions::GOAL::URC:
case SUBool::PCCheckGeneralOptions::GOAL::URC:
return urc_checker_sat(conf);
default:
throw SUBool::BadParameterException("checker_sat", "Unknown goal");
......
......@@ -30,8 +30,8 @@ const SUBool::EnumAnnotation<SUBool::PCCompAlgorithmOptions::ALGORITHM>
"equivalence and closure queries (Arias et al. 2015). The goal "
"is an equivalent PC formula."}});
const SUBool::EnumAnnotation<SUBool::PCCheckGoalOptions::GOAL>
SUBool::PCCheckGoalOptions::kGoalAnnotation(
const SUBool::EnumAnnotation<SUBool::PCCheckGeneralOptions::GOAL>
SUBool::PCCheckGeneralOptions::kGoalAnnotation(
"GOAL", {
//
{GOAL::PC, "pc",
......@@ -250,15 +250,20 @@ SUBool::PCMinimizationOptions::GetValues()
return mMinimizeMethodOption.GetValue(mMinimizeMethod);
}
SUBool::PCTimeoutsOptions::PCTimeoutsOptions() : OptionsGroup("Timeouts")
SUBool::PCTimeoutsOptions::PCTimeoutsOptions(bool include_timeout)
: OptionsGroup("Timeouts")
{
if (include_timeout)
{
AddOptions() //
("timeout,t",
po::value<long double>(&mTimeout)->default_value(-1.0l, "-1.0"),
"Total timeout for the computation in seconds as a fractional "
"number. After this amount of seconds, the process finishes. "
"Value t<=0.0 means that the computation is not bounded by a "
"timeout. The timer uses CLOCK_REALTIME");
}
AddOptions() //
("timeout,t",
po::value<long double>(&mTimeout)->default_value(-1.0l, "-1.0"),
"Total timeout for the computation in seconds as a fractional "
"number. After this amount of seconds, the process finishes. Value "
"t<=0.0 means that the computation is not bounded by a timeout. The "
"timer uses CLOCK_REALTIME") //
("emp-timeout",
po::value<long double>(&mEmpTimeouts.timeout)
->default_value(-1.0l, "-1.0"),
......@@ -294,7 +299,7 @@ SUBool::PCTimeoutsOptions::GetValues()
return true;
}
SUBool::PCCheckGoalOptions::PCCheckGoalOptions()
SUBool::PCCheckGeneralOptions::PCCheckGeneralOptions()
: OptionsGroup("General Options"),
mGoalOption(
kGoalAnnotation, "goal,g", "What should be checked", kDefaultGoal)
......@@ -305,11 +310,15 @@ SUBool::PCCheckGoalOptions::PCCheckGoalOptions()
"Do not check, just write the encoding to the given file.") //
("dump,d", po::bool_switch(&mDump),
"Dump the names of variables into the output file (given with -e "
"option).");
"option).") // i
("no-up-backbones,n", po::bool_switch(&mNoUPBackbones),
"Do NOT perform propagation of literals which can be derived by "
"unit propagation from the input formula. This is useful for "
"checking the construction of an encoding.");
}
bool
SUBool::PCCheckGoalOptions::GetValues()
SUBool::PCCheckGeneralOptions::GetValues()
{
return true;
}
......
......@@ -215,7 +215,7 @@ namespace SUBool
long double mTimeout{-1.0};
public:
PCTimeoutsOptions();
PCTimeoutsOptions(bool include_timeout = true);
virtual bool GetValues() override;
......@@ -223,7 +223,7 @@ namespace SUBool
long double Timeout() const;
};
class PCCheckGoalOptions : public OptionsGroup
class PCCheckGeneralOptions : public OptionsGroup
{
public:
enum class GOAL
......@@ -240,15 +240,17 @@ namespace SUBool
GOAL mGoal{kDefaultGoal};
bool mDump{false};
boost::optional<std::string> mEncodeFile{};
bool mNoUPBackbones;
public:
PCCheckGoalOptions();
PCCheckGeneralOptions();
virtual bool GetValues() override;
GOAL Goal() const;
bool Dump() const;
const boost::optional<std::string> &EncodeFile() const;
bool NoUPBackbones() const;
};
} // namespace SUBool
......@@ -379,22 +381,28 @@ SUBool::PCTimeoutsOptions::Timeout() const
return mTimeout;
}
inline SUBool::PCCheckGoalOptions::GOAL
SUBool::PCCheckGoalOptions::Goal() const
inline SUBool::PCCheckGeneralOptions::GOAL
SUBool::PCCheckGeneralOptions::Goal() const
{
return mGoal;
}
inline bool
SUBool::PCCheckGoalOptions::Dump() const
SUBool::PCCheckGeneralOptions::Dump() const
{
return mDump;
}
inline const boost::optional<std::string> &
SUBool::PCCheckGoalOptions::EncodeFile() const
SUBool::PCCheckGeneralOptions::EncodeFile() const
{
return mEncodeFile;
}
inline bool
SUBool::PCCheckGeneralOptions::NoUPBackbones() const
{
return mNoUPBackbones;
}
#endif
......@@ -186,7 +186,8 @@ namespace SUBool
po::options_description_easy_init AddOptions();
void Add(const po::options_description &desc);
void AddOptionsGroup(std::shared_ptr<OptionsGroup> opt_group);
template <class T> std::shared_ptr<T> MakeOptionsGroup();
template <typename T, typename... Args>
std::shared_ptr<T> MakeOptionsGroup(Args &&...args);
bool HasValue(const std::string &opt_name) const;
};
......@@ -248,11 +249,11 @@ SUBool::PrgOptions::HasValue(const std::string &opt_name) const
return mVM.count(opt_name);
}
template <class T>
template <typename T, typename... Args>
std::shared_ptr<T>
SUBool::PrgOptions::MakeOptionsGroup()
SUBool::PrgOptions::MakeOptionsGroup(Args &&...args)
{
auto opt_group = std::make_shared<T>();
auto opt_group = std::make_shared<T>(std::forward<Args>(args)...);
AddOptionsGroup(opt_group);
return opt_group;
}
......
......@@ -10,9 +10,6 @@ Goal
output file
-d, --dump Back mapping of variables (names) are used
wherever possible
PREPROCESSING
-n, --no-up-backbones Do NOT perform propagation of literals which
can be derived by unit propagation from the
input formula. This is useful for checking the
......
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