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

pccompile solvers options

parent ad7518b4
...@@ -112,8 +112,8 @@ dump_config(const config_t &conf, unsigned level) ...@@ -112,8 +112,8 @@ dump_config(const config_t &conf, unsigned level)
"\t", level, "amo_encoding", conf.amo_encoding); "\t", level, "amo_encoding", conf.amo_encoding);
SUBool::ExOneEncoder::kKindAnnotation.DumpValue( SUBool::ExOneEncoder::kKindAnnotation.DumpValue(
"\t", level, "exone_encoding", conf.exone_encoding); "\t", level, "exone_encoding", conf.exone_encoding);
SUBool::dump_enum_value( SUBool::kSolverTypeAnnotation.DumpValue(
"\t", level, "solver_type", conf.solver_type, SUBool::kSolverTypeNames); "\t", level, "solver_type", conf.solver_type);
SUBool::logs.TLog(level) << "END" << std::endl; SUBool::logs.TLog(level) << "END" << std::endl;
} }
......
...@@ -152,8 +152,8 @@ dump_config(const config_t &conf, unsigned level) ...@@ -152,8 +152,8 @@ dump_config(const config_t &conf, unsigned level)
SUBool::logs.TLog(level) SUBool::logs.TLog(level)
<< "\tcomp_base_config.timeouts.level_factor: " << "\tcomp_base_config.timeouts.level_factor: "
<< conf.comp_base_config.timeouts.level_factor << std::endl; << conf.comp_base_config.timeouts.level_factor << std::endl;
SUBool::dump_enum_value("\t", level, "cop_base_config.solver_type", SUBool::kSolverTypeAnnotation.DumpValue("\t", level,
conf.comp_base_config.solver_type, SUBool::kSolverTypeNames); "comp_base_config.solver_type", conf.comp_base_config.solver_type);
SUBool::logs.TLog(level) << "\tenc_conf:" << std::endl; SUBool::logs.TLog(level) << "\tenc_conf:" << std::endl;
conf.comp_base_config.enc_conf.Dump("\t\t", level); conf.comp_base_config.enc_conf.Dump("\t\t", level);
SUBool::AmoEncoder::kKindAnnotation.DumpValue( SUBool::AmoEncoder::kKindAnnotation.DumpValue(
...@@ -205,6 +205,7 @@ parse_arguments(int argc, char *argv[], config_t &conf) ...@@ -205,6 +205,7 @@ parse_arguments(int argc, char *argv[], config_t &conf)
auto pclearncomp_opts = opts.MakeOptionsGroup<SUBool::PCLearnCompOptions>(); auto pclearncomp_opts = opts.MakeOptionsGroup<SUBool::PCLearnCompOptions>();
auto preprocess_opts = auto preprocess_opts =
opts.MakeOptionsGroup<SUBool::PCCompPreprocessOptions>(); opts.MakeOptionsGroup<SUBool::PCCompPreprocessOptions>();
auto solver_opts = opts.MakeOptionsGroup<SUBool::PCSolverOptions>();
if (!opts.Parse(argc, argv)) if (!opts.Parse(argc, argv))
{ {
return 1; return 1;
...@@ -217,6 +218,7 @@ parse_arguments(int argc, char *argv[], config_t &conf) ...@@ -217,6 +218,7 @@ parse_arguments(int argc, char *argv[], config_t &conf)
conf.comp_base_config.preprocess = preprocess_opts->PreprocessMethod(); conf.comp_base_config.preprocess = preprocess_opts->PreprocessMethod();
conf.comp_base_config.propagate_backbones = conf.comp_base_config.propagate_backbones =
!preprocess_opts->NoBackbonePropagation(); !preprocess_opts->NoBackbonePropagation();
conf.comp_base_config.solver_type = solver_opts->SolverType();
return 0; return 0;
#if 0 #if 0
try try
......
...@@ -89,3 +89,19 @@ SUBool::PCCompPreprocessOptions::GetValues() ...@@ -89,3 +89,19 @@ SUBool::PCCompPreprocessOptions::GetValues()
{ {
return mPreprocessMethodOption.GetValue(mPreprocessMethod); return mPreprocessMethodOption.GetValue(mPreprocessMethod);
} }
SUBool::PCSolverOptions::PCSolverOptions()
: OptionsGroup("Solvers"),
mSolverTypeOption(kSolverTypeAnnotation, "pccheck-solver",
"Solver to be used for the PC check. Only the available solvers are "
"listed.",
kDefaultSolverType)
{
Add(mSolverTypeOption);
}
bool
SUBool::PCSolverOptions::GetValues()
{
return mSolverTypeOption.GetValue(mSolverType);
}
...@@ -89,6 +89,23 @@ namespace SUBool ...@@ -89,6 +89,23 @@ namespace SUBool
AbsComp::PREPROCESS_METHOD PreprocessMethod() const; AbsComp::PREPROCESS_METHOD PreprocessMethod() const;
}; };
// Solver selection
class PCSolverOptions : public OptionsGroup
{
public:
static const SOLVER_TYPE kDefaultSolverType = SOLVER_TYPE::GLUCOSE;
private:
EnumOption<SOLVER_TYPE> mSolverTypeOption;
SOLVER_TYPE mSolverType{kDefaultSolverType};
public:
PCSolverOptions();
virtual bool GetValues() override;
SOLVER_TYPE SolverType() const;
};
} // namespace SUBool } // namespace SUBool
inline auto inline auto
...@@ -122,4 +139,10 @@ SUBool::PCCompPreprocessOptions::PreprocessMethod() const ...@@ -122,4 +139,10 @@ SUBool::PCCompPreprocessOptions::PreprocessMethod() const
return mPreprocessMethod; return mPreprocessMethod;
} }
inline SUBool::SOLVER_TYPE
SUBool::PCSolverOptions::SolverType() const
{
return mSolverType;
}
#endif #endif
...@@ -15,9 +15,15 @@ std::atomic<long unsigned> SUBool::SolverInterface::sSolveCountUNSAT; ...@@ -15,9 +15,15 @@ std::atomic<long unsigned> SUBool::SolverInterface::sSolveCountUNSAT;
std::atomic<long unsigned> SUBool::SolverInterface::sSolveCountUNDEF; std::atomic<long unsigned> SUBool::SolverInterface::sSolveCountUNDEF;
SUBool::SolverPool SUBool::SolverPool::sDefaultPool; SUBool::SolverPool SUBool::SolverPool::sDefaultPool;
const std::array<std::string, const SUBool::EnumAnnotation<SUBool::SOLVER_TYPE> SUBool::kSolverTypeAnnotation(
static_cast<size_t>(SUBool::SOLVER_TYPE::Last) + 1> "SOLVER_TYPE", { //
SUBool::kSolverTypeNames{"glucose", "kissat"}; {
SOLVER_TYPE::GLUCOSE, "glucose", "use glucose."
}
#if HAS_KISSAT
, { SOLVER_TYPE::KISSAT, "kissat", "use kissat." }
#endif
});
bool bool
SUBool::SolverInterface::AddClauses(const std::vector<Clause> &clauses) SUBool::SolverInterface::AddClauses(const std::vector<Clause> &clauses)
...@@ -37,24 +43,26 @@ SUBool::SolverPool::InterruptAll() ...@@ -37,24 +43,26 @@ SUBool::SolverPool::InterruptAll()
{ {
std::lock_guard<std::mutex> lock(mMutex); std::lock_guard<std::mutex> lock(mMutex);
std::for_each(mSolverList.begin(), mSolverList.end(), std::for_each(mSolverList.begin(), mSolverList.end(),
[](auto &h) { h.solver->Interrupt(); }); [](auto &h) { h.solver->Interrupt(); });
} }
void void
SUBool::SolverPool::InterruptInThread(std::thread::id thread_id) SUBool::SolverPool::InterruptInThread(std::thread::id thread_id)
{ {
std::lock_guard<std::mutex> lock(mMutex); std::lock_guard<std::mutex> lock(mMutex);
std::for_each(mSolverList.begin(), mSolverList.end(), [thread_id](auto &h) { std::for_each(mSolverList.begin(), mSolverList.end(),
if (h.thread_id == thread_id) [thread_id](auto &h)
{ {
h.solver->Interrupt(); if (h.thread_id == thread_id)
} {
}); h.solver->Interrupt();
}
});
} }
SUBool::AbsSolverWrapper SUBool::AbsSolverWrapper
SUBool::solver_wrapper(SOLVER_TYPE solver_type, SUBool::solver_wrapper(
SolverInterface::ADAPTATION adapt) SOLVER_TYPE solver_type, SolverInterface::ADAPTATION adapt)
{ {
switch (solver_type) switch (solver_type)
{ {
...@@ -64,12 +72,12 @@ SUBool::solver_wrapper(SOLVER_TYPE solver_type, ...@@ -64,12 +72,12 @@ SUBool::solver_wrapper(SOLVER_TYPE solver_type,
#if HAS_KISSAT #if HAS_KISSAT
return KissatSolverWrapper(adapt); return KissatSolverWrapper(adapt);
#else #else
throw BadParameterException("AbsCheckerSAT::NewSolverWrapper", throw BadParameterException(
"Kissat support not available"); "AbsCheckerSAT::NewSolverWrapper", "Kissat support not available");
#endif #endif
default: default:
throw BadParameterException("AbsCheckerSAT::NewSolverWrapper", throw BadParameterException(
"Unknown solver type"); "AbsCheckerSAT::NewSolverWrapper", "Unknown solver type");
} }
}; };
...@@ -15,6 +15,7 @@ ...@@ -15,6 +15,7 @@
#include <optional> #include <optional>
#include <thread> #include <thread>
#include "enum.h"
#include "normalform.h" #include "normalform.h"
namespace SUBool namespace SUBool
...@@ -86,8 +87,7 @@ namespace SUBool ...@@ -86,8 +87,7 @@ namespace SUBool
PartialValue SolveWithTimeout( PartialValue SolveWithTimeout(
const std::chrono::duration<Rep, Period> &timeout_duration) const; const std::chrono::duration<Rep, Period> &timeout_duration) const;
template <class Rep, class Period> template <class Rep, class Period>
PartialValue SolveWithTimeout( PartialValue SolveWithTimeout(const std::vector<Literal> &assump,
const std::vector<Literal> &assump,
const std::chrono::duration<Rep, Period> &timeout_duration) const; const std::chrono::duration<Rep, Period> &timeout_duration) const;
virtual PartialValue ValueOfVariable(unsigned var) const = 0; virtual PartialValue ValueOfVariable(unsigned var) const = 0;
...@@ -225,16 +225,13 @@ namespace SUBool ...@@ -225,16 +225,13 @@ namespace SUBool
enum class SOLVER_TYPE enum class SOLVER_TYPE
{ {
GLUCOSE, GLUCOSE,
KISSAT, KISSAT
Last = KISSAT
}; };
extern const std::array<std::string, extern const EnumAnnotation<SOLVER_TYPE> kSolverTypeAnnotation;
static_cast<size_t>(SOLVER_TYPE::Last) + 1>
kSolverTypeNames;
AbsSolverWrapper solver_wrapper(SOLVER_TYPE solver_type, AbsSolverWrapper solver_wrapper(
SolverInterface::ADAPTATION adapt); SOLVER_TYPE solver_type, SolverInterface::ADAPTATION adapt);
template <class S> class SolverWrapperTemplate : public AbsSolverWrapper template <class S> class SolverWrapperTemplate : public AbsSolverWrapper
{ {
...@@ -265,12 +262,11 @@ SUBool::SolverInterface::SolveWithTimeout( ...@@ -265,12 +262,11 @@ SUBool::SolverInterface::SolveWithTimeout(
template <class Rep, class Period> template <class Rep, class Period>
SUBool::PartialValue SUBool::PartialValue
SUBool::SolverInterface::SolveWithTimeout( SUBool::SolverInterface::SolveWithTimeout(const std::vector<Literal> &assump,
const std::vector<Literal> &assump,
const std::chrono::duration<Rep, Period> &timeout_duration) const const std::chrono::duration<Rep, Period> &timeout_duration) const
{ {
auto fut = std::async(std::launch::async, auto fut = std::async(
[this, &assump]() { return Solve(assump); }); std::launch::async, [this, &assump]() { return Solve(assump); });
if (fut.wait_for(timeout_duration) == std::future_status::timeout) if (fut.wait_for(timeout_duration) == std::future_status::timeout)
{ {
Interrupt(); Interrupt();
...@@ -286,7 +282,7 @@ SUBool::SolverPool::NewSolver(Args &&...arg) ...@@ -286,7 +282,7 @@ SUBool::SolverPool::NewSolver(Args &&...arg)
{ {
std::lock_guard<std::mutex> lock(mMutex); std::lock_guard<std::mutex> lock(mMutex);
mSolverList.emplace_back(std::this_thread::get_id(), mSolverList.emplace_back(std::this_thread::get_id(),
std::make_unique<S>(std::forward<Args>(arg)...)); std::make_unique<S>(std::forward<Args>(arg)...));
return std::prev(mSolverList.end()); return std::prev(mSolverList.end());
} }
#endif #endif
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