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

Solver type can be changed globally

parent 41346aa3
......@@ -95,7 +95,7 @@ parse_arguments(int argc, char *argv[])
opts.SetHelpDesc(prg_help);
opts.SinglePositional({&conf.input_file, "input"});
auto general_opts = opts.MakeOptionsGroup<SUBool::PCCheckGeneralOptions>();
auto solver_opts = opts.MakeOptionsGroup<SUBool::SolverOptions>(true);
auto solver_opts = opts.MakeOptionsGroup<SUBool::SolverOptions>();
auto oneprove_opts = opts.MakeOptionsGroup<SUBool::PCOneProveOptions>(false);
auto timeout_opts = opts.MakeOptionsGroup<SUBool::PCTimeoutsOptions>(false);
auto cardinal_opt_group =
......
......@@ -138,7 +138,7 @@ parse_arguments(int argc, char *argv[], config_t &conf)
auto pclearncomp_opts = opts.MakeOptionsGroup<SUBool::PCLearnCompOptions>();
auto preprocess_opts =
opts.MakeOptionsGroup<SUBool::PCCompPreprocessOptions>();
auto solver_opts = opts.MakeOptionsGroup<SUBool::SolverOptions>(true);
auto solver_opts = opts.MakeOptionsGroup<SUBool::SolverOptions>();
auto oneprove_opts = opts.MakeOptionsGroup<SUBool::PCOneProveOptions>(true);
auto pccheck_random_opts =
opts.MakeOptionsGroup<SUBool::PCRandomPCChecksOptions>();
......
......@@ -86,7 +86,8 @@ SUBool::AbsCanon::PrintStatistics(unsigned level) const
}
SUBool::CanonSAT::CanonSAT(CNF cnf)
: mOpen(), mClosed(), mInput(std::move(cnf)), mSolver(mInput)
: mOpen(), mClosed(), mInput(std::move(cnf)),
mSolver(inc_solver_wrapper(mInput, false))
{
}
......
......@@ -63,7 +63,7 @@ namespace SUBool
CNF mInput;
double mInprocTime{0.0};
double mPreprocTime{0.0};
IncSolverWrapper mSolver;
AbsSolverWrapper mSolver;
public:
CanonSAT(CNF cnf);
......
......@@ -14,7 +14,7 @@
bool
SUBool::cnf_implies(const CNF &a, const CNF &b)
{
IncSolverWrapper solver(a);
auto solver = inc_solver_wrapper(a, false);
size_t i = 0;
bool log_progress = (b.Size() > LogStream::kMinLogCNFSize);
for (const auto &clause : b)
......
......@@ -19,9 +19,6 @@ namespace SUBool
std::vector<Literal> masked_clause_assump(
const Clause &clause, const std::vector<bool> &mask);
Clause masked_clause(const Clause &clause, const std::vector<bool> &mask);
std::optional<Clause> solve_with_learning(const CNF &prime, const CNF &cnf,
unsigned cnf_start_index, CNF *learned, const Clause *clause,
const std::vector<Literal> &assump);
std::unordered_set<Literal> intersect_lits_with_assign(
std::unordered_set<Literal> lits, const PartialAssignment &alpha);
......@@ -94,10 +91,8 @@ SUBool::clause_falsifying(const Clause &clause, unsigned n)
bool
SUBool::is_implicate(const CNF &cnf, const Clause &clause)
{
SimpSolverWrapper wrap;
auto &g = wrap.Solver();
g.AddCnf(cnf);
return is_implicate(g, clause);
auto wrap = solver_wrapper(cnf);
return is_implicate(wrap.Solver(), clause);
}
bool
......@@ -109,7 +104,6 @@ SUBool::is_implicate(const SolverInterface &solver, const Clause &clause)
{
neg_literals.push_back(lit.Negation());
}
SimpSolverWrapper wrap;
return !solver.Solve(neg_literals);
}
......@@ -117,7 +111,7 @@ std::optional<SUBool::Clause>
SUBool::prime_subimplicate(const CNF &cnf, const Clause &clause,
unsigned ignore_var, bool promised_sat)
{
IncSolverWrapper solver(cnf);
auto solver = inc_solver_wrapper(cnf, false);
return prime_subimplicate(solver.Solver(), clause, ignore_var, promised_sat);
}
......@@ -170,42 +164,6 @@ SUBool::prime_subimplicate(const SolverInterface &solver, const Clause &clause,
return subclause;
}
std::optional<SUBool::Clause>
SUBool::solve_with_learning(const CNF &prime, const CNF &cnf,
unsigned cnf_start_index, CNF *learned, const Clause *clause,
const std::vector<Literal> &assump)
{
SimpSolverWrapper wrap;
auto &g = wrap.Solver();
g.AddCnf(prime);
if (learned)
{
g.AddCnf(*learned);
}
if (clause)
{
g.AddClause(*clause);
}
if (cnf_start_index < cnf.Size())
{
for (auto i_clause = cnf.begin() + cnf_start_index; i_clause != cnf.end();
++i_clause)
{
g.AddClause(*i_clause);
}
}
auto r = g.Solve(assump);
if (learned)
{
learned->Append(g.ExtractLearnts());
}
if (!r)
{
return g.ConflictClause();
}
return {};
}
SUBool::CNF
SUBool::prime_cnf(
const SolverInterface &solver, const CNF &cnf, size_t progress_step)
......@@ -248,8 +206,6 @@ SUBool::prime_cnf(
bool
SUBool::is_satisfiable(const CNF &cnf)
{
SimpSolverWrapper wrap;
auto &g = wrap.Solver();
g.AddCnf(cnf);
return g.Solve();
auto wrap = solver_wrapper(cnf);
return wrap.Solver().Solve();
}
......@@ -61,8 +61,8 @@ namespace SUBool
inline CNF
prime_cnf(const CNF &cnf, size_t progress_step = 0)
{
IncSolverWrapper solver(cnf);
return prime_cnf(solver.Solver(), cnf, progress_step);
auto wrap = inc_solver_wrapper(cnf, false);
return prime_cnf(wrap.Solver(), cnf, progress_step);
}
CNF masked_cnf(SUBool::CNF cnf, const std::vector<bool> &mask);
......@@ -75,8 +75,8 @@ template <class Pred>
SUBool::CNF
SUBool::prime_cnf_with_ignore(const CNF &cnf, Pred pred)
{
IncSolverWrapper solver(cnf);
return prime_cnf_with_ignore(solver.Solver(), cnf, pred);
auto wrap = inc_solver_wrapper(cnf, false);
return prime_cnf_with_ignore(wrap.Solver(), cnf, pred);
}
template <class Pred>
......@@ -113,7 +113,7 @@ SUBool::prime_cnf_with_ignore(
inline bool
SUBool::is_consistent(const CNF &cnf, const std::vector<Literal> &assump)
{
SimpSolverWrapper wrap(cnf);
auto wrap = 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)
{
SimpSolverWrapper wrap(cnf);
auto wrap = 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)
{
SimpSolverWrapper wrap(cnf);
auto wrap = solver_wrapper(cnf);
auto &g = wrap.Solver();
return g.Solve(assump);
}
......
......@@ -13,8 +13,8 @@
#include "propagate.h"
SUBool::CompHypothesis::CompHypothesis(MINIMIZE_METHOD minimize_method)
: mRepresentation(), mHypothesis(), mSolver(), mSafe(false),
mOneProveRepr(mRepresentation), mOneProveHyp(mHypothesis),
: mRepresentation(), mHypothesis(), mSolver(inc_solver_wrapper(true)),
mSafe(false), mOneProveRepr(mRepresentation), mOneProveHyp(mHypothesis),
mMinSubimplicant(&mRepresentation),
mSemPropagator(
mSolver.GetSolverPtr(), &(mOneProveRepr.UP()), &mMinSubimplicant),
......@@ -25,8 +25,8 @@ SUBool::CompHypothesis::CompHypothesis(MINIMIZE_METHOD minimize_method)
SUBool::CompHypothesis::CompHypothesis(
MINIMIZE_METHOD minimize_method, CNF cnf, CNF repr, bool safe)
: mRepresentation(std::move(repr)), mHypothesis(std::move(cnf)),
mSolver(safe ? mHypothesis : mRepresentation), mSafe(safe),
mOneProveRepr(mRepresentation), mOneProveHyp(mHypothesis),
mSolver(inc_solver_wrapper((safe ? mHypothesis : mRepresentation), true)),
mSafe(safe), mOneProveRepr(mRepresentation), mOneProveHyp(mHypothesis),
mMinSubimplicant(safe ? &mHypothesis : &mRepresentation),
mSemPropagator(mSolver.GetSolverPtr(),
safe ? &(mOneProveHyp.UP()) : &(mOneProveRepr.UP()),
......
......@@ -49,7 +49,7 @@ namespace SUBool
{
CNF mRepresentation;
CNF mHypothesis;
IncSolverWrapper mSolver;
AbsSolverWrapper mSolver;
bool mSafe;
// should rename it and the propagator could be semantical?
OneProveM mOneProveRepr;
......
......@@ -134,7 +134,7 @@ SUBool::CNFEncoding::EliminateAuxVariablesWithMaxSizeMinimize(
}
CPUTime cpu_time;
CNF ref_cnf;
IncSolverWrapper ref_solver;
auto ref_solver = inc_solver_wrapper(false);
if (mBlockPrime == BLOCK_PRIME::PRIME)
{
ref_cnf = mCnf;
......
......@@ -182,7 +182,7 @@ namespace SUBool
class SATEncoding : public CNFEncoding
{
IncSolverWrapper mSolver;
AbsSolverWrapper mSolver;
UnitPropagatorM mUP;
MinimalSubimplicant mMinSubimplicant;
Propagator mPropagator;
......@@ -196,7 +196,8 @@ namespace SUBool
DPEliminator::IGNORE_POLICY::IMPLICATES,
DPEliminator::INPROCESSING::NONE,
DPEliminator::INCREASE_POLICY::ESTIMATE, BLOCK_PRIME::NONE),
mSolver(mCnf), mUP(mCnf), mMinSubimplicant(&mCnf),
mSolver(inc_solver_wrapper(mCnf, false)), mUP(mCnf),
mMinSubimplicant(&mCnf),
mPropagator(mSolver.GetSolverPtr(), &mUP, &mMinSubimplicant)
{
}
......
......@@ -152,8 +152,8 @@ namespace SUBool
Glucose::Lit glucose_lit(const Literal &lit);
PartialValue of_glucose_value(Glucose::lbool val);
using SimpSolverWrapper = SolverWrapperTemplate<GlucoseBindSimp>;
using IncSolverWrapper = SolverWrapperTemplate<GlucoseBindInc>;
using GlucoseSimpWrapper = SolverWrapperTemplate<GlucoseBindSimp>;
using GlucoseIncWrapper = SolverWrapperTemplate<GlucoseBindInc>;
} // namespace SUBool
template <class Solver>
......
......@@ -21,7 +21,7 @@ SUBool::ImplicateChecker::AddToLearnts(std::vector<Clause> clauses)
bool
SUBool::ImplicateChecker::IsImplicate(const CNF &cnf, const Clause &clause)
{
SimpSolverWrapper wrap(cnf);
auto wrap = inc_solver_wrapper(cnf, true);
auto &g = wrap.Solver();
auto r = is_implicate(g, clause);
AddToLearnts(g.ExtractLearnts());
......@@ -32,7 +32,7 @@ std::optional<SUBool::Clause>
SUBool::ImplicateChecker::PrimeSubimplicate(const CNF &cnf,
const Clause &clause, unsigned ignore_var, bool promised_sat)
{
IncSolverWrapper wrap(cnf);
auto wrap = inc_solver_wrapper(cnf, true);
auto &g = wrap.Solver();
auto prime = prime_subimplicate(cnf, clause, ignore_var, promised_sat);
AddToLearnts(g.ExtractLearnts());
......@@ -67,7 +67,7 @@ bool
SUBool::ImplicateChecker::Solve(
const CNF &cnf, const std::vector<Literal> &assump)
{
SimpSolverWrapper wrap(cnf);
auto wrap = inc_solver_wrapper(cnf, true);
auto &g = wrap.Solver();
auto result = g.Solve(assump);
AddToLearnts(g.ExtractLearnts());
......
......@@ -72,7 +72,12 @@ namespace SUBool
public:
KissatBind(const SolverInterface::ADAPTATION adapt =
SolverInterface::ADAPTATION::DEFAULT);
KissatBind(const CNF &cnf) : KissatBind() { AddCnf(cnf); }
KissatBind(const CNF &cnf, const SolverInterface::ADAPTATION adapt =
SolverInterface::ADAPTATION::DEFAULT)
: KissatBind(adapt)
{
AddCnf(cnf);
}
virtual bool Reset(const CNF &cnf) override;
virtual bool AddCnf(const CNF &cnf) override;
......@@ -103,7 +108,7 @@ namespace SUBool
PartialValue of_kissat_value(int val);
using KissatSolverWrapper = SolverWrapperTemplate<KissatBindSolver>;
using KissatWrapper = SolverWrapperTemplate<KissatBindSolver>;
} // namespace SUBool
template <class Solver>
......
......@@ -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, false,
assume_sat ? SolverInterface::ADAPTATION::LIKELY_SAT
: SolverInterface::ADAPTATION::LIKELY_UNSAT);
auto wrap = solver_wrapper(
mSolverType, 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()
......
......@@ -10,9 +10,8 @@
namespace SUBool
{
std::unordered_set<Literal>
intersect_lits_with_assign(std::unordered_set<Literal> lits,
const PartialAssignment &alpha);
std::unordered_set<Literal> intersect_lits_with_assign(
std::unordered_set<Literal> lits, const PartialAssignment &alpha);
}; // namespace SUBool
......@@ -22,8 +21,7 @@ SUBool::AbsPropagator::Propagate(const SUBool::PartialAssignment &alpha) const
if (!valid_solver_ptr(mSolverPtr) || mUP == nullptr
|| mMinSubimplicant == nullptr)
{
throw BadParameterException(
"AbsPropagator::Propagate(alpha)",
throw BadParameterException("AbsPropagator::Propagate(alpha)",
"No solver, unit propagator, or minimal subimplicant ");
}
auto gamma = mUP->Propagate(alpha);
......@@ -89,8 +87,8 @@ SUBool::Propagator::InnerPropagate(const PartialAssignment &alpha) const
}
SUBool::PartialAssignment
SUBool::Propagator::ProcessMinModel(PartialAssignment alpha,
PartialAssignment beta) const
SUBool::Propagator::ProcessMinModel(
PartialAssignment alpha, PartialAssignment beta) const
{
size_t fixed_var_index = 0;
for (unsigned i = 1; i <= alpha.Size(); ++i)
......@@ -120,8 +118,8 @@ SUBool::Propagator::ProcessMinModel(PartialAssignment alpha,
}
void
SUBool::Propagator::InitFreeVars(const PartialAssignment &alpha,
const PartialAssignment &min_model) const
SUBool::Propagator::InitFreeVars(
const PartialAssignment &alpha, const PartialAssignment &min_model) const
{
mFreeSetVars.clear();
mFreeUnsetVars.clear();
......@@ -152,16 +150,16 @@ SUBool::Propagator::MinimalModelWithFreeVars(PartialAssignment model) const
{
mFreeVars.assign(mFreeSetVars.begin(), mFreeSetVars.end());
std::shuffle(mFreeVars.begin(), mFreeVars.end(), sub_rand);
mFreeVars.insert(mFreeVars.end(), mFreeUnsetVars.begin(),
mFreeUnsetVars.end());
std::shuffle(mFreeVars.begin() + mFreeSetVars.size(), mFreeVars.end(),
sub_rand);
mFreeVars.insert(
mFreeVars.end(), mFreeUnsetVars.begin(), mFreeUnsetVars.end());
std::shuffle(
mFreeVars.begin() + mFreeSetVars.size(), mFreeVars.end(), sub_rand);
return MinimalSubmodelWithFreeVars(std::move(model), mFreeVars);
}
SUBool::PartialAssignment
SUBool::Propagator::UpdateFreeVarsNoModel(unsigned var, PartialAssignment alpha,
const PartialAssignment &beta) const
SUBool::Propagator::UpdateFreeVarsNoModel(
unsigned var, PartialAssignment alpha, const PartialAssignment &beta) const
{
auto closed_alpha = mUP->Propagate(alpha);
assert(closed_alpha);
......@@ -206,8 +204,7 @@ SUBool::Propagator::UpdateFreeVarsWithModel(
SUBool::PartialAssignment
SUBool::propagate_core_chunk(const CNF &cnf, PartialAssignment alpha,
std::unordered_set<Literal> free_lits,
size_t chunk_size)
std::unordered_set<Literal> free_lits, size_t chunk_size)
{
std::unordered_set<Literal> chunk_literals;
std::unordered_set<Literal> omega;
......@@ -225,7 +222,7 @@ SUBool::propagate_core_chunk(const CNF &cnf, PartialAssignment alpha,
{
chunk_literals.clear();
std::copy_n(free_lits.begin(), std::min(free_lits.size(), chunk_size),
std::inserter(chunk_literals, chunk_literals.end()));
std::inserter(chunk_literals, chunk_literals.end()));
omega.clear();
for (auto &lit : chunk_literals)
{
......@@ -233,9 +230,8 @@ SUBool::propagate_core_chunk(const CNF &cnf, PartialAssignment alpha,
}
while (true)
{
SimpSolverWrapper wrap;
auto wrap = solver_wrapper(cnf);
auto &g = wrap.Solver();
g.AddCnf(cnf);
g.AddClauses(units);
omega_lits.assign(omega.begin(), omega.end());
auto result = g.Solve(omega_lits);
......@@ -263,8 +259,7 @@ SUBool::propagate_core_chunk(const CNF &cnf, PartialAssignment alpha,
}
if (intersect_size == 0)
{
throw InvariantFailedException(
"propagate_core_chunk",
throw InvariantFailedException("propagate_core_chunk",
"Intersection of core with omega is empty");
}
if (intersect_size == 1)
......@@ -282,7 +277,7 @@ SUBool::propagate_core_chunk(const CNF &cnf, PartialAssignment alpha,
}
auto cl_size = chunk_literals.size();
alpha = propagate_iterative(cnf, alpha, std::move(chunk_literals),
iterative_chunk_size(cl_size), units);
iterative_chunk_size(cl_size), units);
break;
}
}
......@@ -292,17 +287,17 @@ SUBool::propagate_core_chunk(const CNF &cnf, PartialAssignment alpha,
SUBool::PartialAssignment
SUBool::propagate_iterative(const CNF &cnf, PartialAssignment alpha,
std::unordered_set<Literal> free_lits,
size_t chunk_size, const std::vector<Clause> &units)
std::unordered_set<Literal> free_lits, size_t chunk_size,
const std::vector<Clause> &units)
{
Clause c;
while (!free_lits.empty())
{
c.Clear();
std::copy_n(free_lits.begin(), std::min(free_lits.size(), chunk_size),
std::back_inserter(c));
std::back_inserter(c));
c.NegateLiterals();
SimpSolverWrapper wrap;
auto wrap = solver_wrapper();
auto &g = wrap.Solver();
if (g.AddCnf(cnf) && g.AddClauses(units) && g.AddClause(c)
&& g.Solve(alpha))
......@@ -314,14 +309,14 @@ SUBool::propagate_iterative(const CNF &cnf, PartialAssignment alpha,
c.NegateLiterals();
alpha.SetLiterals(c.begin(), c.end());
std::for_each(c.begin(), c.end(),
[&free_lits](const Literal &lit) { free_lits.erase(lit); });
[&free_lits](const Literal &lit) { free_lits.erase(lit); });
}
return alpha;
}
std::unordered_set<SUBool::Literal>
SUBool::intersect_lits_with_assign(std::unordered_set<Literal> lits,
const PartialAssignment &alpha)
SUBool::intersect_lits_with_assign(
std::unordered_set<Literal> lits, const PartialAssignment &alpha)
{
auto i_lit = lits.begin();
while (i_lit != lits.end())
......@@ -340,7 +335,7 @@ SUBool::intersect_lits_with_assign(std::unordered_set<Literal> lits,
size_t
SUBool::chunk_size(size_t free_lits_size, size_t min_chunk_size,
size_t max_chunk_size, size_t min_chunk_count)
size_t max_chunk_size, size_t min_chunk_count)
{
size_t k = std::min(max_chunk_size, free_lits_size / min_chunk_count);
return std::max<size_t>(k, min_chunk_size);
......
......@@ -44,16 +44,15 @@ namespace SUBool
protected:
// alpha is already closed under unit propagation when passed to
// InnerPropagate
virtual std::optional<PartialAssignment>
InnerPropagate(const PartialAssignment &alpha) const = 0;
std::optional<PartialAssignment>
ConsistentModel(const PartialAssignment &alpha) const;
std::optional<PartialAssignment>
MinimalConsistentModelFixedVars(const PartialAssignment &alpha) const;
PartialAssignment
MinimalSubmodelWithFreeVars(PartialAssignment model,
const std::vector<unsigned> &free_vars) const;
virtual std::optional<PartialAssignment> InnerPropagate(
const PartialAssignment &alpha) const = 0;
std::optional<PartialAssignment> ConsistentModel(
const PartialAssignment &alpha) const;
std::optional<PartialAssignment> MinimalConsistentModelFixedVars(
const PartialAssignment &alpha) const;
PartialAssignment MinimalSubmodelWithFreeVars(PartialAssignment model,
const std::vector<unsigned> &free_vars) const;
unsigned
FixedVarAt(size_t i) const
{
......@@ -62,7 +61,7 @@ namespace SUBool
public:
AbsPropagator(SolverConstPtr solver_ptr, const UnitPropagatorM *up,
const MinimalSubimplicant *min_subimplicant) noexcept
const MinimalSubimplicant *min_subimplicant) noexcept
: mSolverPtr(solver_ptr), mUP(up), mMinSubimplicant(min_subimplicant),
mFixedVars()
{
......@@ -77,7 +76,7 @@ namespace SUBool
virtual void
Reset(SolverConstPtr solver_ptr, const UnitPropagatorM *up,
const MinimalSubimplicant *min_subimplicant)
const MinimalSubimplicant *min_subimplicant)
{
mSolverPtr = solver_ptr;
mUP = up;
......@@ -89,18 +88,18 @@ namespace SUBool
// @param pred specifies predicate for checking if a variable should be
// considered for propagation (with a SAT call).
template <class FreePred>
std::optional<PartialAssignment> Propagate(const PartialAssignment &alpha,
FreePred free_pred) const;
std::optional<PartialAssignment> Propagate(
const PartialAssignment &alpha, FreePred free_pred) const;
// propagates all
std::optional<PartialAssignment>
Propagate(const PartialAssignment &alpha) const;
std::optional<PartialAssignment> Propagate(
const PartialAssignment &alpha) const;
std::optional<PartialAssignment>
PropagateMaxVar(const PartialAssignment &alpha, unsigned max_var) const
{
return Propagate(alpha,
[max_var](unsigned i) { return i <= max_var; });
return Propagate(
alpha, [max_var](unsigned i) { return i <= max_var; });
}
std::optional<PartialAssignment>
......@@ -119,24 +118,22 @@ namespace SUBool
mutable std::vector<unsigned> mFreeVars;
void InitFreeVars(const PartialAssignment &alpha,
const PartialAssignment &min_model) const;
PartialAssignment ProcessMinModel(PartialAssignment alpha,
PartialAssignment beta) const;
const PartialAssignment &min_model) const;
PartialAssignment ProcessMinModel(
PartialAssignment alpha, PartialAssignment beta) const;
PartialAssignment MinimalModelWithFreeVars(PartialAssignment model) const;
PartialAssignment
UpdateFreeVarsNoModel(unsigned var, PartialAssignment alpha,
const PartialAssignment &beta) const;
PartialAssignment
UpdateFreeVarsWithModel(PartialAssignment beta,
const PartialAssignment &min_model) const;
PartialAssignment UpdateFreeVarsNoModel(unsigned var,
PartialAssignment alpha, const PartialAssignment &beta) const;
PartialAssignment UpdateFreeVarsWithModel(
PartialAssignment beta, const PartialAssignment &min_model) const;
protected:
virtual std::optional<PartialAssignment>
InnerPropagate(const PartialAssignment &alpha) const override;
virtual std::optional<PartialAssignment> InnerPropagate(
const PartialAssignment &alpha) const override;
public:
Propagator(SolverConstPtr solver, const UnitPropagatorM *up,
const MinimalSubimplicant *min_subimplicant)
const MinimalSubimplicant *min_subimplicant)
: AbsPropagator(solver, up, min_subimplicant), mFreeSetVars(),
mFreeUnsetVars(), mFreeVars()
{
......@@ -145,31 +142,29 @@ namespace SUBool
// A second propagation algorithm, right now it uses propagate_iterative
template <class Pred>
std::optional<PartialAssignment>
propagate2(const CNF &cnf, const PartialAssignment &alpha, Pred pred);
std::optional<PartialAssignment> propagate2(
const CNF &cnf, const PartialAssignment &alpha, Pred pred);
PartialAssignment propagate_core_chunk(const CNF &cnf,
PartialAssignment alpha,
std::unordered_set<Literal> free_lits,
size_t chunk_size);
PartialAssignment alpha, std::unordered_set<Literal> free_lits,