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

goal selection in pccheck

parent 903a3a37
......@@ -19,6 +19,7 @@
#include "cnfcompress.h"
#include "logstream.h"
#include "normalform.h"
#include "pc_opt.h"
#include "pccomp.h"
#include "pcenc.h"
#include "pclearncomp.h"
......@@ -35,12 +36,6 @@ const std::string prg_help =
"Checks if a given CNF is propagation complete (PC) or unit refutation "
"complete (URC). Can also output the SAT encoding of the required query.";
enum class GOAL
{
PC,
UC
};
struct config_t
{
std::string input_file{};
......@@ -53,7 +48,8 @@ struct config_t
SUBool::AbsEncoder::AbsConfig enc_conf{};
SUBool::AbsCheckerSAT::Timeouts timeouts{};
SUBool::LIT_IMPL_SYSTEM impl_system{SUBool::LIT_IMPL_SYSTEM::Default};
GOAL goal{GOAL::PC};
SUBool::PCCheckGoalOptions::GOAL goal{
SUBool::PCCheckGoalOptions::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};
......@@ -76,12 +72,6 @@ struct config_t
};
};
constexpr const char *
goal_name(const config_t &conf)
{
return (conf.goal == GOAL::PC ? "PC" : "URC");
}
void
dump_config(const config_t &conf, unsigned level)
{
......@@ -90,6 +80,8 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level)
<< "\toutput_file: " << conf.output_file << std::endl;
SUBool::logs.DumpVerbosity("\t", level);
SUBool::PCCheckGoalOptions::kGoalAnnotation.DumpValue(
"\t", level, "goal", conf.goal);
SUBool::logs.TLog(level)
<< "\tencode_only: " << SUBool::bool_to_string(conf.encode_only)
<< std::endl;
......@@ -109,7 +101,6 @@ dump_config(const config_t &conf, unsigned level)
<< std::endl;
SUBool::kLitImplSystemAnnotation.DumpValue(
"\t", level, "impl_system", conf.impl_system);
SUBool::logs.TLog(level) << "\tgoal: " << goal_name(conf) << std::endl;
SUBool::AmoEncoder::kKindAnnotation.DumpValue(
"\t", level, "amo_encoding", conf.amo_encoding);
SUBool::ExOneEncoder::kKindAnnotation.DumpValue(
......@@ -157,10 +148,12 @@ parse_arguments(int argc, char *argv[])
SUBool::PrgOptions opts(true);
opts.SetHelpDesc(prg_help);
opts.InputOutput(&conf.input_file, &conf.output_file);
auto goal_opts = opts.MakeOptionsGroup<SUBool::PCCheckGoalOptions>();
if (!opts.Parse(argc, argv))
{
return {};
}
conf.goal = goal_opts->Goal();
return conf;
#if 0
try
......@@ -474,41 +467,6 @@ encode(const config_t &conf, const SUBool::CompHypothesis &hyp,
return 0;
}
const std::string kPCEmpoweringImplicateName = "empowering implicate";
const std::string kUCEmpoweringImplicateName = "URC empowering implicate";
const std::string kPCEmpoweringVarName = "empowering 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");
}
}
int
empower(const config_t &conf, SUBool::CompHypothesis &hyp,
SUBool::AbsCheckerSAT &checker)
......@@ -526,7 +484,9 @@ empower(const config_t &conf, SUBool::CompHypothesis &hyp,
return 1;
}
SUBool::logs.TLog(1) << "No empowering implicate found, formula is "
<< goal_name(conf) << " complete" << std::endl;
<< SUBool::PCCheckGoalOptions::kGoalAnnotation.Name(
conf.goal)
<< " complete" << std::endl;
return 0;
}
......@@ -563,9 +523,9 @@ checker_sat(const config_t &conf)
{
switch (conf.goal)
{
case GOAL::PC:
case SUBool::PCCheckGoalOptions::GOAL::PC:
return pc_checker_sat(conf);
case GOAL::UC:
case SUBool::PCCheckGoalOptions::GOAL::URC:
return urc_checker_sat(conf);
default:
throw SUBool::BadParameterException("checker_sat", "Unknown goal");
......
......@@ -30,6 +30,16 @@ 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(
"GOAL", {
//
{GOAL::PC, "pc",
"check if the formula is propagation complete."}, //
{GOAL::URC, "urc",
"check if the formula is unit refutation complete."} //
});
auto
SUBool::minimize_method_opt() -> EnumOption<MINIMIZE_METHOD>
{
......@@ -283,3 +293,18 @@ SUBool::PCTimeoutsOptions::GetValues()
{
return true;
}
SUBool::PCCheckGoalOptions::PCCheckGoalOptions()
: OptionsGroup("General Options"),
mGoalOption(
kGoalAnnotation, "goal,g", "What should be checked", kDefaultGoal)
{
Add(mGoalOption);
}
bool
SUBool::PCCheckGoalOptions::GetValues()
{
return true;
}
......@@ -222,6 +222,30 @@ namespace SUBool
const AbsCheckerSAT::Timeouts &EmpTimeouts() const;
long double Timeout() const;
};
class PCCheckGoalOptions : public OptionsGroup
{
public:
enum class GOAL
{
PC,
URC
};
static const EnumAnnotation<GOAL> kGoalAnnotation;
static const GOAL kDefaultGoal = GOAL::PC;
private:
EnumOption<GOAL> mGoalOption;
GOAL mGoal;
public:
PCCheckGoalOptions();
virtual bool GetValues() override;
GOAL Goal() const;
};
} // namespace SUBool
inline auto
......@@ -350,4 +374,11 @@ SUBool::PCTimeoutsOptions::Timeout() const
{
return mTimeout;
}
inline SUBool::PCCheckGoalOptions::GOAL
SUBool::PCCheckGoalOptions::Goal() const
{
return mGoal;
}
#endif
......@@ -2,11 +2,21 @@
TODO: Allow only input file, output file should be passed with -e option
UNIT REFUTATION COMPLETENESS
General Options
-u, --uc Aim for unit refutation completeness instead
of propagation completeness.
-e, --encode Do not check, just write the encoding to the
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
construction of an encoding.
ONE PROVABILITY
-1, --one-prove arg What kind of encoding should be used for
......@@ -62,19 +72,7 @@ ONE PROVABILITY
logarithm of the parameter rounded up.
(default: 0)
GENERAL OPTIONS
-d, --dump Back mapping of variables (names) are used
wherever possible
-e, --encode Do not check, just write the encoding to the
output file
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
construction of an encoding.
EMPOWEREMENT
-w, --empower arg What kind of encoding should be used for
......
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