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

Options of pccompile related to the learning algorithm

parent e010c290
......@@ -139,9 +139,8 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level)
<< "\tpccheck_random_budget_inc: " << conf.pccheck_random_budget_inc
<< std::endl;
SUBool::logs.DumpValue("\t", level, "initial_negatives",
SUBool::PCLearnComp::cInitialNegativesNames[static_cast<size_t>(
conf.initial_negatives)]);
SUBool::PCLearnComp::kInitialNegativesAnnotation.DumpValue(
"\t", level, "initial_negatives", conf.initial_negatives);
SUBool::logs.TLog(level)
<< "\trandom seed: " << conf.random_seed << std::endl;
SUBool::logs.TLog(level) << "\ttimeout: " << conf.timeout << std::endl;
......@@ -204,11 +203,17 @@ parse_arguments(int argc, char *argv[], config_t &conf)
opts.InputOutput(&conf.input_file, &conf.output_file);
auto algorithm_opts = std::make_shared<SUBool::PCCAlgorithmOptions>();
opts.AddOptionsGroup(algorithm_opts);
auto pclearncomp_opts = std::make_shared<SUBool::PCLearnCompOptions>();
opts.AddOptionsGroup(pclearncomp_opts);
if (!opts.Parse(argc, argv))
{
return 1;
}
conf.algorithm = algorithm_opts->Algorithm();
conf.use_empty_initial_hypothesis =
pclearncomp_opts->UseEmptyInitialHypothesis();
conf.initial_negatives = pclearncomp_opts->InitialNegatives();
return 0;
#if 0
try
......@@ -802,9 +807,12 @@ main(int argc, char *argv[])
<< "PCCompile " << SUBool::kVersionInfo << std::endl;
dump_config(the_conf, 3);
return 0;
#if 0
SUBool::AmoEncoder::sGlobalKind = the_conf.amo_encoding;
SUBool::ExOneEncoder::sGlobalKind = the_conf.exone_encoding;
auto ret = compile(std::move(cnf));
the_compiler = nullptr;
return ret;
#endif
}
......@@ -11,20 +11,20 @@
const SUBool::EnumAnnotation<SUBool::PCCAlgorithmOptions::ALGORITHM>
SUBool::PCCAlgorithmOptions::kAlgorithmAnnotation("ALGORITHM",
{//
{ALGORITHM::INCREMENT_PC, "increment_pc",
{ALGORITHM::INCREMENT_PC, "incremental_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",
{ALGORITHM::INCREMENT_URC, "incremental_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",
{ALGORITHM::INCREMENT_URC_PC, "incremental_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."}, //
"check if the formula is URC or PC in an interleaving way."}, //
{ALGORITHM::LEARNING, "learning",
"based on the algorithm for learning a Horn formula through "
"equivalence and closure queries (Arias et al. 2015). The goal "
......@@ -38,7 +38,7 @@ SUBool::minimize_method_opt() -> EnumOption<MINIMIZE_METHOD>
}
SUBool::PCCAlgorithmOptions::PCCAlgorithmOptions()
: OptionsGroup("Algorithm"),
: OptionsGroup("Algorithm Selection"),
mAlgorithmOption(kAlgorithmAnnotation, "algorithm,a",
"Algorithm used for compilation", kDefaultAlgorithm)
{
......@@ -50,3 +50,25 @@ SUBool::PCCAlgorithmOptions::GetValues()
{
return mAlgorithmOption.GetValue(mAlgorithm);
}
SUBool::PCLearnCompOptions::PCLearnCompOptions()
: OptionsGroup("Learning Algorithm Options"),
mInitialNegativesOption(PCLearnComp::kInitialNegativesAnnotation,
"initial-negatives",
"How the initial negative examples in the learning algorithm "
"should be produced. The option specifies how the negatives for each "
"clause in the preprocessed CNF are created.",
kDefaultInitialNegatives)
{
AddOptions()("use-empty-initial-hypothesis",
po::bool_switch(&mUseEmptyInitialHypothesis),
"Use empty initial hypothesis in the learning algorithm. If not "
"set, the preprocessed input CNF is used as an initial hypothesis.");
Add(mInitialNegativesOption);
}
bool
SUBool::PCLearnCompOptions::GetValues()
{
return mInitialNegativesOption.GetValue(mInitialNegatives);
}
......@@ -11,6 +11,7 @@
#include "empower.h"
#include "enum_opt.h"
#include "pclearncomp.h"
#include "prg_opt_group.h"
namespace SUBool
......@@ -45,6 +46,28 @@ namespace SUBool
ALGORITHM Algorithm() const;
};
// Learning Algorithm Options
class PCLearnCompOptions : public OptionsGroup
{
public:
PCLearnComp::INITIAL_NEGATIVES kDefaultInitialNegatives{
PCLearnComp::INITIAL_NEGATIVES::ALL_EMPOWERING};
private:
bool mUseEmptyInitialHypothesis{false};
EnumOption<PCLearnComp::INITIAL_NEGATIVES> mInitialNegativesOption;
PCLearnComp::INITIAL_NEGATIVES mInitialNegatives{
kDefaultInitialNegatives};
public:
PCLearnCompOptions();
virtual bool GetValues() override;
bool UseEmptyInitialHypothesis() const;
PCLearnComp::INITIAL_NEGATIVES InitialNegatives() const;
};
} // namespace SUBool
inline auto
......@@ -53,4 +76,17 @@ SUBool::PCCAlgorithmOptions::Algorithm() const -> ALGORITHM
return mAlgorithm;
}
inline bool
SUBool::PCLearnCompOptions::UseEmptyInitialHypothesis() const
{
return mUseEmptyInitialHypothesis;
}
inline auto
SUBool::PCLearnCompOptions::InitialNegatives() const
-> PCLearnComp::INITIAL_NEGATIVES
{
return mInitialNegatives;
}
#endif
......@@ -53,12 +53,31 @@ const SUBool::AbsComp::StateValue
SUBool::PCLearnComp::REMOVE_DUPLICITIES_IN_NEGATIVES{
"REMOVE_DUPLICITIES_IN_NEGATIVES", SUBool::AbsComp::RESULT::UNFINISHED};
const std::array<std::string, static_cast<size_t>(
SUBool::PCLearnComp::INITIAL_NEGATIVES::Last)
+ 1>
SUBool::PCLearnComp::cInitialNegativesNames{"single_empowering", "all",
"all_empowering", "gd_basis",
"body_minimal"};
const SUBool::EnumAnnotation<SUBool::PCLearnComp::INITIAL_NEGATIVES>
SUBool::PCLearnComp::kInitialNegativesAnnotation("INITIAL_NEGATIVES",
{//
{PCLearnComp::INITIAL_NEGATIVES::SINGLE_EMPOWERING,
"single_empowering",
"one negative example is produced from every empowering "
"clause "
"(the clause C without an empowered literal)"}, //
{PCLearnComp::INITIAL_NEGATIVES::ALL, "all",
"all negative examples from all clauses are produced, i.e. for "
"every clause C and a literal l in C, C without l is added as "
"a negative example regardless on whether C is empowering with "
"l being an empowered literal."}, //
{PCLearnComp::INITIAL_NEGATIVES::ALL_EMPOWERING, "all_empowering",
"for every empowering clause C and every empowered literal l "
"in C, C without l is added as a negative example to the "
"initial list."}, //
{PCLearnComp::INITIAL_NEGATIVES::GD_BASIS, "gd_basis",
"GD basis of the dual rail encoding of the preprocessed CNF is "
"computed, the bodies in the GD basis form the initial list of "
"negative examples."}, //
{PCLearnComp::INITIAL_NEGATIVES::BODY_MINIMAL, "body_minimal",
"body minimal representation of the dual rail encoding of the "
"preprocessed CNF is computed. Its bodies are used as an "
"initial list of negative examples."}});
SUBool::PCLearnComp::PCLearnComp(CNF cnf, Config conf)
: AbsComp(cnf, conf.minimize_method, conf.impl_system),
......@@ -174,9 +193,8 @@ SUBool::PCLearnComp::PrintStatistics(unsigned level) const
{
logs.TLog(4) << "Final negatives list:" << std::endl;
const auto &comp = mHypothesis.Compressor();
mNegatives.PrettyPrint(std::cout, [&comp](const Literal &lit) {
return comp.UncompressLiteral(lit);
});
mNegatives.PrettyPrint(std::cout,
[&comp](const Literal &lit) { return comp.UncompressLiteral(lit); });
logs.TLog(4) << "Final negatives clauses:" << std::endl;
std::cout << comp.UncompressCNF(dual_rail_to_cnf(mNegatives))
<< std::endl;
......@@ -241,9 +259,9 @@ SUBool::PCLearnComp::PrintStatistics(unsigned level) const
<< mSemanticClosureCount << std::endl;
double avg_semantic_closure_solve_count =
(mSemanticClosureCount > 0
? static_cast<double>(mSemanticClosureSolveCount)
/ static_cast<double>(mSemanticClosureCount)
: 0.0);
? static_cast<double>(mSemanticClosureSolveCount)
/ static_cast<double>(mSemanticClosureCount)
: 0.0);
logs.TLog(level)
<< "Average number of SAT calls in semantic closure computations: "
<< avg_semantic_closure_solve_count << std::endl;
......@@ -294,9 +312,8 @@ SUBool::PCLearnComp::MoveNegativesToCandidates(std::vector<LitImpl> negatives)
logs.TLog(4) << "Initial negatives list:" << std::endl;
const auto &comp = mHypothesis.Compressor();
LitImplSystem negatives_is(negatives);
negatives_is.PrettyPrint(std::cout, [&comp](const Literal &lit) {
return comp.UncompressLiteral(lit);
});
negatives_is.PrettyPrint(std::cout,
[&comp](const Literal &lit) { return comp.UncompressLiteral(lit); });
logs.TLog(4) << "Initial negatives clauses:" << std::endl;
std::cout << comp.UncompressCNF(dual_rail_to_cnf(negatives_is))
<< std::endl;
......@@ -321,7 +338,7 @@ SUBool::PCLearnComp::InitialCandidatesList()
return InitialCandidatesBodyMinimal();
default:
throw BadParameterException("PCLearnComp::InitialCandidatesList",
"Unknown INITIAL_NEGATIVES value");
"Unknown INITIAL_NEGATIVES value");
}
}
......@@ -350,10 +367,10 @@ SUBool::PCLearnComp::InitialCandidatesEmpowering(bool collect_all)
}
std::vector<LitImpl> negatives;
for (const auto &clause_we :
mHypothesis.MinimizeReprWithCollectingEmpowered(collect_all))
mHypothesis.MinimizeReprWithCollectingEmpowered(collect_all))
{
add_proto_negatives_of_clause(negatives, clause_we.clause,
clause_we.empowered);
add_proto_negatives_of_clause(
negatives, clause_we.clause, clause_we.empowered);
}
return RemoveDuplicitiesInNegatives(std::move(negatives));
}
......@@ -408,8 +425,8 @@ SUBool::PCLearnComp::RemoveDuplicitiesInNegatives(
CPUTime cpu_time;
logs.TLog(3) << "Removing duplicities in negatives" << std::endl;
std::sort(negatives.begin(), negatives.end(), ImplBodyCompare<Literal>());
auto end = std::unique(negatives.begin(), negatives.end(),
ImplEqualBody<Literal>());
auto end = std::unique(
negatives.begin(), negatives.end(), ImplEqualBody<Literal>());
logs.TLog(3) << "Resizing negatives from " << negatives.size() << " to "
<< end - negatives.begin() << std::endl;
negatives.resize(end - negatives.begin());
......@@ -504,8 +521,7 @@ SUBool::PCLearnComp::UpdateClosureWithMinimizing(LitImpl &neg)
}
if (body.empty())
{
throw InvariantFailedException(
"PCLearnComp::UpdateClosureWithMinimizing",
throw InvariantFailedException("PCLearnComp::UpdateClosureWithMinimizing",
"Unit or empty implicate found, should not happen at this stage");
}
neg = LitImpl(body, *beta, true);
......@@ -559,7 +575,7 @@ SUBool::PCLearnComp::NextNegativeExample()
++mCandidatesWithClosureCount;
logs.TLog(3) << "... "
<< NEPrinter(mHypothesis.Compressor(),
mCandidatesWithClosure.top(), false)
mCandidatesWithClosure.top(), false)
<< std::endl;
neg = CheckNegativeWithBodyUpdate(mCandidatesWithClosure.top());
if (neg)
......@@ -578,7 +594,7 @@ SUBool::PCLearnComp::NextNegativeExample()
{
logs.TLog(3) << "Have a candidate without closure "
<< NEPrinter(mHypothesis.Compressor(),
mCandidatesWithoutClosure.top(), false)
mCandidatesWithoutClosure.top(), false)
<< std::endl;
++mCandidatesWithoutClosureCount;
auto e =
......@@ -796,8 +812,8 @@ SUBool::PCLearnComp::AddNegativesForEmpowering(const Clause &clause)
{
logs.Log(2) << " " << emp_lit;
std::vector<Literal> body;
std::remove_copy(c->begin(), c->end(), std::back_inserter(body),
emp_lit.Negation());
std::remove_copy(
c->begin(), c->end(), std::back_inserter(body), emp_lit.Negation());
mCandidatesWithoutClosure.push(LitImpl(body, {}, true));
}
logs.Log(2) << std::endl;
......@@ -828,8 +844,8 @@ SUBool::PCLearnComp::Refine(const LitImpl &e)
mCandidatesWithClosure.push(e);
AddNegativeToHypothesis(*neg);
logs.TLog(3) << "Refining "
<< NEPrinter(mHypothesis.Compressor(), mNegatives.At(i),
false)
<< NEPrinter(
mHypothesis.Compressor(), mNegatives.At(i), false)
<< " to "
<< NEPrinter(mHypothesis.Compressor(), *neg, false)
<< std::endl;
......
......@@ -22,6 +22,7 @@
#include "comp_hypothesis.h"
#include "cpuutil.h"
#include "empower.h"
#include "enum.h"
#include "impl_system.h"
#include "implic_learn.h"
#include "pcchecker.h"
......@@ -43,10 +44,8 @@ namespace SUBool
Last = BODY_MINIMAL
};
static const std::array<
std::string,
static_cast<size_t>(SUBool::PCLearnComp::INITIAL_NEGATIVES::Last) + 1>
cInitialNegativesNames;
static const EnumAnnotation<INITIAL_NEGATIVES>
kInitialNegativesAnnotation;
struct Config : public BaseConfig
{
......@@ -123,29 +122,29 @@ namespace SUBool
std::vector<LitImpl> InitialCandidatesGDBasis();
std::vector<LitImpl> InitialCandidatesBodyMinimal();
std::vector<LitImpl>
ComputeClosuresOfNegatives(std::vector<LitImpl> negatives);
std::vector<LitImpl> ComputeClosuresOfNegatives(
std::vector<LitImpl> negatives);
void SortNegatives();
std::optional<LitImpl> NextNegativeExample();
bool Refine(const LitImpl &e);
std::optional<LitImpl> TryToRefine(const LitImpl &e, const LitImpl &neg);
std::optional<LitImpl> RefinedNegative(std::vector<Literal> hyp_positive,
std::vector<Literal> closure);
std::optional<LitImpl> RefinedNegative(
std::vector<Literal> hyp_positive, std::vector<Literal> closure);
void AddNegativeExample(LitImpl e);
void AddNegativeToHypothesis(const LitImpl &e);
void ConstructHypothesis();
bool UpdateClosureWithMinimizing(LitImpl &neg);
// Returns none if the assumption given by the body is unsatisfiable.
std::optional<std::vector<Literal>>
SemanticClosure(const std::vector<Literal> &body);
std::optional<std::vector<Literal>>
SemanticClosureWithCaching(const std::vector<Literal> &body);
std::optional<std::vector<Literal>>
NegClosure(const std::vector<Literal> &body);
std::optional<LitImpl> UpdateClosureWithCaching(const LitImpl &neg,
bool minimize);
std::vector<LitImpl>
RemoveDuplicitiesInNegatives(std::vector<LitImpl> negatives);
std::optional<std::vector<Literal>> SemanticClosure(
const std::vector<Literal> &body);
std::optional<std::vector<Literal>> SemanticClosureWithCaching(
const std::vector<Literal> &body);
std::optional<std::vector<Literal>> NegClosure(
const std::vector<Literal> &body);
std::optional<LitImpl> UpdateClosureWithCaching(
const LitImpl &neg, bool minimize);
std::vector<LitImpl> RemoveDuplicitiesInNegatives(
std::vector<LitImpl> negatives);
// Check whether it is still negative
bool CheckNegativeExample(const LitImpl &neg);
std::optional<LitImpl> CheckNegativeWithBodyUpdate(const LitImpl &neg);
......@@ -157,8 +156,8 @@ namespace SUBool
bool CheckPCWithSAT();
// return value determines if the clause was empowering
bool AddNegativesForEmpowering(const Clause &clause);
std::optional<NECache::const_iterator>
CachedClosure(const std::vector<Literal> &body) const;
std::optional<NECache::const_iterator> CachedClosure(
const std::vector<Literal> &body) const;
bool HasNegative();
......
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