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

OptionsGroup and using them in dpelim

parent 1119ef8e
......@@ -87,33 +87,33 @@ parse_arguments(int argc, char *argv[])
opts.InputOutput(&conf.input_file, &conf.output_file);
opts.SetHelpDesc(prg_help);
SUBool::DPElimEliminationOptions elim_opts;
SUBool::DPElimClauseManipOptions clause_manip_opts;
SUBool::DPElimMinimizeOptions minimize_opts;
opts.Add(elim_opts.Desc());
opts.Add(clause_manip_opts.Desc());
opts.Add(minimize_opts.Desc());
if (!opts.Parse(argc, argv) || !elim_opts.GetValues()
|| !clause_manip_opts.GetValues() || !minimize_opts.GetValues())
auto elim_opts = std::make_shared<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);
if (!opts.Parse(argc, argv))
{
return {};
}
conf.max_input_var = elim_opts.MaxInputVar();
conf.eliminate = elim_opts.EliminatePolicy();
conf.increase_policy = elim_opts.IncreasePolicy();
conf.max_increase = elim_opts.MaxIncrease();
conf.factor = elim_opts.Factor();
conf.max_input_var = elim_opts->MaxInputVar();
conf.eliminate = elim_opts->EliminatePolicy();
conf.increase_policy = elim_opts->IncreasePolicy();
conf.max_increase = elim_opts->MaxIncrease();
conf.factor = elim_opts->Factor();
conf.block_prime = clause_manip_opts.BlockPrime();
conf.inprocessing = clause_manip_opts.Inprocessing();
conf.ignore_policy = clause_manip_opts.IgnorePolicy();
conf.block_prime = clause_manip_opts->BlockPrime();
conf.inprocessing = clause_manip_opts->Inprocessing();
conf.ignore_policy = clause_manip_opts->IgnorePolicy();
conf.elim_minimize = minimize_opts.ElimMinimize();
conf.final_minimize = minimize_opts.FinalMinimize();
conf.minimize_size_step = minimize_opts.SizeStep();
conf.minimize_size_factor = minimize_opts.SizeFactor();
conf.elim_minimize = minimize_opts->ElimMinimize();
conf.final_minimize = minimize_opts->FinalMinimize();
conf.minimize_size_step = minimize_opts->SizeStep();
conf.minimize_size_factor = minimize_opts->SizeFactor();
return conf;
}
......
......@@ -23,7 +23,7 @@ const SUBool::EnumAnnotation<SUBool::DPElimEliminationOptions::ELIMINATE_POLICY>
void
SUBool::DPElimMinimizeOptions::Init()
{
mOptionsDesc.add_options() //
AddOptions() //
("minimize,m", po::bool_switch(&mFinalMinimize),
"Perform minimization at the end (not needed with -M option).") //
("elim-minimize,M", po::bool_switch(&mElimMinimize),
......@@ -44,10 +44,10 @@ SUBool::DPElimMinimizeOptions::GetValues()
}
SUBool::DPElimClauseManipOptions::DPElimClauseManipOptions()
: mBlockPrimeOption(CNFEncoding::kBlockPrimeAnnotation, "block-prime,P",
"Make new clauses prime after each block of DP "
"elimination.",
kDefaultBlockPrime),
: OptionsGroup("Clause manipulation"),
mBlockPrimeOption(CNFEncoding::kBlockPrimeAnnotation, "block-prime,P",
"Make new clauses prime after each block of DP elimination.",
kDefaultBlockPrime),
mInprocessingOption(DPEliminator::kInprocessingAnnotation, "process,p",
"how to inprocess the resolvent during auxiliary variable "
"elimination.",
......@@ -56,12 +56,11 @@ SUBool::DPElimClauseManipOptions::DPElimClauseManipOptions()
"ignore-policy,g",
"Which resolvents should be discarded during auxiliary variable "
"elimination.",
kDefaultIgnorePolicy),
mOptionsDesc("Clause manipulation")
kDefaultIgnorePolicy)
{
mOptionsDesc.add(mBlockPrimeOption);
mOptionsDesc.add(mInprocessingOption);
mOptionsDesc.add(mIgnorePolicyOption);
Add(mBlockPrimeOption);
Add(mInprocessingOption);
Add(mIgnorePolicyOption);
}
bool
......@@ -73,15 +72,15 @@ SUBool::DPElimClauseManipOptions::GetValues()
}
SUBool::DPElimEliminationOptions::DPElimEliminationOptions()
: mEliminatePolicyOption(kEliminatePolicyAnnotation, "eliminate,e",
"When to stop elimination", kDefaultEliminatePolicy),
: OptionsGroup("Elimination options"),
mEliminatePolicyOption(kEliminatePolicyAnnotation, "eliminate,e",
"When to stop elimination", kDefaultEliminatePolicy),
mIncreasePolicyOption(DPEliminator::kIncreasePolicyAnnotation,
"increase-policy,C", "How the size bound should be checked.",
kDefaultIncreasePolicy),
mOptionsDesc("Elimination options")
kDefaultIncreasePolicy)
{
mOptionsDesc.add(mEliminatePolicyOption);
mOptionsDesc.add_options() //
Add(mEliminatePolicyOption);
AddOptions() //
("max-input-var,x", po::value<unsigned>(&mMaxInputVar)->default_value(0),
"Maximum input variable. All variables with higher index are "
"considered auxiliary and possibly eliminated.") //
......@@ -95,7 +94,7 @@ SUBool::DPElimEliminationOptions::DPElimEliminationOptions()
kDefaultFactor, kDefaultFactorString),
"Stop the elimination when the number of clauses increases by the "
"given factor");
mOptionsDesc.add(mIncreasePolicyOption);
Add(mIncreasePolicyOption);
}
bool
......
......@@ -14,38 +14,13 @@
#include "dpelim.h"
#include "encoding.h"
#include "enum_opt.h"
#include "prg_opt_group.h"
namespace po = boost::program_options;
namespace SUBool
{
#if 0
struct elim_config_t
{
unsigned max_input_var{0};
// Clause manipulation
CNFEncoding::BLOCK_PRIME block_prime{CNFEncoding::BLOCK_PRIME::NONE};
DPEliminator::INPROCESSING inprocessing{DPEliminator::INPROCESSING::NONE};
DPEliminator::IGNORE_POLICY ignore_policy{
DPEliminator::IGNORE_POLICY::ABSORBED};
// Elimination policy
ELIMINATE_POLICY eliminate{ELIMINATE_POLICY::ALL};
DPEliminator::INCREASE_POLICY increase_policy{
DPEliminator::INCREASE_POLICY::AFTER_BOUND};
unsigned max_increase{0};
long double factor{1.0};
// bool use_minimize{false};
// bool final_minimize{false};
// unsigned minimize_size_step{5000};
// double minimize_size_factor{0.6};
};
#endif
class DPElimMinimizeOptions
class DPElimMinimizeOptions : public OptionsGroup
{
public:
static constexpr unsigned kDefaultSizeStep = 5000u;
......@@ -53,8 +28,6 @@ namespace SUBool
inline static const std::string kDefaultSizeFactorString = "0.6";
private:
po::options_description mOptionsDesc;
bool mElimMinimize{false};
bool mFinalMinimize{false};
unsigned mSizeStep{kDefaultSizeStep};
......@@ -65,9 +38,7 @@ namespace SUBool
public:
DPElimMinimizeOptions();
bool GetValues();
const po::options_description &Desc() const;
virtual bool GetValues() override;
bool ElimMinimize() const;
bool FinalMinimize() const;
......@@ -75,7 +46,7 @@ namespace SUBool
double SizeFactor() const;
};
class DPElimClauseManipOptions
class DPElimClauseManipOptions : public OptionsGroup
{
public:
static const CNFEncoding::BLOCK_PRIME kDefaultBlockPrime =
......@@ -94,21 +65,17 @@ namespace SUBool
DPEliminator::INPROCESSING mInprocessing{kDefaultInprocessing};
DPEliminator::IGNORE_POLICY mIgnorePolicy{kDefaultIgnorePolicy};
po::options_description mOptionsDesc;
public:
DPElimClauseManipOptions();
bool GetValues();
const po::options_description &Desc() const;
virtual bool GetValues() override;
CNFEncoding::BLOCK_PRIME BlockPrime() const;
DPEliminator::INPROCESSING Inprocessing() const;
DPEliminator::IGNORE_POLICY IgnorePolicy() const;
};
class DPElimEliminationOptions
class DPElimEliminationOptions : public OptionsGroup
{
public:
enum class ELIMINATE_POLICY
......@@ -139,14 +106,10 @@ namespace SUBool
unsigned mMaxIncrease{kDefaultMaxIncrease};
long double mFactor{kDefaultFactor};
po::options_description mOptionsDesc;
public:
DPElimEliminationOptions();
bool GetValues();
const po::options_description &Desc() const;
virtual bool GetValues() override;
ELIMINATE_POLICY EliminatePolicy() const;
DPEliminator::INCREASE_POLICY IncreasePolicy() const;
......@@ -158,17 +121,11 @@ namespace SUBool
} // namespace SUBool
inline SUBool::DPElimMinimizeOptions::DPElimMinimizeOptions()
: mOptionsDesc("Minimize options")
: OptionsGroup("Minimize options")
{
Init();
}
inline const po::options_description &
SUBool::DPElimMinimizeOptions::Desc() const
{
return mOptionsDesc;
}
inline bool
SUBool::DPElimMinimizeOptions::ElimMinimize() const
{
......@@ -193,12 +150,6 @@ SUBool::DPElimMinimizeOptions::SizeFactor() const
return mSizeFactor;
}
inline const po::options_description &
SUBool::DPElimClauseManipOptions::Desc() const
{
return mOptionsDesc;
}
inline SUBool::CNFEncoding::BLOCK_PRIME
SUBool::DPElimClauseManipOptions::BlockPrime() const
{
......@@ -217,12 +168,6 @@ SUBool::DPElimClauseManipOptions::IgnorePolicy() const
return mIgnorePolicy;
}
inline const po::options_description &
SUBool::DPElimEliminationOptions::Desc() const
{
return mOptionsDesc;
}
inline SUBool::DPElimEliminationOptions::ELIMINATE_POLICY
SUBool::DPElimEliminationOptions::EliminatePolicy() const
{
......
/*
* Project SUBool
* Petr Kucera, 2021
*/
/**@file prg_opt_group.h
* Program options group.
*/
#ifndef __PRG_OPT_GROUP
#define __PRG_OPT_GROUP
#include <boost/program_options.hpp>
#include <boost/smart_ptr/make_shared.hpp>
namespace po = boost::program_options;
namespace SUBool
{
class OptionsGroup
{
po::options_description mOptionsDesc;
protected:
po::options_description_easy_init AddOptions();
void Add(boost::shared_ptr<po::option_description> opt);
public:
OptionsGroup(const std::string &name);
virtual ~OptionsGroup() = default;
virtual bool GetValues() = 0;
const po::options_description &Desc() const;
};
} // namespace SUBool
inline const po::options_description &
SUBool::OptionsGroup::Desc() const
{
return mOptionsDesc;
}
inline po::options_description_easy_init
SUBool::OptionsGroup::AddOptions()
{
return mOptionsDesc.add_options();
}
inline void
SUBool::OptionsGroup::Add(boost::shared_ptr<po::option_description> opt)
{
mOptionsDesc.add(std::move(opt));
}
inline SUBool::OptionsGroup::OptionsGroup(const std::string &name)
: mOptionsDesc(name)
{
}
#endif
......@@ -121,6 +121,13 @@ SUBool::PrgOptions::Version() const
print_version(std::cout, mPrgName, mPrgDesc);
}
void
SUBool::PrgOptions::AddOptionsGroup(std::shared_ptr<OptionsGroup> opt_group)
{
Add(opt_group->Desc());
mOptGroups.push_back(std::move(opt_group));
}
bool
SUBool::PrgOptions::Parse(int argc, char *argv[])
{
......@@ -143,10 +150,23 @@ SUBool::PrgOptions::Parse(int argc, char *argv[])
<< std::endl;
return false;
}
if (!ProcessCommon())
if (!ProcessCommon() || !ProcessConfig())
{
return false;
}
for (auto &opt_group : mOptGroups)
{
if (!opt_group->GetValues())
{
return false;
}
}
return true;
}
bool
SUBool::PrgOptions::ProcessConfig()
{
if (!mUseConfigFile || mVM.count("no-config") || mConfigFile.empty())
{
return true;
......@@ -177,6 +197,4 @@ SUBool::PrgOptions::Parse(int argc, char *argv[])
return false;
}
return true;
// TODO: parse config file
}
......@@ -20,6 +20,7 @@
#include "enum.h"
#include "logstream.h"
#include "prg_opt_group.h"
#include "sbexception.h"
#include "util.h"
......@@ -148,11 +149,13 @@ namespace SUBool
po::options_description mVisible{};
po::positional_options_description mPositional{};
po::variables_map mVM{};
std::vector<std::shared_ptr<OptionsGroup>> mOptGroups;
void Help() const;
void Version() const;
void Info() const;
bool ProcessCommon() const;
bool ProcessConfig();
void InitCommon();
......@@ -181,6 +184,7 @@ namespace SUBool
const po::variables_map &VarMap() const;
po::options_description_easy_init AddOptions();
void Add(const po::options_description &desc);
void AddOptionsGroup(std::shared_ptr<OptionsGroup> opt_group);
bool HasValue(const std::string &opt_name) const;
};
......
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