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

pccompile preprocessing options

parent 12c6127c
......@@ -87,13 +87,10 @@ parse_arguments(int argc, char *argv[])
opts.InputOutput(&conf.input_file, &conf.output_file);
opts.SetHelpDesc(prg_help);
auto elim_opts = std::make_shared<SUBool::DPElimEliminationOptions>();
auto elim_opts = opts.MakeOptionsGroup<SUBool::DPElimEliminationOptions>();
auto clause_manip_opts =
std::make_shared<SUBool::DPElimClauseManipOptions>();
auto minimize_opts = std::make_shared<SUBool::DPElimMinimizeOptions>();
opts.AddOptionsGroup(elim_opts);
opts.AddOptionsGroup(clause_manip_opts);
opts.AddOptionsGroup(minimize_opts);
opts.MakeOptionsGroup<SUBool::DPElimClauseManipOptions>();
auto minimize_opts = opts.MakeOptionsGroup<SUBool::DPElimMinimizeOptions>();
if (!opts.Parse(argc, argv))
{
......
......@@ -104,7 +104,6 @@ parse_arguments(int argc, char *argv[])
"level-func,L",
"How to compute levels in case of construction of URC or PC encoding.",
kDefaultLevelFunc);
auto cardinal_opt_group = std::make_shared<SUBool::CardinalOptionsGroup>();
SUBool::PrgOptions opts(true);
opts.SetHelpDesc(kPrgHelp);
......@@ -119,7 +118,8 @@ parse_arguments(int argc, char *argv[])
"Check for smoothness and make DNNF smooth before constructing the "
"encoding if necessary");
opts.Add(desc);
opts.AddOptionsGroup(cardinal_opt_group);
auto cardinal_opt_group =
opts.MakeOptionsGroup<SUBool::CardinalOptionsGroup>();
if (!opts.Parse(argc, argv)
|| !opt_encoding_type.GetValue(conf.encoding_type)
|| !opt_level_func.GetValue(conf.level_func))
......
......@@ -123,9 +123,8 @@ dump_config(const config_t &conf, unsigned level)
SUBool::dump_enum_value("\t", level, "comp_base_config.impl_system",
conf.comp_base_config.impl_system, SUBool::kImplSystemNames);
SUBool::logs.TLog(level) << "\tverbosity: " << conf.verbosity << std::endl;
SUBool::logs.TLog(level)
<< "\tcomp_base_config.preprocess: "
<< static_cast<unsigned>(conf.comp_base_config.preprocess) << std::endl;
SUBool::AbsComp::kPreprocessMethodAnnotation.DumpValue("\t", level,
"comp_base_config.preprocess", conf.comp_base_config.preprocess);
SUBool::logs.DumpValue("\t", level, "comp_base_config.propagate_backbones",
conf.comp_base_config.propagate_backbones);
SUBool::logs.DumpValue("\t", level, "use_empty_initial_hypothesis",
......@@ -201,10 +200,11 @@ parse_arguments(int argc, char *argv[], config_t &conf)
SUBool::PrgOptions opts(true);
opts.SetHelpDesc(prg_help);
opts.InputOutput(&conf.input_file, &conf.output_file);
auto algorithm_opts = std::make_shared<SUBool::PCCompAlgorithmOptions>();
opts.AddOptionsGroup(algorithm_opts);
auto pclearncomp_opts = std::make_shared<SUBool::PCLearnCompOptions>();
opts.AddOptionsGroup(pclearncomp_opts);
auto algorithm_opts =
opts.MakeOptionsGroup<SUBool::PCCompAlgorithmOptions>();
auto pclearncomp_opts = opts.MakeOptionsGroup<SUBool::PCLearnCompOptions>();
auto preprocess_opts =
opts.MakeOptionsGroup<SUBool::PCCompPreprocessOptions>();
if (!opts.Parse(argc, argv))
{
return 1;
......@@ -214,6 +214,9 @@ parse_arguments(int argc, char *argv[], config_t &conf)
conf.use_empty_initial_hypothesis =
pclearncomp_opts->UseEmptyInitialHypothesis();
conf.initial_negatives = pclearncomp_opts->InitialNegatives();
conf.comp_base_config.preprocess = preprocess_opts->PreprocessMethod();
conf.comp_base_config.propagate_backbones =
!preprocess_opts->NoBackbonePropagation();
return 0;
#if 0
try
......
......@@ -31,11 +31,30 @@ const SUBool::AbsComp::StateValue SUBool::AbsComp::SOLVER_INTERRUPTED{
const SUBool::AbsComp::StateValue SUBool::AbsComp::TIMED_OUT{
"TIMED_OUT", SUBool::AbsComp::RESULT::TIMED_OUT};
SUBool::AbsComp::AbsComp(CNF cnf, MINIMIZE_METHOD minimize_method,
LIT_IMPL_SYSTEM impl_system_kind)
const SUBool::EnumAnnotation<SUBool::AbsComp::PREPROCESS_METHOD>
SUBool::AbsComp::kPreprocessMethodAnnotation("PREPROCESS_METHOD",
{ //
{PREPROCESS_METHOD::NONE, "none", "no preprocessing."}, //
{PREPROCESS_METHOD::MINIMIZE, "minimize",
"minimize the formula by removing the clauses absorbed by the "
"others (not empowering with respect to propagation "
"completeness)"}, //
{PREPROCESS_METHOD::UP_PRIME_MINIMIZE, "up_prime_minimize",
"make the CNF prime with respect to 1-provability, then "
"minimize it."}, //
{PREPROCESS_METHOD::PRIME_MINIMIZE, "prime_minimize",
"make the CNF prime and then minimize it."}, //
{PREPROCESS_METHOD::UP_PRIME, "up_prime",
"make the CNF prime with respect to 1-provability with no "
"minimization."}, //
{PREPROCESS_METHOD::PRIME, "prime",
"make the CNF prime with no minimization."}});
SUBool::AbsComp::AbsComp(
CNF cnf, MINIMIZE_METHOD minimize_method, LIT_IMPL_SYSTEM impl_system_kind)
: mStateMutex(), mRTime(), mCPUTime(),
mHypothesis(minimize_method, impl_system_kind, CNF(), std::move(cnf),
false)
mHypothesis(
minimize_method, impl_system_kind, CNF(), std::move(cnf), false)
{
}
......@@ -156,8 +175,8 @@ SUBool::AbsComp::Preprocess()
PreprocessPrime();
break;
default:
throw BadParameterException("AbsComp::Preprocess",
"Unkown preprocess method");
throw BadParameterException(
"AbsComp::Preprocess", "Unkown preprocess method");
}
if (minimize)
{
......
......@@ -16,6 +16,7 @@
#include "comp_hypothesis.h"
#include "cpuutil.h"
#include "drenc.h"
#include "enum.h"
#include "normalform.h"
namespace SUBool
......@@ -54,6 +55,8 @@ namespace SUBool
Last = PRIME
};
static const EnumAnnotation<PREPROCESS_METHOD>
kPreprocessMethodAnnotation;
static PREPROCESS_METHOD PMRemoveMinimize(PREPROCESS_METHOD preprocess);
struct StateValue
......@@ -124,7 +127,7 @@ namespace SUBool
public:
AbsComp(CNF cnf, MINIMIZE_METHOD minimize_method,
LIT_IMPL_SYSTEM impl_system_kind);
LIT_IMPL_SYSTEM impl_system_kind);
virtual ~AbsComp() = default;
AbsComp(const AbsComp &other) = delete;
......
......@@ -37,7 +37,7 @@ SUBool::minimize_method_opt() -> EnumOption<MINIMIZE_METHOD>
"Minimization method", kDefaultMinimizeMethod);
}
SUBool::PCCompAlgorithmOptions::PCCAlgorithmOptions()
SUBool::PCCompAlgorithmOptions::PCCompAlgorithmOptions()
: OptionsGroup("Algorithm Selection"),
mAlgorithmOption(kAlgorithmAnnotation, "algorithm,a",
"Algorithm used for compilation", kDefaultAlgorithm)
......@@ -72,3 +72,20 @@ SUBool::PCLearnCompOptions::GetValues()
{
return mInitialNegativesOption.GetValue(mInitialNegatives);
}
SUBool::PCCompPreprocessOptions::PCCompPreprocessOptions()
: OptionsGroup("Preprocessing"),
mPreprocessMethodOption(AbsComp::kPreprocessMethodAnnotation,
"preprocess,r", "Method of preprocessing.", kDefaultPreprocessMethod)
{
Add(mPreprocessMethodOption);
AddOptions()("no-backbone-propagation",
po::bool_switch(&mNoBackbonePropagation),
"Do not perform backbone propagation before preprocessing.");
}
bool
SUBool::PCCompPreprocessOptions::GetValues()
{
return mPreprocessMethodOption.GetValue(mPreprocessMethod);
}
......@@ -32,7 +32,7 @@ namespace SUBool
};
static const EnumAnnotation<ALGORITHM> kAlgorithmAnnotation;
static const ALGORITHM kDefaultAlgorithm = ALGORITHM::LEARNING;
static constexpr ALGORITHM kDefaultAlgorithm = ALGORITHM::LEARNING;
private:
EnumOption<ALGORITHM> mAlgorithmOption;
......@@ -68,6 +68,27 @@ namespace SUBool
PCLearnComp::INITIAL_NEGATIVES InitialNegatives() const;
};
// pccompile preprocessing
class PCCompPreprocessOptions : public OptionsGroup
{
public:
static constexpr AbsComp::PREPROCESS_METHOD kDefaultPreprocessMethod =
AbsComp::PREPROCESS_METHOD::PRIME_MINIMIZE;
private:
bool mNoBackbonePropagation{false};
EnumOption<AbsComp::PREPROCESS_METHOD> mPreprocessMethodOption;
AbsComp::PREPROCESS_METHOD mPreprocessMethod{kDefaultPreprocessMethod};
public:
PCCompPreprocessOptions();
virtual bool GetValues() override;
bool NoBackbonePropagation() const;
AbsComp::PREPROCESS_METHOD PreprocessMethod() const;
};
} // namespace SUBool
inline auto
......@@ -89,4 +110,16 @@ SUBool::PCLearnCompOptions::InitialNegatives() const
return mInitialNegatives;
}
inline bool
SUBool::PCCompPreprocessOptions::NoBackbonePropagation() const
{
return mNoBackbonePropagation;
}
inline SUBool::AbsComp::PREPROCESS_METHOD
SUBool::PCCompPreprocessOptions::PreprocessMethod() const
{
return mPreprocessMethod;
}
#endif
......@@ -186,6 +186,7 @@ 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();
bool HasValue(const std::string &opt_name) const;
};
......@@ -247,4 +248,13 @@ SUBool::PrgOptions::HasValue(const std::string &opt_name) const
return mVM.count(opt_name);
}
template <class T>
std::shared_ptr<T>
SUBool::PrgOptions::MakeOptionsGroup()
{
auto opt_group = std::make_shared<T>();
AddOptionsGroup(opt_group);
return opt_group;
}
#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