Skip to content

GitLab

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

One provability options of pccompile

parent d9df191c
Hide whitespace changes
Inline Side-by-side
bin/pccheck.cpp
View file @ c7755637
......@@ -52,7 +52,7 @@ struct config_t
SUBool::PCEncoder::UP_EMPOWER::ONE_LEVEL};
SUBool::AbsEncoder::AbsConfig enc_conf{};
SUBool::AbsCheckerSAT::Timeouts timeouts{};
SUBool::LIT_IMPL_SYSTEM impl_system{SUBool::LIT_IMPL_SYSTEM::NONE};
SUBool::LIT_IMPL_SYSTEM impl_system{SUBool::LIT_IMPL_SYSTEM::Default};
GOAL goal{GOAL::PC};
SUBool::AmoEncoder::KIND amo_encoding{SUBool::AmoEncoder::KIND::REPR};
SUBool::ExOneEncoder::KIND exone_encoding{SUBool::ExOneEncoder::KIND::REPR};
......@@ -89,11 +89,13 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level) << "\tinput_file: " << conf.input_file << std::endl;
SUBool::logs.TLog(level)
<< "\toutput_file: " << conf.output_file << std::endl;
SUBool::logs.DumpVerbosity("\t", level);
SUBool::logs.TLog(level)
<< "\tencode_only: " << SUBool::bool_to_string(conf.encode_only)
<< std::endl;
SUBool::logs.DumpValue("\t", level, "no_up_backbones", conf.no_up_backbones);
SUBool::kLitImplSystemAnnotation.DumpValue(
"\t", level, "impl_system", conf.impl_system);
SUBool::PCEncoder::kUPEmpowerAnnotation.DumpValue(
"\t", level, "up_empower", conf.up_empower);
SUBool::logs.TLog(level) << "\tenc_conf:" << std::endl;
......@@ -105,8 +107,8 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level)
<< "\ttimeouts.level_factor: " << conf.timeouts.level_factor
<< std::endl;
SUBool::dump_enum_value(
"\t", level, "impl_system", conf.impl_system, SUBool::kImplSystemNames);
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);
......
bin/pccompile.cpp
View file @ c7755637
......@@ -65,7 +65,7 @@ struct config_t
SUBool::AbsEncoder::AbsConfig(),
SUBool::AbsCheckerSAT::Timeouts(),
true,
SUBool::LIT_IMPL_SYSTEM::NONE,
SUBool::LIT_IMPL_SYSTEM::Default,
SUBool::SOLVER_TYPE::GLUCOSE,
};
bool unfinished_write{true};
......@@ -102,12 +102,15 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level) << "\tinput_file: " << conf.input_file << std::endl;
SUBool::logs.TLog(level)
<< "\toutput_file: " << conf.output_file << std::endl;
SUBool::logs.DumpVerbosity("\t", level);
SUBool::logs.TLog(level)
<< "\tminimize: " << SUBool::bool_to_string(conf.minimize) << std::endl;
SUBool::kMinimizeMethodAnnotation.DumpValue(
"\t", level, "minimize_method", conf.comp_base_config.minimize_method);
SUBool::PCCompAlgorithmOptions::kAlgorithmAnnotation.DumpValue(
"\t", level, "algorithm", conf.algorithm);
SUBool::kLitImplSystemAnnotation.DumpValue(
"\t", level, "impl_system", conf.comp_base_config.impl_system);
SUBool::PCEncoder::kUPEmpowerAnnotation.DumpValue("\t", level,
"comp_base_config.up_empower", conf.comp_base_config.up_empower);
SUBool::logs.TLog(level)
......@@ -119,9 +122,8 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level)
<< "\tlevel_simplify: " << (conf.level_simplify ? "yes" : "no")
<< std::endl;
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::kLitImplSystemAnnotation.DumpValue("\t", level,
"comp_base_config.impl_system", conf.comp_base_config.impl_system);
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",
......@@ -206,12 +208,12 @@ parse_arguments(int argc, char *argv[], config_t &conf)
opts.MakeOptionsGroup<SUBool::PCCompPreprocessOptions>();
auto solver_opts = opts.MakeOptionsGroup<SUBool::PCSolverOptions>();
auto empower_opts = opts.MakeOptionsGroup<SUBool::PCEmpowerOptions>();
auto oneprove_opts = opts.MakeOptionsGroup<SUBool::PCOneProveOptions>();
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();
......@@ -220,6 +222,12 @@ parse_arguments(int argc, char *argv[], config_t &conf)
!preprocess_opts->NoBackbonePropagation();
conf.comp_base_config.solver_type = solver_opts->SolverType();
conf.comp_base_config.up_empower = empower_opts->Empower();
conf.comp_base_config.enc_conf.up_one_prove = oneprove_opts->OneProve();
conf.comp_base_config.enc_conf.up_level_bound =
oneprove_opts->UPLevelBound();
conf.comp_base_config.enc_conf.log_conf =
oneprove_opts->EncLogarithmicConf();
conf.comp_base_config.impl_system = oneprove_opts->ImplSystem();
return 0;
#if 0
try
......
bin/pcminimize.cpp
View file @ c7755637
......@@ -187,7 +187,7 @@ minimize(const config_t &conf, SUBool::CNF cnf)
{
SUBool::CPUTime cpu_time;
SUBool::CompHypothesis hyp(conf.minimize_method,
SUBool::LIT_IMPL_SYSTEM::NONE, SUBool::CNF(), std::move(cnf), false);
SUBool::LIT_IMPL_SYSTEM::Default, SUBool::CNF(), std::move(cnf), false);
if (conf.backbones
&& !run_with_timeout(
conf.timeout < 0.0f, conf.timeout - cpu_time.TimeSpan(),
......
lib/abscomp.h
View file @ c7755637
......@@ -78,7 +78,7 @@ namespace SUBool
AbsEncoder::AbsConfig enc_conf{};
AbsCheckerSAT::Timeouts timeouts{};
bool level_simplify{true};
LIT_IMPL_SYSTEM impl_system{LIT_IMPL_SYSTEM::NONE};
LIT_IMPL_SYSTEM impl_system{LIT_IMPL_SYSTEM::Default};
SOLVER_TYPE solver_type{SOLVER_TYPE::GLUCOSE};
};
......
lib/absenc.cpp
View file @ c7755637
......@@ -22,6 +22,36 @@
#include "up_scc_binary.h"
#include "up_scc_unary.h"
const SUBool::EnumAnnotation<SUBool::AbsEncoder::UP_ONE_PROVE>
SUBool::AbsEncoder::kUPOneProveAnnotation("UP_ONE_PROVE",
{//
{UP_ONE_PROVE::QUADRATIC_EQUIV, "quadratic_equiv",
"quadratic encoding with equivalences."}, //
{UP_ONE_PROVE::QUADRATIC_ONE_SIDED, "quadratic_one_sided",
"quadratic encoding with implications."}, //
{UP_ONE_PROVE::LOGARITHMIC, "logarithmic",
"based on encoding levels of unit propagations with binary "
"encoding (logarithmic size)"}, //
{UP_ONE_PROVE::MAX_LEVEL, "max_level",
"encoding based on determining a maximum level of a literal in "
"a clause"}, //
{UP_ONE_PROVE::MIN_LQ, "min_lq",
"each time, pick the smaller one from the quadratic encoding "
"with implications (quadratic_one_sided) and the logarithmic "
"encoding (logarithmic)"}, //
{UP_ONE_PROVE::QUAD_IMPL_SYSTEM, "quad_impl_system",
"quadratic encoding which uses an implication system to "
"represent the dual rail encoding."}, //
{UP_ONE_PROVE::IMPL_LEVEL, "impl_level",
"encoding based on an implication system where levels are "
"encoded in binary."}, //
{UP_ONE_PROVE::SCC_UNARY, "scc_unary",
"encoding based on the strongly connected components (SCC) of "
"an implication system with unary encoding of levels."}, //
{UP_ONE_PROVE::SCC_BINARY, "scc_binary",
"encoding based on the strongly connected components (SCC) of "
"an implication system with binary encoding of levels."}});
SUBool::AbsEncoder::AbsEncoder(const AbsConfig &conf)
: mVarStore(conf.use_backmap), mClauses(), mOneProveEncoder(),
mCnfMaxVariable(0), mMaxUPLevelBound(0)
......@@ -198,9 +228,8 @@ void
SUBool::AbsEncoder::AbsConfig::Dump(
const std::string &line_prefix, unsigned level) const
{
logs.DumpValue(line_prefix, level, "up_one_prove",
AbsEncoder::kUPOneProveNames.at(static_cast<unsigned>(up_one_prove))
+ " (" + std::to_string(static_cast<unsigned>(up_one_prove)) + ")");
kUPOneProveAnnotation.DumpValue(
line_prefix, level, "up_one_prove", up_one_prove);
logs.DumpValue(line_prefix, level, "optimize", optimize);
logs.DumpValue(line_prefix, level, "up_level_bound", up_level_bound);
logs.DumpValue(line_prefix, level, "use_backmap", use_backmap);
......@@ -211,16 +240,3 @@ SUBool::AbsEncoder::AbsConfig::Dump(
line_prefix, level, "min_lq_quad_weights", min_lq_quad_weights);
}
auto
SUBool::AbsEncoder::ParseUPOneProve(const std::string &up_one_prove)
-> UP_ONE_PROVE
{
if (isdigit(up_one_prove.front()))
{
return enum_of_int<SUBool::AbsEncoder::UP_ONE_PROVE>(
std::stol(up_one_prove));
}
return enum_of_name<SUBool::AbsEncoder::UP_ONE_PROVE>(
up_one_prove, SUBool::AbsEncoder::kUPOneProveNames);
}
lib/absenc.h
View file @ c7755637
......@@ -16,6 +16,7 @@
#include "cardinal.h"
#include "cl2lit.h"
#include "enum.h"
#include "glucose_bind.h"
#include "impl_system.h"
#include "impl_system_graph.h"
......@@ -40,8 +41,7 @@ namespace SUBool
QUAD_IMPL_SYSTEM,
IMPL_LEVEL,
SCC_UNARY,
SCC_BINARY,
Last = SCC_BINARY
SCC_BINARY
};
struct UPOneProveTraits
......@@ -51,26 +51,19 @@ namespace SUBool
bool requires_scc_graph;
};
inline static const std::array<
UPOneProveTraits, static_cast<unsigned>(UP_ONE_PROVE::Last) + 1>
kUPOneProveTraits = {
UPOneProveTraits{UP_ONE_PROVE::QUADRATIC_EQUIV, false, false},
UPOneProveTraits{UP_ONE_PROVE::QUADRATIC_ONE_SIDED, false, false},
UPOneProveTraits{UP_ONE_PROVE::LOGARITHMIC, false, false},
UPOneProveTraits{UP_ONE_PROVE::MAX_LEVEL, false, false},
UPOneProveTraits{UP_ONE_PROVE::MIN_LQ, false, false},
UPOneProveTraits{UP_ONE_PROVE::QUAD_IMPL_SYSTEM, true, false},
UPOneProveTraits{UP_ONE_PROVE::IMPL_LEVEL, true, false},
UPOneProveTraits{UP_ONE_PROVE::SCC_UNARY, true, true},
UPOneProveTraits{UP_ONE_PROVE::SCC_BINARY, true, true}};
inline static const std::array<
std::string, static_cast<unsigned>(UP_ONE_PROVE::Last) + 1>
kUPOneProveNames = {"quadratic_equiv", "quadratic_one_sided",
"logarithmic", "max_level",
"min_lq", "quad_impl_system",
"impl_level", "scc_unary",
"scc_binary"};
inline static const std::array kUPOneProveTraits{
UPOneProveTraits{UP_ONE_PROVE::QUADRATIC_EQUIV, false, false},
UPOneProveTraits{UP_ONE_PROVE::QUADRATIC_ONE_SIDED, false, false},
UPOneProveTraits{UP_ONE_PROVE::LOGARITHMIC, false, false},
UPOneProveTraits{UP_ONE_PROVE::MAX_LEVEL, false, false},
UPOneProveTraits{UP_ONE_PROVE::MIN_LQ, false, false},
UPOneProveTraits{UP_ONE_PROVE::QUAD_IMPL_SYSTEM, true, false},
UPOneProveTraits{UP_ONE_PROVE::IMPL_LEVEL, true, false},
UPOneProveTraits{UP_ONE_PROVE::SCC_UNARY, true, true},
UPOneProveTraits{UP_ONE_PROVE::SCC_BINARY, true, true}};
static const EnumAnnotation<UP_ONE_PROVE> kUPOneProveAnnotation;
static UP_ONE_PROVE ParseUPOneProve(const std::string &up_one_prove);
struct AbsConfig
......@@ -95,8 +88,8 @@ namespace SUBool
AbsConfig(AbsConfig &&conf) = default;
AbsConfig &operator=(const AbsConfig &conf) = default;
AbsConfig &operator=(AbsConfig &&conf) = default;
virtual void Dump(const std::string &line_prefix,
unsigned level) const;
virtual void Dump(
const std::string &line_prefix, unsigned level) const;
static constexpr bool
OneProveRequiresImplSystem(UP_ONE_PROVE op)
{
......@@ -119,25 +112,23 @@ namespace SUBool
unsigned mMaxUPLevelBound;
virtual void InitOneProveEncoder(const CNF &cnf,
const ClausesToLiterals &cl2lit,
const LitImplSystem &impl_system,
const LitISGraph &scc_graph);
const ClausesToLiterals &cl2lit, const LitImplSystem &impl_system,
const LitISGraph &scc_graph);
virtual void WriteHeader(std::ostream &out) const;
virtual std::string Name() const = 0;
virtual void WriteMappingsOfVariable(std::ostream &out, unsigned i) const;
virtual void WriteClause(std::ostream &out, const Clause &clause) const;
virtual void AddClauses(const CNF &cnf, const ClausesToLiterals &cl2lit,
const LitImplSystem &impl_system) = 0;
const LitImplSystem &impl_system) = 0;
virtual const AbsConfig &GetConfig() const = 0;
public:
AbsEncoder(const AbsConfig &conf = AbsConfig());
virtual ~AbsEncoder() = default;
virtual void BuildEncoding(const CNF &cnf,
const ClausesToLiterals &cl2lit,
const LitImplSystem &impl_system,
const LitISGraph &scc_graph);
const ClausesToLiterals &cl2lit, const LitImplSystem &impl_system,
const LitISGraph &scc_graph);
virtual unsigned MaxVariable() const;
virtual unsigned Size() const;
......@@ -146,14 +137,12 @@ namespace SUBool
virtual bool RequiresSCCGraph() const;
virtual unsigned MaxUPLevelBound() const;
virtual unsigned NextUPLevelBound(const CNF &cnf,
const ClausesToLiterals &cl2lit,
const LitImplSystem &impl_system,
const LitISGraph &scc_graph,
unsigned level);
const ClausesToLiterals &cl2lit, const LitImplSystem &impl_system,
const LitISGraph &scc_graph, unsigned level);
// The meaning of the return value depends on descendant,
// in any case it returns a witness variable (e.g. empowered)
virtual unsigned ExtractClause(const SolverInterface &solver,
Clause *clause) const = 0;
virtual unsigned ExtractClause(
const SolverInterface &solver, Clause *clause) const = 0;
virtual bool PassToSolver(SolverInterface &solver) const;
virtual void WriteEncoding(std::ostream &out) const;
......
lib/comp_hypothesis.h
View file @ c7755637
......@@ -34,7 +34,7 @@ namespace SUBool
bool mHypSimplified{false};
bool mReprSimplified{false};
MINIMIZE_METHOD mMinimizeMethod{MINIMIZE_METHOD::FULL};
LIT_IMPL_SYSTEM mImplSystemKind{kDefaultImplSystem};
LIT_IMPL_SYSTEM mImplSystemKind{LIT_IMPL_SYSTEM::Default};
std::vector<Literal> mBackbone{};
CNFCompressor mCompressor{};
LitImplSystem mImplSystem{};
......@@ -67,11 +67,10 @@ namespace SUBool
public:
static const unsigned kSimpLogThreshold = 3000;
CompHypothesis(
MINIMIZE_METHOD minimize_method, LIT_IMPL_SYSTEM impl_system_kind);
CompHypothesis(MINIMIZE_METHOD minimize_method,
LIT_IMPL_SYSTEM impl_system_kind);
CompHypothesis(MINIMIZE_METHOD minimize_method,
LIT_IMPL_SYSTEM impl_system_kind, CNF cnf, CNF repr,
bool safe);
LIT_IMPL_SYSTEM impl_system_kind, CNF cnf, CNF repr, bool safe);
~CompHypothesis() = default;
void ClearHypothesis();
......@@ -109,17 +108,17 @@ namespace SUBool
void SetSafe();
bool Safe() const;
std::optional<PartialAssignment>
PropagateUP(const PartialAssignment &alpha);
std::optional<PartialAssignment>
PropagateAllSAT(const PartialAssignment &alpha); // const;
std::optional<std::vector<Literal>>
AllEmpoweredLiterals(const Clause &clause);
std::optional<PartialAssignment> PropagateUP(
const PartialAssignment &alpha);
std::optional<PartialAssignment> PropagateAllSAT(
const PartialAssignment &alpha); // const;
std::optional<std::vector<Literal>> AllEmpoweredLiterals(
const Clause &clause);
std::optional<Literal> EmpoweredLiteral(const Clause &clause);
bool SimplifyHypothesis(); // true if simplification executed
bool SimplifyRepresentation(); // true if simplification executed
std::vector<ClauseWithEmpowered>
MinimizeReprWithCollectingEmpowered(bool collect_all);
std::vector<ClauseWithEmpowered> MinimizeReprWithCollectingEmpowered(
bool collect_all);
const CNFCompressor &
Compressor() const
{
......@@ -132,11 +131,10 @@ namespace SUBool
bool IsEmpowering(const Clause &c);
bool IsImplicate(const Clause &clause) const;
std::optional<Clause> PrimeSubimplicate(const Clause &clause,
unsigned ignore_var,
bool promised_sat) const;
std::optional<Clause> FindEmpowering(AbsCheckerSAT &checker,
bool level_simplify);
std::optional<Clause> PrimeSubimplicate(
const Clause &clause, unsigned ignore_var, bool promised_sat) const;
std::optional<Clause> FindEmpowering(
AbsCheckerSAT &checker, bool level_simplify);
void PushBack(Clause c);
// Returns true if pushed
bool PushIfEmpowering(const Clause &c, bool find_prime_subimplicate);
......
lib/drenc.cpp
View file @ c7755637
......@@ -9,25 +9,27 @@
#include "drenc.h"
const std::array<std::string,
static_cast<unsigned>(SUBool::LIT_IMPL_SYSTEM::Last) + 1>
SUBool::kImplSystemNames = {"none",
"drenc",
"irredundant",
"gdbasis",
"gdbasis_right_irred",
"body_minimal",
"body_minimal_irred"};
const SUBool::LIT_IMPL_SYSTEM SUBool::kDefaultImplSystem =
SUBool::LIT_IMPL_SYSTEM::BODY_MINIMAL_IRRED;
const SUBool::EnumAnnotation<SUBool::LIT_IMPL_SYSTEM>
SUBool::kLitImplSystemAnnotation("LIT_IMPL_SYSTEM",
{ //
{LIT_IMPL_SYSTEM::DRENC, "drenc", "plain dual rail encoding"}, //
{LIT_IMPL_SYSTEM::IRREDUNDANT, "irredundant",
"make the dual rail encoding irredundant (both body and right "
"irredundant)"}, //
{LIT_IMPL_SYSTEM::GDBASIS, "gdbasis",
"use GD basis of the dual rail encoding."}, //
{LIT_IMPL_SYSTEM::GDBASIS_RIGHT_IRRED, "gdbasis_right_irred",
"construct the GD basis and make it right irredundant."}, //
{LIT_IMPL_SYSTEM::BODY_MINIMAL, "body_minimal",
"make the dual rail encoding body minimal (like GD basis but "
"without left saturation)."}, //
{LIT_IMPL_SYSTEM::BODY_MINIMAL_IRRED, "body_minimal_irred",
"make the dual rail encoding body minimal and right "
"irredundant."}});
SUBool::LitImplSystem
SUBool::init_lit_impl_system(const CNF &cnf, LIT_IMPL_SYSTEM is_kind)
{
if (is_kind == LIT_IMPL_SYSTEM::NONE)
{
return SUBool::LitImplSystem();
}
auto impl_system = dual_rail(cnf, true);
if (is_kind == LIT_IMPL_SYSTEM::GDBASIS
|| is_kind == LIT_IMPL_SYSTEM::GDBASIS_RIGHT_IRRED)
......@@ -53,8 +55,8 @@ SUBool::init_lit_impl_system(const CNF &cnf, LIT_IMPL_SYSTEM is_kind)
}
void
SUBool::append_clause_dual_rail(std::vector<LitImpl> &impl,
const Clause &clause)
SUBool::append_clause_dual_rail(
std::vector<LitImpl> &impl, const Clause &clause)
{
if (clause.Empty())
{
......@@ -63,12 +65,12 @@ SUBool::append_clause_dual_rail(std::vector<LitImpl> &impl,
std::vector<Literal> body(clause.Size() - 1);
for (size_t i = 0; i < clause.Size(); ++i)
{
if (std::remove_copy(clause.cbegin(), clause.cend(), body.begin(),
clause[i])
if (std::remove_copy(
clause.cbegin(), clause.cend(), body.begin(), clause[i])
!= body.end())
{
throw BadParameterException("append_clause_dual_rail",
"two equal literals");
throw BadParameterException(
"append_clause_dual_rail", "two equal literals");
}
std::for_each(body.begin(), body.end(), [](auto &lit) { lit.Negate(); });
impl.push_back(LitImpl(body, {clause[i]}, true));
......@@ -92,8 +94,8 @@ SUBool::dual_rail(const CNF &cnf, bool merge_bodies)
}
void
SUBool::append_clauses_of_impl(std::vector<Clause> &clauses,
const LitImpl &impl)
SUBool::append_clauses_of_impl(
std::vector<Clause> &clauses, const LitImpl &impl)
{
LitImpl simple_impl = impl;
simple_impl.MakeConsWithoutBody();
......
lib/drenc.h
View file @ c7755637
......@@ -9,6 +9,7 @@
#ifndef __DRENC_H
#define __DRENC_H
#include "enum.h"
#include "impl_system.h"
#include "normalform.h"
......@@ -16,34 +17,24 @@ namespace SUBool
{
enum class LIT_IMPL_SYSTEM
{
NONE,
DRENC,
IRREDUNDANT, // left+right
GDBASIS,
GDBASIS_RIGHT_IRRED,
BODY_MINIMAL,
BODY_MINIMAL_IRRED,
Last = BODY_MINIMAL_IRRED
Default = BODY_MINIMAL_IRRED
};
extern const std::array<std::string,
static_cast<unsigned>(LIT_IMPL_SYSTEM::Last) + 1>
kImplSystemNames;
extern const LIT_IMPL_SYSTEM kDefaultImplSystem;
inline const std::string &
DefaultImplSystemName()
{
return kImplSystemNames[static_cast<unsigned>(kDefaultImplSystem)];
}
extern const EnumAnnotation<LIT_IMPL_SYSTEM> kLitImplSystemAnnotation;
LitImplSystem init_lit_impl_system(const CNF &cnf, LIT_IMPL_SYSTEM is_kind);
void append_clause_dual_rail(std::vector<LitImpl> &impl,
const Clause &clause);
void append_clause_dual_rail(
std::vector<LitImpl> &impl, const Clause &clause);
LitImplSystem dual_rail(const CNF &cnf, bool merge_bodies);
void append_clauses_of_impl(std::vector<Clause> &clauses,
const LitImpl &impl);
void append_clauses_of_impl(
std::vector<Clause> &clauses, const LitImpl &impl);
CNF dual_rail_to_cnf(const LitImplSystem &is);
std::vector<Clause> dr_clauses_of_impl(const LitImpl &impl);
......
lib/pc_opt.cpp
View file @ c7755637
......@@ -119,3 +119,74 @@ SUBool::PCEmpowerOptions::GetValues()
{
return mEmpowerOption.GetValue(mEmpower);
}
SUBool::PCOneProveOptions::PCOneProveOptions()
: OptionsGroup("1-Provability Encoding"),
mOneProveOption(AbsEncoder::kUPOneProveAnnotation, "one-prove,1",
"The kind of encoding used to encode 1-provability",
kDefaultOneProve),
mImplSystemOption(kLitImplSystemAnnotation, "impl-system",
"Determines the type of an implication system to be used if needed "
"by encoding of empowerement or 1-provability.",
kDefaultLitImplSystem)
{
Add(mOneProveOption);
Add(mImplSystemOption);
AddOptions()("level,l",
po::value<unsigned>(&mUPLevelBound)->default_value(mUPLevelBound),
"Maximum level of unit propagation for 1-provability. This is the "
"maximum level used when checking propagation or unit refutation "
"completeness by SAT. Value 0 means, the level is not bounded.") //
("log-enc-opts",
po::value<std::string>(&mLogEncOpts)
->default_value(kDefaultLogEncOpts),
"Options specifying some of the features of the logarithmic "
"encoding. It is a string composed of comma separated option "
"strings which specifies which additional parts should be added to "
"the encoding. Possible values specifying the features are:\n"
"amf -- AMO on fire variables for each derived literal will be part "
"of the encoding.\n"
"cex -- Comparison exclusivity clauses will be added to the "
"encoding.\n"
"flm -- Clauses forcing linear order when the number of levels is "
"maximum will be added to the encoding.\n"
"cml -- A variable is contradictory if and only its level has all "
"ones.");
}
bool
SUBool::PCOneProveOptions::GetValues()
{
return mOneProveOption.GetValue(mOneProve)
&& mImplSystemOption.GetValue(mImplSystem) && ParseLogEncOpts();
}
bool
SUBool::PCOneProveOptions::ParseLogEncOpts()
{
std::vector<bool> opt_values(kLogEncOptsNames.size(), false);
size_t start = 0;
size_t end = 0;
if (!mLogEncOpts.empty())
{
while (start != std::string::npos)
{
end = mLogEncOpts.find_first_of(',', start);
auto i = std::find(kLogEncOptsNames.begin(), kLogEncOptsNames.end(),
mLogEncOpts.substr(start, end - start));
if (i == kLogEncOptsNames.end())
{
logs.Log(0) << "Error parsing the value of option --log-enc-opts"
<< std::endl;
return false;
}
opt_values[i - kLogEncOptsNames.begin()] = true;
start = end + static_cast<size_t>(end < std::string::npos);
}
}
mEncLogarithmicConf.add_amo_on_fire_vars = opt_values[0];
mEncLogarithmicConf.add_compare_exclusivity = opt_values[1];
mEncLogarithmicConf.add_force_linear_order_on_max_level = opt_values[2];
mEncLogarithmicConf.contradiction_has_max_level = opt_values[3];
return true;
}
lib/pc_opt.h
View file @ c7755637
......@@ -9,6 +9,7 @@
#ifndef __PC_OPT_H
#define __PC_OPT_H
#include "drenc.h"
#include "empower.h"
#include "enum_opt.h"
#include "pclearncomp.h"
......@@ -125,6 +126,39 @@ namespace SUBool
PCEncoder::UP_EMPOWER Empower() const;
};
class PCOneProveOptions : public OptionsGroup
{
public:
static constexpr AbsEncoder::UP_ONE_PROVE kDefaultOneProve =
AbsEncoder::UP_ONE_PROVE::SCC_UNARY;
static constexpr LIT_IMPL_SYSTEM kDefaultLitImplSystem =
LIT_IMPL_SYSTEM::Default;
static constexpr std::array kLogEncOptsNames{"amf", "cex", "flm", "cml"};
inline static const std::string kDefaultLogEncOpts{"amf,cex,flm,cml"};
private:
EnumOption<AbsEncoder::UP_ONE_PROVE> mOneProveOption;
std::string mLogEncOpts{};
EnumOption<LIT_IMPL_SYSTEM> mImplSystemOption;
unsigned mUPLevelBound{0};
UPEncLogarithmic::Config mEncLogarithmicConf{};
AbsEncoder::UP_ONE_PROVE mOneProve{kDefaultOneProve};
LIT_IMPL_SYSTEM mImplSystem{kDefaultLitImplSystem};
bool ParseLogEncOpts();
public: