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

Algorithm selection in pccompile

parent 869738e1
...@@ -18,6 +18,7 @@ ...@@ -18,6 +18,7 @@
#include "cnfcompress.h" #include "cnfcompress.h"
#include "logstream.h" #include "logstream.h"
#include "normalform.h" #include "normalform.h"
#include "pc_opt.h"
#include "pccomp.h" #include "pccomp.h"
#include "pcenc.h" #include "pcenc.h"
#include "pclearncomp.h" #include "pclearncomp.h"
...@@ -36,31 +37,16 @@ const std::string prg_help = ...@@ -36,31 +37,16 @@ const std::string prg_help =
"Implements an incremental algorithm based on adding empowering " "Implements an incremental algorithm based on adding empowering "
"implicates and a learning algorithm"; "implicates and a learning algorithm";
enum class GOAL
{
PC,
UC
};
enum class ALGORITHM
{
INCREMENT,
LEARNING,
Last = LEARNING
};
const std::array<std::string, static_cast<size_t>(ALGORITHM::Last) + 1>
algorithm_names{"incremental", "learning"};
struct config_t struct config_t
{ {
std::string input_file{}; std::string input_file{};
std::string output_file{}; std::string output_file{};
bool minimize{false}; bool minimize{false};
SUBool::MINIMIZE_METHOD minimize_method{SUBool::MINIMIZE_METHOD::FULL}; SUBool::MINIMIZE_METHOD minimize_method{SUBool::MINIMIZE_METHOD::FULL};
ALGORITHM algorithm{ALGORITHM::INCREMENT}; SUBool::PCCAlgorithmOptions::ALGORITHM algorithm{
bool level_simplify{true}; // simplification at level increase SUBool::PCCAlgorithmOptions::kDefaultAlgorithm};
unsigned verbosity{3}; // 0 means no output bool level_simplify{true}; // simplification at level increase
bool uc_interleave_pc{false}; unsigned verbosity{3}; // 0 means no output
bool use_empty_initial_hypothesis{false}; // For PCLearnComp bool use_empty_initial_hypothesis{false}; // For PCLearnComp
unsigned pccheck_random_rounds{100}; unsigned pccheck_random_rounds{100};
unsigned pccheck_random_budget{10}; unsigned pccheck_random_budget{10};
...@@ -82,7 +68,6 @@ struct config_t ...@@ -82,7 +68,6 @@ struct config_t
SUBool::LIT_IMPL_SYSTEM::NONE, SUBool::LIT_IMPL_SYSTEM::NONE,
SUBool::SOLVER_TYPE::GLUCOSE, SUBool::SOLVER_TYPE::GLUCOSE,
}; };
GOAL goal{GOAL::PC};
bool unfinished_write{true}; bool unfinished_write{true};
SUBool::AmoEncoder::KIND amo_encoding{SUBool::AmoEncoder::KIND::REPR}; SUBool::AmoEncoder::KIND amo_encoding{SUBool::AmoEncoder::KIND::REPR};
SUBool::ExOneEncoder::KIND exone_encoding{SUBool::ExOneEncoder::KIND::REPR}; SUBool::ExOneEncoder::KIND exone_encoding{SUBool::ExOneEncoder::KIND::REPR};
...@@ -121,10 +106,8 @@ dump_config(const config_t &conf, unsigned level) ...@@ -121,10 +106,8 @@ dump_config(const config_t &conf, unsigned level)
<< "\tminimize: " << SUBool::bool_to_string(conf.minimize) << std::endl; << "\tminimize: " << SUBool::bool_to_string(conf.minimize) << std::endl;
SUBool::kMinimizeMethodAnnotation.DumpValue( SUBool::kMinimizeMethodAnnotation.DumpValue(
"\t", level, "minimize_method", conf.comp_base_config.minimize_method); "\t", level, "minimize_method", conf.comp_base_config.minimize_method);
SUBool::logs.TLog(level) SUBool::PCCAlgorithmOptions::kAlgorithmAnnotation.DumpValue(
<< "\talgorithm: " "\t", level, "algorithm", conf.algorithm);
<< algorithm_names.at(static_cast<unsigned>(conf.algorithm))
<< std::endl;
SUBool::logs.TLog(level) SUBool::logs.TLog(level)
<< "\tcomp_base_config.up_empower: " << "\tcomp_base_config.up_empower: "
<< static_cast<unsigned>(conf.comp_base_config.up_empower) << std::endl; << static_cast<unsigned>(conf.comp_base_config.up_empower) << std::endl;
...@@ -145,9 +128,6 @@ dump_config(const config_t &conf, unsigned level) ...@@ -145,9 +128,6 @@ dump_config(const config_t &conf, unsigned level)
<< static_cast<unsigned>(conf.comp_base_config.preprocess) << std::endl; << static_cast<unsigned>(conf.comp_base_config.preprocess) << std::endl;
SUBool::logs.DumpValue("\t", level, "comp_base_config.propagate_backbones", SUBool::logs.DumpValue("\t", level, "comp_base_config.propagate_backbones",
conf.comp_base_config.propagate_backbones); conf.comp_base_config.propagate_backbones);
SUBool::logs.TLog(level)
<< "\tuc_interleave_pc: "
<< SUBool::bool_to_string(conf.uc_interleave_pc) << std::endl;
SUBool::logs.DumpValue("\t", level, "use_empty_initial_hypothesis", SUBool::logs.DumpValue("\t", level, "use_empty_initial_hypothesis",
conf.use_empty_initial_hypothesis); conf.use_empty_initial_hypothesis);
SUBool::logs.TLog(level) SUBool::logs.TLog(level)
...@@ -176,8 +156,6 @@ dump_config(const config_t &conf, unsigned level) ...@@ -176,8 +156,6 @@ dump_config(const config_t &conf, unsigned level)
<< conf.comp_base_config.timeouts.level_factor << std::endl; << conf.comp_base_config.timeouts.level_factor << std::endl;
SUBool::dump_enum_value("\t", level, "cop_base_config.solver_type", SUBool::dump_enum_value("\t", level, "cop_base_config.solver_type",
conf.comp_base_config.solver_type, SUBool::kSolverTypeNames); conf.comp_base_config.solver_type, SUBool::kSolverTypeNames);
SUBool::logs.TLog(level)
<< "\tgoal: " << (conf.goal == GOAL::PC ? "PC" : "UC") << std::endl;
SUBool::logs.TLog(level) << "\tenc_conf:" << std::endl; SUBool::logs.TLog(level) << "\tenc_conf:" << std::endl;
conf.comp_base_config.enc_conf.Dump("\t\t", level); conf.comp_base_config.enc_conf.Dump("\t\t", level);
SUBool::AmoEncoder::kKindAnnotation.DumpValue( SUBool::AmoEncoder::kKindAnnotation.DumpValue(
...@@ -224,10 +202,13 @@ parse_arguments(int argc, char *argv[], config_t &conf) ...@@ -224,10 +202,13 @@ parse_arguments(int argc, char *argv[], config_t &conf)
SUBool::PrgOptions opts(true); SUBool::PrgOptions opts(true);
opts.SetHelpDesc(prg_help); opts.SetHelpDesc(prg_help);
opts.InputOutput(&conf.input_file, &conf.output_file); opts.InputOutput(&conf.input_file, &conf.output_file);
auto algorithm_opts = std::make_shared<SUBool::PCCAlgorithmOptions>();
opts.AddOptionsGroup(algorithm_opts);
if (!opts.Parse(argc, argv)) if (!opts.Parse(argc, argv))
{ {
return 1; return 1;
} }
conf.algorithm = algorithm_opts->Algorithm();
return 0; return 0;
#if 0 #if 0
try try
...@@ -681,31 +662,32 @@ incremental_compiler(const config_t &conf, SUBool::CNF cnf) ...@@ -681,31 +662,32 @@ incremental_compiler(const config_t &conf, SUBool::CNF cnf)
{ {
SUBool::AbsComp::BaseConfig a_conf; SUBool::AbsComp::BaseConfig a_conf;
fill_base_conf(a_conf, conf); fill_base_conf(a_conf, conf);
bool interleave_pc = false;
switch (conf.goal) switch (conf.algorithm)
{ {
case GOAL::PC: case SUBool::PCCAlgorithmOptions::ALGORITHM::INCREMENT_PC:
return std::make_shared<SUBool::PCComp>( return std::make_shared<SUBool::PCComp>(
std::move(cnf), std::move(a_conf)); std::move(cnf), std::move(a_conf));
case GOAL::UC: case SUBool::PCCAlgorithmOptions::ALGORITHM::INCREMENT_URC_PC:
interleave_pc = true;
[[fallthrough]];
case SUBool::PCCAlgorithmOptions::ALGORITHM::INCREMENT_URC:
{ {
SUBool::UCComp::Config uc_conf(a_conf); SUBool::UCComp::Config uc_conf(a_conf);
uc_conf.interleave_pc = conf.uc_interleave_pc; uc_conf.interleave_pc = interleave_pc;
return std::make_shared<SUBool::UCComp>( return std::make_shared<SUBool::UCComp>(
std::move(cnf), std::move(uc_conf)); std::move(cnf), std::move(uc_conf));
} }
default:
throw SUBool::BadParameterException(
"compiler", "Bad algorithm specification");
} }
throw SUBool::BadParameterException("compiler", "Bad goal specification");
} }
std::shared_ptr<SUBool::PCLearnComp> std::shared_ptr<SUBool::PCLearnComp>
learning_compiler(const config_t &conf, SUBool::CNF cnf) learning_compiler(const config_t &conf, SUBool::CNF cnf)
{ {
if (conf.goal != GOAL::PC)
{
throw SUBool::BadParameterException("learning_compiler",
"The learning compiler does not work with goal UC.");
}
SUBool::PCLearnComp::Config l_conf; SUBool::PCLearnComp::Config l_conf;
fill_base_conf(l_conf, conf); fill_base_conf(l_conf, conf);
l_conf.use_empty_initial_hypothesis = conf.use_empty_initial_hypothesis; l_conf.use_empty_initial_hypothesis = conf.use_empty_initial_hypothesis;
...@@ -720,15 +702,11 @@ learning_compiler(const config_t &conf, SUBool::CNF cnf) ...@@ -720,15 +702,11 @@ learning_compiler(const config_t &conf, SUBool::CNF cnf)
std::shared_ptr<SUBool::AbsComp> std::shared_ptr<SUBool::AbsComp>
compiler(const config_t &conf, SUBool::CNF cnf) compiler(const config_t &conf, SUBool::CNF cnf)
{ {
switch (conf.algorithm) if (conf.algorithm == SUBool::PCCAlgorithmOptions::ALGORITHM::LEARNING)
{ {
case ALGORITHM::INCREMENT:
return incremental_compiler(conf, std::move(cnf));
case ALGORITHM::LEARNING:
return learning_compiler(conf, std::move(cnf)); return learning_compiler(conf, std::move(cnf));
} }
throw SUBool::BadParameterException( return incremental_compiler(conf, std::move(cnf));
"compiler", "Unknown compilation algorithm specification");
} }
int int
...@@ -779,36 +757,6 @@ const std::string kUCEmpoweringImplicateName = "URC empowering implicate"; ...@@ -779,36 +757,6 @@ const std::string kUCEmpoweringImplicateName = "URC empowering implicate";
const std::string kPCEmpoweringVarName = "empowering variable"; const std::string kPCEmpoweringVarName = "empowering variable";
const std::string kUCEmpoweringVarName = "extending variable"; const std::string kUCEmpoweringVarName = "extending variable";
const std::string &
empowering_implicate_name(const config_t &conf)
{
switch (conf.goal)
{
case GOAL::PC:
return kPCEmpoweringImplicateName;
case GOAL::UC:
return kUCEmpoweringImplicateName;
default:
throw SUBool::BadParameterException(
"empowering_implicate_name", "Bad goal");
}
}
const std::string &
empowering_variable_name(const config_t &conf)
{
switch (conf.goal)
{
case GOAL::PC:
return kPCEmpoweringVarName;
case GOAL::UC:
return kUCEmpoweringVarName;
default:
throw SUBool::BadParameterException(
"empowering_variable_name", "Bad goal");
}
}
void void
terminate(int signal) terminate(int signal)
{ {
......
...@@ -8,9 +8,45 @@ ...@@ -8,9 +8,45 @@
#include "pc_opt.h" #include "pc_opt.h"
const SUBool::EnumAnnotation<SUBool::PCCAlgorithmOptions::ALGORITHM>
SUBool::PCCAlgorithmOptions::kAlgorithmAnnotation("ALGORITHM",
{//
{ALGORITHM::INCREMENT_PC, "increment_pc",
"heuristic algorithm based on incremental adding empowering "
"implicates. The goal is an equivalent PC formula and SAT "
"solver is used to "
"check if the formula is PC."}, //
{ALGORITHM::INCREMENT_URC, "increment_urc",
"heuristic algorithm based on incremental adding empowering "
"implicates. The goal is an equivalent URC formula and SAT "
"solver is used to "
"check if the formula is URC."}, //
{ALGORITHM::INCREMENT_URC_PC, "increment_urc_pc",
"heuristic algorithm based on incremental adding empowering "
"implicates. The goal is URC formula and SAT solver is used to "
"check if the formula is URC or PC in an interleaving wa."}, //
{ALGORITHM::LEARNING, "learning",
"based on the algorithm for learning a Horn formula through "
"equivalence and closure queries (Arias et al. 2015). The goal "
"is an equivalent PC formula."}});
auto auto
SUBool::minimize_method_opt() -> EnumOption<MINIMIZE_METHOD> SUBool::minimize_method_opt() -> EnumOption<MINIMIZE_METHOD>
{ {
return make_enum_option(kMinimizeMethodAnnotation, "minimize-method", return make_enum_option(kMinimizeMethodAnnotation, "minimize-method",
"Minimization method", kDefaultMinimizeMethod); "Minimization method", kDefaultMinimizeMethod);
} }
SUBool::PCCAlgorithmOptions::PCCAlgorithmOptions()
: OptionsGroup("Algorithm"),
mAlgorithmOption(kAlgorithmAnnotation, "algorithm,a",
"Algorithm used for compilation", kDefaultAlgorithm)
{
Add(mAlgorithmOption);
}
bool
SUBool::PCCAlgorithmOptions::GetValues()
{
return mAlgorithmOption.GetValue(mAlgorithm);
}
...@@ -11,11 +11,46 @@ ...@@ -11,11 +11,46 @@
#include "empower.h" #include "empower.h"
#include "enum_opt.h" #include "enum_opt.h"
#include "prg_opt_group.h"
namespace SUBool namespace SUBool
{ {
// "Minimization method", "minimize-method" // "Minimization method", "minimize-method"
EnumOption<MINIMIZE_METHOD> minimize_method_opt(); EnumOption<MINIMIZE_METHOD> minimize_method_opt();
// Algorithm selection in pccompile
class PCCAlgorithmOptions : public OptionsGroup
{
public:
enum class ALGORITHM
{
INCREMENT_PC,
INCREMENT_URC,
INCREMENT_URC_PC,
LEARNING
};
static const EnumAnnotation<ALGORITHM> kAlgorithmAnnotation;
static const ALGORITHM kDefaultAlgorithm = ALGORITHM::LEARNING;
private:
EnumOption<ALGORITHM> mAlgorithmOption;
ALGORITHM mAlgorithm{kDefaultAlgorithm};
public:
PCCAlgorithmOptions();
virtual bool GetValues() override;
ALGORITHM Algorithm() const;
};
} // namespace SUBool } // namespace SUBool
inline auto
SUBool::PCCAlgorithmOptions::Algorithm() const -> ALGORITHM
{
return mAlgorithm;
}
#endif #endif
pccompile [OPTION...] [input [output]] pccompile [OPTION...] [input [output]]
Algorithm Selection ALGORITHM SELECTION
-a, --algorithm arg The compilation algorithm. 'incremental' -- a -a, --algorithm arg The compilation algorithm. 'incremental' -- a
heuristic algorithm based on incremental heuristic algorithm based on incremental
...@@ -14,12 +14,15 @@ Algorithm Selection ...@@ -14,12 +14,15 @@ Algorithm Selection
Other parameters are used appropriately. Other parameters are used appropriately.
(default: incremental) (default: incremental)
NEW: Includes goal, possible choices:
incremental_pc, incremental_uc, incremental_ucpc, learning
UNIT REFUTATION COMPLETENESS UNIT REFUTATION COMPLETENESS
-u, --uc Aim for unit refutation completeness instead # -u, --uc Aim for unit refutation completeness instead
of propagation completeness. # of propagation completeness.
--interleave-pc In case of compilation to UC, interleave #--interleave-pc In case of compilation to UC, interleave
encodings for UC and PC. #encodings for UC and PC.
LEARNING ALGORITHM LEARNING ALGORITHM
......
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