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

Reworked solver related options

parent 8c1e6682
......@@ -53,7 +53,6 @@ struct config_t : public SUBool::PrgConfigBase
SUBool::PCCheckGeneralOptions::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};
virtual void InnerDump(unsigned level) const override;
};
......@@ -61,6 +60,7 @@ struct config_t : public SUBool::PrgConfigBase
void
config_t::InnerDump(unsigned level) const
{
SUBool::SolverPool::DumpSolverTypes("\t", level);
SUBool::logs.DumpValue("\t", level, "input_file", input_file);
SUBool::PCCheckGeneralOptions::kGoalAnnotation.DumpValue(
"\t", level, "goal", goal);
......@@ -83,8 +83,6 @@ config_t::InnerDump(unsigned level) const
"\t", level, "amo_encoding", amo_encoding);
SUBool::ExOneEncoder::kKindAnnotation.DumpValue(
"\t", level, "exone_encoding", exone_encoding);
SUBool::kSolverTypeAnnotation.DumpValue(
"\t", level, "solver_type", solver_type);
}
std::optional<config_t>
......@@ -113,7 +111,6 @@ parse_arguments(int argc, char *argv[])
conf.enc_conf.use_backmap = general_opts->Dump();
conf.no_up_backbones = general_opts->NoUPBackbones();
conf.initial_up_level = general_opts->InitialUPLevel();
conf.solver_type = solver_opts->SolverType();
conf.enc_conf.up_one_prove = oneprove_opts->OneProve();
conf.enc_conf.up_level_bound = oneprove_opts->UPLevelBound();
conf.enc_conf.log_conf = oneprove_opts->EncLogarithmicConf();
......@@ -205,7 +202,6 @@ pc_checker_sat(const config_t &conf)
auto checker = std::make_unique<SUBool::PCCheckerSAT>();
SUBool::PCEncoder::Config check_conf(conf.enc_conf);
checker->Init(check_conf, false, conf.timeouts, conf.initial_up_level);
checker->SetSolverType(conf.solver_type);
return checker;
}
......@@ -214,7 +210,6 @@ urc_checker_sat(const config_t &conf)
{
auto checker = std::make_unique<SUBool::UCCheckerSAT>();
checker->Init(conf.enc_conf, false, conf.timeouts);
checker->SetSolverType(conf.solver_type);
return checker;
}
......
......@@ -73,6 +73,7 @@ config_t the_conf;
void
config_t::InnerDump(unsigned level) const
{
SUBool::SolverPool::DumpSolverTypes("\t", level);
SUBool::logs.DumpValue("\t", level, "input_file", input_file);
SUBool::logs.DumpValue("\t", level, "output_file", output_file);
SUBool::logs.DumpValue("\t", level, "minimize", minimize);
......@@ -117,8 +118,6 @@ config_t::InnerDump(unsigned level) const
comp_base_config.timeouts.level_base);
SUBool::logs.DumpValue("\t", level, "comp_base_config.timeouts.level_factor",
comp_base_config.timeouts.level_factor);
SUBool::kSolverTypeAnnotation.DumpValue("\t", level,
"comp_base_config.solver_type", comp_base_config.solver_type);
SUBool::logs.TLog(level) << "\tenc_conf:" << std::endl;
comp_base_config.enc_conf.Dump("\t\t", level);
SUBool::AmoEncoder::kKindAnnotation.DumpValue(
......@@ -159,7 +158,6 @@ parse_arguments(int argc, char *argv[], config_t &conf)
conf.comp_base_config.preprocess = preprocess_opts->PreprocessMethod();
conf.comp_base_config.propagate_backbones =
!preprocess_opts->NoBackbonePropagation();
conf.comp_base_config.solver_type = solver_opts->SolverType();
conf.comp_base_config.enc_conf.up_one_prove = oneprove_opts->OneProve();
conf.comp_base_config.enc_conf.up_level_bound =
oneprove_opts->UPLevelBound();
......
......@@ -78,7 +78,6 @@ namespace SUBool
AbsCheckerSAT::Timeouts timeouts{};
bool level_minimize{false};
LIT_IMPL_SYSTEM impl_system{LIT_IMPL_SYSTEM::Default};
SOLVER_TYPE solver_type{SOLVER_TYPE::GLUCOSE};
IMPL_SYSTEM_REBUILD impl_system_rebuild{
IMPL_SYSTEM_REBUILD::CLAUSE_ADDED};
};
......
......@@ -91,7 +91,7 @@ SUBool::clause_falsifying(const Clause &clause, unsigned n)
bool
SUBool::is_implicate(const CNF &cnf, const Clause &clause)
{
auto wrap = solver_wrapper(cnf);
auto wrap = noninc_solver_wrapper(cnf);
return is_implicate(wrap.Solver(), clause);
}
......@@ -206,6 +206,6 @@ SUBool::prime_cnf(
bool
SUBool::is_satisfiable(const CNF &cnf)
{
auto wrap = solver_wrapper(cnf);
auto wrap = noninc_solver_wrapper(cnf);
return wrap.Solver().Solve();
}
......@@ -113,7 +113,7 @@ SUBool::prime_cnf_with_ignore(
inline bool
SUBool::is_consistent(const CNF &cnf, const std::vector<Literal> &assump)
{
auto wrap = solver_wrapper(cnf);
auto wrap = noninc_solver_wrapper(cnf);
auto &g = wrap.Solver();
return g.Solve(assump);
}
......@@ -121,7 +121,7 @@ SUBool::is_consistent(const CNF &cnf, const std::vector<Literal> &assump)
inline bool
SUBool::is_consistent(const CNF &cnf, const PartialAssignment &assump)
{
auto wrap = solver_wrapper(cnf);
auto wrap = noninc_solver_wrapper(cnf);
auto &g = wrap.Solver();
return g.Solve(assump);
}
......@@ -129,7 +129,7 @@ SUBool::is_consistent(const CNF &cnf, const PartialAssignment &assump)
inline bool
SUBool::is_consistent(const CNF &cnf, const Assignment &assump)
{
auto wrap = solver_wrapper(cnf);
auto wrap = noninc_solver_wrapper(cnf);
auto &g = wrap.Solver();
return g.Solve(assump);
}
......
......@@ -79,9 +79,9 @@ SUBool::AbsCheckerSAT::FindEmpoweringWithLevel(const CNF &cnf,
logs.TLog(3) << "[AbsCheckerSAT::FindEmpoweringWithLevel] level="
<< (level == 0 ? mMaxUPLevel : level) << ", input cnf "
<< cnf.MaxVariable() << " " << cnf.Size() << std::endl;
auto wrap = solver_wrapper(
mSolverType, assume_sat ? SolverInterface::ADAPTATION::LIKELY_SAT
: SolverInterface::ADAPTATION::LIKELY_UNSAT);
auto wrap = noninc_solver_wrapper(
assume_sat ? SolverInterface::ADAPTATION::LIKELY_SAT
: SolverInterface::ADAPTATION::LIKELY_UNSAT);
auto &g = wrap.Solver();
enc->PassToSolver(g);
logs.TLog(3) << "... Calling SAT with encoding (p cnf " << enc->MaxVariable()
......
......@@ -43,7 +43,6 @@ namespace SUBool
unsigned mSolveCountSAT{0};
unsigned mSolveCountUNSAT{0};
unsigned mLastWitnessVariable{0};
SOLVER_TYPE mSolverType{SOLVER_TYPE::GLUCOSE};
enum class STATE
{
NO_SPLIT,
......@@ -105,12 +104,6 @@ namespace SUBool
{
mState = STATE::INTERRUPT;
}
void
SetSolverType(SOLVER_TYPE solver_type)
{
mSolverType = solver_type;
}
};
template <class T> class CheckerSATTemplate : public AbsCheckerSAT
......
......@@ -19,7 +19,6 @@ SUBool::PCComp::PCComp(CNF cnf, Config conf)
mCheckerSAT(), mEncConf(conf.enc_conf), mConf(std::move(conf))
{
mCheckerSAT.Init(mEncConf, true, mConf.timeouts);
mCheckerSAT.SetSolverType(mConf.solver_type);
}
const SUBool::AbsComp::BaseConfig &
......
......@@ -107,7 +107,6 @@ SUBool::PCLearnComp::PCLearnComp(CNF cnf, Config conf)
{
mConf.preprocess = AbsComp::PMRemoveMinimize(mConf.preprocess);
mPCCheckerSAT.Init(mConf.EncoderConfig(), true, mConf.timeouts);
mPCCheckerSAT.SetSolverType(mConf.solver_type);
if (mPCCheckerSAT.RequiresImplSystem()
|| mConf.candidates_from_negative_policy
== CANDIDATES_FROM_NEGATIVE_POLICY::SYNCHRONIZE)
......
......@@ -232,13 +232,13 @@ SUBool::PrgConfigBase::Init(unsigned verbosity, unsigned long long seed)
void
SUBool::PrgConfigBase::Dump(unsigned level) const
{
if (!SUBool::logs.CheckLevel(level))
if (!logs.CheckLevel(level))
{
return;
}
SUBool::logs.TLog(level) << "Configuration:" << std::endl;
SUBool::logs.DumpVerbosity("\t", level);
SUBool::logs.DumpValue("\t", level, "seed", mSeed);
logs.TLog(level) << "Configuration:" << std::endl;
logs.DumpVerbosity("\t", level);
logs.DumpValue("\t", level, "seed", mSeed);
InnerDump(level);
SUBool::logs.TLog(level) << "END" << std::endl;
logs.TLog(level) << "END" << std::endl;
}
......@@ -230,7 +230,7 @@ SUBool::propagate_core_chunk(const CNF &cnf, PartialAssignment alpha,
}
while (true)
{
auto wrap = solver_wrapper(cnf);
auto wrap = noninc_solver_wrapper(cnf);
auto &g = wrap.Solver();
g.AddClauses(units);
omega_lits.assign(omega.begin(), omega.end());
......@@ -297,7 +297,7 @@ SUBool::propagate_iterative(const CNF &cnf, PartialAssignment alpha,
std::copy_n(free_lits.begin(), std::min(free_lits.size(), chunk_size),
std::back_inserter(c));
c.NegateLiterals();
auto wrap = solver_wrapper();
auto wrap = noninc_solver_wrapper();
auto &g = wrap.Solver();
if (g.AddCnf(cnf) && g.AddClauses(units) && g.AddClause(c)
&& g.Solve(alpha))
......
......@@ -16,20 +16,21 @@ std::atomic<long unsigned> SUBool::SolverInterface::sSolveCountUNSAT;
std::atomic<long unsigned> SUBool::SolverInterface::sSolveCountUNDEF;
SUBool::SolverPool SUBool::SolverPool::sDefaultPool;
SUBool::SOLVER_TYPE SUBool::SolverPool::sSolverType{default_solver_type()};
SUBool::NONINC_SOLVER_TYPE SUBool::SolverPool::sNonIncSolverType{
default_noninc_solver_type()};
SUBool::INC_SOLVER_TYPE SUBool::SolverPool::sIncSolverType{
default_inc_solver_type()};
const SUBool::EnumAnnotation<SUBool::SOLVER_TYPE> SUBool::kSolverTypeAnnotation(
"SOLVER_TYPE", { //
const SUBool::EnumAnnotation<SUBool::NONINC_SOLVER_TYPE>
SUBool::kNonIncSolverTypeAnnotation("NONINC_SOLVER_TYPE", { //
{
SOLVER_TYPE::GLUCOSE, "glucose", "use glucose."
NONINC_SOLVER_TYPE::GLUCOSE, "glucose", "use glucose."
}
#if HAS_CADICAL
, { SOLVER_TYPE::CADICAL, "cadical", "use cadical." }
, { NONINC_SOLVER_TYPE::CADICAL, "cadical", "use cadical." }
#endif
#if HAS_KISSAT
, { SOLVER_TYPE::KISSAT, "kissat", "use kissat." }
, { NONINC_SOLVER_TYPE::KISSAT, "kissat", "use kissat." }
#endif
});
......@@ -79,56 +80,58 @@ SUBool::SolverPool::InterruptInThread(std::thread::id thread_id)
}
SUBool::AbsSolverWrapper
SUBool::solver_wrapper(
SOLVER_TYPE solver_type, SolverInterface::ADAPTATION adapt)
SUBool::noninc_solver_wrapper(
NONINC_SOLVER_TYPE solver_type, SolverInterface::ADAPTATION adapt)
{
switch (solver_type)
{
case SOLVER_TYPE::GLUCOSE:
case NONINC_SOLVER_TYPE::GLUCOSE:
return GlucoseSimpWrapper(adapt);
case SOLVER_TYPE::CADICAL:
case NONINC_SOLVER_TYPE::CADICAL:
#if HAS_CADICAL
return CadicalWrapper(false, adapt);
#else
throw BadParameterException(
"solver_wrapper", "Cadical support not available");
"noninc_solver_wrapper", "Cadical support not available");
#endif
case SOLVER_TYPE::KISSAT:
case NONINC_SOLVER_TYPE::KISSAT:
#if HAS_KISSAT
return KissatWrapper(adapt);
#else
throw BadParameterException(
"solver_wrapper", "Kissat support not available");
"noninc_solver_wrapper", "Kissat support not available");
#endif
default:
throw BadParameterException("solver_wrapper", "Unknown solver type");
throw BadParameterException(
"noninc_solver_wrapper", "Unknown solver type");
}
};
SUBool::AbsSolverWrapper
SUBool::solver_wrapper(
SOLVER_TYPE solver_type, const CNF &cnf, SolverInterface::ADAPTATION adapt)
SUBool::noninc_solver_wrapper(NONINC_SOLVER_TYPE solver_type, const CNF &cnf,
SolverInterface::ADAPTATION adapt)
{
switch (solver_type)
{
case SOLVER_TYPE::GLUCOSE:
case NONINC_SOLVER_TYPE::GLUCOSE:
return GlucoseSimpWrapper(cnf, adapt);
case SOLVER_TYPE::CADICAL:
case NONINC_SOLVER_TYPE::CADICAL:
#if HAS_CADICAL
return CadicalWrapper(cnf, false, adapt);
#else
throw BadParameterException(
"solver_wrapper", "Cadical support not available");
"noninc_solver_wrapper", "Cadical support not available");
#endif
case SOLVER_TYPE::KISSAT:
case NONINC_SOLVER_TYPE::KISSAT:
#if HAS_KISSAT
return KissatWrapper(cnf, adapt);
#else
throw BadParameterException(
"solver_wrapper", "Kissat support not available");
"noninc_solver_wrapper", "Kissat support not available");
#endif
default:
throw BadParameterException("solver_wrapper", "Unknown solver type");
throw BadParameterException(
"noninc_solver_wrapper", "Unknown solver type");
}
};
......@@ -171,3 +174,13 @@ SUBool::inc_solver_wrapper(INC_SOLVER_TYPE solver_type, const CNF &cnf,
throw BadParameterException("inc_solver_wrapper", "Unknown solver type");
}
};
void
SUBool::SolverPool::DumpSolverTypes(
const std::string &line_prefix, unsigned level)
{
kIncSolverTypeAnnotation.DumpValue(
line_prefix, level, "solver", sIncSolverType);
kNonIncSolverTypeAnnotation.DumpValue(
line_prefix, level, "nonincremental_solver", sNonIncSolverType);
}
......@@ -105,7 +105,7 @@ namespace SUBool
virtual bool IsIncremental() const = 0;
};
enum class SOLVER_TYPE
enum class NONINC_SOLVER_TYPE
{
GLUCOSE,
CADICAL,
......@@ -118,10 +118,10 @@ namespace SUBool
CADICAL
};
extern const EnumAnnotation<SOLVER_TYPE> kSolverTypeAnnotation;
extern const EnumAnnotation<NONINC_SOLVER_TYPE> kNonIncSolverTypeAnnotation;
extern const EnumAnnotation<INC_SOLVER_TYPE> kIncSolverTypeAnnotation;
constexpr SOLVER_TYPE default_solver_type();
constexpr NONINC_SOLVER_TYPE default_noninc_solver_type();
constexpr INC_SOLVER_TYPE default_inc_solver_type();
struct SolverHandle
......@@ -149,7 +149,7 @@ namespace SUBool
public:
static INC_SOLVER_TYPE sIncSolverType;
static SOLVER_TYPE sSolverType;
static NONINC_SOLVER_TYPE sNonIncSolverType;
SolverPool() : mSolverList(), mMutex() {}
~SolverPool() = default;
......@@ -187,6 +187,9 @@ namespace SUBool
{
return mSolverList.end();
}
static void DumpSolverTypes(
const std::string &line_prefix, unsigned level);
};
inline bool
......@@ -246,15 +249,17 @@ namespace SUBool
}
}; // namespace SUBool
AbsSolverWrapper solver_wrapper(
SOLVER_TYPE solver_type, SolverInterface::ADAPTATION adapt =
SolverInterface::ADAPTATION::DEFAULT);
AbsSolverWrapper solver_wrapper(SOLVER_TYPE solver_type, const CNF &cnf,
AbsSolverWrapper noninc_solver_wrapper(NONINC_SOLVER_TYPE solver_type,
SolverInterface::ADAPTATION adapt =
SolverInterface::ADAPTATION::DEFAULT);
AbsSolverWrapper noninc_solver_wrapper(NONINC_SOLVER_TYPE solver_type,
const CNF &cnf,
SolverInterface::ADAPTATION adapt =
SolverInterface::ADAPTATION::DEFAULT);
AbsSolverWrapper solver_wrapper(SolverInterface::ADAPTATION adapt =
SolverInterface::ADAPTATION::DEFAULT);
AbsSolverWrapper solver_wrapper(
AbsSolverWrapper noninc_solver_wrapper(
SolverInterface::ADAPTATION adapt =
SolverInterface::ADAPTATION::DEFAULT);
AbsSolverWrapper noninc_solver_wrapper(
const CNF &cnf, SolverInterface::ADAPTATION adapt =
SolverInterface::ADAPTATION::DEFAULT);
......@@ -340,10 +345,10 @@ SUBool::default_inc_solver_type()
#elif HAS_CADICAL
constexpr SUBool::SOLVER_TYPE
SUBool::default_solver_type()
constexpr SUBool::NONINC_SOLVER_TYPE
SUBool::default_noninc_solver_type()
{
return SOLVER_TYPE::CADICAL;
return NONINC_SOLVER_TYPE::CADICAL;
}
constexpr SUBool::INC_SOLVER_TYPE
......@@ -372,14 +377,14 @@ SUBool::inc_solver_wrapper(
}
inline SUBool::AbsSolverWrapper
SUBool::solver_wrapper(SolverInterface::ADAPTATION adapt)
SUBool::noninc_solver_wrapper(SolverInterface::ADAPTATION adapt)
{
return solver_wrapper(SolverPool::sSolverType, adapt);
return noninc_solver_wrapper(SolverPool::sNonIncSolverType, adapt);
}
inline SUBool::AbsSolverWrapper
SUBool::solver_wrapper(const CNF &cnf, SolverInterface::ADAPTATION adapt)
SUBool::noninc_solver_wrapper(const CNF &cnf, SolverInterface::ADAPTATION adapt)
{
return solver_wrapper(SolverPool::sSolverType, cnf, adapt);
return noninc_solver_wrapper(SolverPool::sNonIncSolverType, cnf, adapt);
}
#endif
......@@ -10,7 +10,8 @@
SUBool::SolverOptions::SolverOptions()
: OptionsGroup("Solvers"),
mSolverTypeOption(kSolverTypeAnnotation, "nonincremental-solver",
mNonIncSolverTypeOption(kNonIncSolverTypeAnnotation,
"nonincremental-solver",
"Solver to be used in cases when incremental solver is not required, "
"e.g. for the PC check. Default is to have the same solver for PC "
"checks as the solver for other queries which is given by option "
......@@ -20,7 +21,7 @@ SUBool::SolverOptions::SolverOptions()
default_inc_solver_type())
{
Add(mIncSolverTypeOption);
Add(mSolverTypeOption);
Add(mNonIncSolverTypeOption);
}
bool
......@@ -30,17 +31,17 @@ SUBool::SolverOptions::GetValues()
{
return false;
}
if (!mSolverTypeOption.Empty())
if (!mNonIncSolverTypeOption.Empty())
{
SOLVER_TYPE solver_type;
if (!mSolverTypeOption.GetValue(solver_type))
NONINC_SOLVER_TYPE noninc_solver_type;
if (!mNonIncSolverTypeOption.GetValue(noninc_solver_type))
{
return false;
}
mSolverType = solver_type;
mNonIncSolverType = noninc_solver_type;
}
SolverPool::sIncSolverType = mIncSolverType;
SolverPool::sSolverType = SolverType();
SolverPool::sNonIncSolverType = NonIncSolverType();
return true;
}
......@@ -21,10 +21,10 @@ namespace SUBool
class SolverOptions : public OptionsGroup
{
private:
EnumOption<SOLVER_TYPE> mSolverTypeOption;
EnumOption<NONINC_SOLVER_TYPE> mNonIncSolverTypeOption;
EnumOption<INC_SOLVER_TYPE> mIncSolverTypeOption;
boost::optional<SOLVER_TYPE> mSolverType{};
boost::optional<NONINC_SOLVER_TYPE> mNonIncSolverType{};
INC_SOLVER_TYPE mIncSolverType{default_inc_solver_type()};
public:
......@@ -32,24 +32,24 @@ namespace SUBool
virtual bool GetValues() override;
SOLVER_TYPE SolverType() const;
NONINC_SOLVER_TYPE NonIncSolverType() const;
INC_SOLVER_TYPE IncSolverType() const;
};
} // namespace SUBool
inline SUBool::SOLVER_TYPE
SUBool::SolverOptions::SolverType() const
inline SUBool::NONINC_SOLVER_TYPE
SUBool::SolverOptions::NonIncSolverType() const
{
if (mSolverType)
if (mNonIncSolverType)
{
return *mSolverType;
return *mNonIncSolverType;
}
switch (mIncSolverType)
{
case INC_SOLVER_TYPE::GLUCOSE:
return SOLVER_TYPE::GLUCOSE;
return NONINC_SOLVER_TYPE::GLUCOSE;
case INC_SOLVER_TYPE::CADICAL:
return SOLVER_TYPE::CADICAL;
return NONINC_SOLVER_TYPE::CADICAL;
default:
throw BadParameterException(
"SolverOptions::SolverType", "Unknown inc solver type");
......
......@@ -22,12 +22,10 @@ SUBool::UCComp::UCComp(CNF cnf, Config conf)
if (mConf.interleave_pc)
{
mUCPCCheckerSAT.Init(mEncConf, mPCEncConf, true, mConf.timeouts);
mUCPCCheckerSAT.SetSolverType(mConf.solver_type);
}
else
{
mUCCheckerSAT.Init(mEncConf, true, mConf.timeouts);
mUCCheckerSAT.SetSolverType(mConf.solver_type);
}
}
......
Supports Markdown
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