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

minimization options in pccompile, simplification renamed to

minimization
parent 5c3c92f5
......@@ -42,10 +42,9 @@ struct config_t
std::string input_file{};
std::string output_file{};
bool minimize{false};
SUBool::MINIMIZE_METHOD minimize_method{SUBool::MINIMIZE_METHOD::FULL};
SUBool::PCCompAlgorithmOptions::ALGORITHM algorithm{
SUBool::PCCompAlgorithmOptions::kDefaultAlgorithm};
bool level_simplify{true}; // simplification at level increase
bool level_minimize{true}; // minimization at level increase
unsigned verbosity{3}; // 0 means no output
bool use_empty_initial_hypothesis{false}; // For PCLearnComp
unsigned pccheck_random_rounds{100};
......@@ -113,14 +112,14 @@ dump_config(const config_t &conf, unsigned level)
"\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) << "\tcomp_base_config.minimize_steps: "
<< conf.comp_base_config.minimize_steps
<< (conf.comp_base_config.minimize_steps > 0
? ""
: "(no minimization in intervals)")
<< std::endl;
SUBool::logs.TLog(level)
<< "\tcomp_base_config.simp_steps: " << conf.comp_base_config.simp_steps
<< (conf.comp_base_config.simp_steps > 0
? ""
: "(no simplification in intervals)")
<< std::endl;
SUBool::logs.TLog(level)
<< "\tlevel_simplify: " << (conf.level_simplify ? "yes" : "no")
<< "\tlevel_minimize: " << (conf.level_minimize ? "yes" : "no")
<< std::endl;
SUBool::kLitImplSystemAnnotation.DumpValue("\t", level,
"comp_base_config.impl_system", conf.comp_base_config.impl_system);
......@@ -182,6 +181,7 @@ parse_arguments(int argc, char *argv[], config_t &conf)
auto oneprove_opts = opts.MakeOptionsGroup<SUBool::PCOneProveOptions>();
auto pccheck_random_opts =
opts.MakeOptionsGroup<SUBool::PCRandomPCChecksOptions>();
auto minimize_opts = opts.MakeOptionsGroup<SUBool::PCMinimizationOptions>();
if (!opts.Parse(argc, argv))
{
return 1;
......@@ -205,6 +205,10 @@ parse_arguments(int argc, char *argv[], config_t &conf)
conf.pccheck_random_rounds = pccheck_random_opts->Rounds();
conf.pccheck_random_budget = pccheck_random_opts->Budget();
conf.pccheck_random_budget_inc = pccheck_random_opts->BudgetInc();
conf.minimize = minimize_opts->FinalMinimize();
conf.comp_base_config.minimize_method = minimize_opts->MinimizeMethod();
conf.comp_base_config.minimize_steps = minimize_opts->MinimizeSteps();
conf.level_minimize = !minimize_opts->NoLevelMinimize();
return 0;
#if 0
try
......@@ -219,7 +223,7 @@ parse_arguments(int argc, char *argv[], config_t &conf)
unsigned up_empower = 0;
unsigned preprocess = 0;
std::string algorithm;
bool no_level_simplify = false;
bool no_level_minimize= false;
bool no_backbone_propagation = false;
unsigned long long seed;
std::string log_enc_opts;
......@@ -403,15 +407,15 @@ parse_arguments(int argc, char *argv[], config_t &conf)
SUBool::PCLearnComp::cInitialNegativesNames[static_cast<
unsigned>(conf.initial_negatives)]))("s,simp-steps",
"Number of empowering clauses after which a heuristic "
"simplification of the current formula proceeds. Zero (0) means that "
"no simplification is made during the compilation. However final "
"minimization of the current formula proceeds. Zero (0) means that "
"no minimization is made during the compilation. However final "
"minimization shall proceed depending on presence of -m option.",
cxxopts::value<unsigned>(conf.comp_base_config.simp_steps)
->default_value(std::to_string(
conf.comp_base_config.simp_steps)))("no-level-simplify",
"Do not perform simplification when the number of levels of unit "
conf.comp_base_config.simp_steps)))("no-level-minimize",
"Do not perform minimization when the number of levels of unit "
"propagation increases.",
cxxopts::value<bool>(no_level_simplify)
cxxopts::value<bool>(no_level_minimize)
->default_value("false"))("r,preprocess",
"Method of preprocessing. "
"0 = No preprocessing. "
......@@ -530,7 +534,7 @@ parse_arguments(int argc, char *argv[], config_t &conf)
.time_since_epoch()
.count());
conf.goal = (uc ? GOAL::UC : GOAL::PC);
conf.level_simplify = !no_level_simplify;
conf.level_minimize= !no_level_minimize;
conf.comp_base_config.propagate_backbones = !no_backbone_propagation;
if (!parse_log_enc_opts(
log_enc_opts, conf.comp_base_config.enc_conf.log_conf))
......@@ -648,8 +652,8 @@ void
fill_base_conf(SUBool::AbsComp::BaseConfig &out_conf, const config_t &conf)
{
out_conf = conf.comp_base_config;
out_conf.final_simplify = conf.minimize;
out_conf.level_simplify = conf.level_simplify;
out_conf.final_minimize = conf.minimize;
out_conf.level_minimize = conf.level_minimize;
}
// std::unique_ptr<SUBool::AbsIncrementalComp>
......
......@@ -202,10 +202,10 @@ minimize(const config_t &conf, SUBool::CNF cnf)
{
return 2;
}
hyp.SimplifyRepresentation();
hyp.MinimizeRepresentation();
if (!run_with_timeout(
conf.timeout < 0.0f, conf.timeout - cpu_time.TimeSpan(),
[&hyp]() { hyp.SimplifyRepresentation(); }, "simplification"))
[&hyp]() { hyp.MinimizeRepresentation(); }, "minimization"))
{
return 2;
}
......
......@@ -24,8 +24,8 @@ const SUBool::AbsComp::StateValue SUBool::AbsComp::ERROR{
"ERROR", SUBool::AbsComp::RESULT::ERROR};
const SUBool::AbsComp::StateValue SUBool::AbsComp::UNSAT{
"UNSAT", SUBool::AbsComp::RESULT::COMPILED};
const SUBool::AbsComp::StateValue SUBool::AbsComp::SIMPLIFY{
"SIMPLIFY", SUBool::AbsComp::RESULT::UNFINISHED};
const SUBool::AbsComp::StateValue SUBool::AbsComp::MINIMIZE{
"MINIMIZE", SUBool::AbsComp::RESULT::UNFINISHED};
const SUBool::AbsComp::StateValue SUBool::AbsComp::SOLVER_INTERRUPTED{
"SOLVER_INTERRUPTED", SUBool::AbsComp::RESULT::UNFINISHED};
const SUBool::AbsComp::StateValue SUBool::AbsComp::TIMED_OUT{
......@@ -180,7 +180,7 @@ SUBool::AbsComp::Preprocess()
}
if (minimize)
{
mHypothesis.SimplifyRepresentation();
mHypothesis.MinimizeRepresentation();
}
}
......
......@@ -68,8 +68,8 @@ namespace SUBool
struct BaseConfig
{
PCEncoder::UP_EMPOWER up_empower{PCEncoder::UP_EMPOWER::ONE_LEVEL};
unsigned simp_steps{50}; // 0 means no simplification
bool final_simplify{true}; // simplify at the end of compilation
unsigned minimize_steps{50}; // 0 means no minimization
bool final_minimize{true}; // minimize at the end of compilation
PREPROCESS_METHOD preprocess{
PREPROCESS_METHOD::PRIME_MINIMIZE}; // Preprocessing method
bool propagate_backbones{true}; // If the backbones should be
......@@ -77,7 +77,7 @@ namespace SUBool
MINIMIZE_METHOD minimize_method{MINIMIZE_METHOD::FULL};
AbsEncoder::AbsConfig enc_conf{};
AbsCheckerSAT::Timeouts timeouts{};
bool level_simplify{true};
bool level_minimize{true};
LIT_IMPL_SYSTEM impl_system{LIT_IMPL_SYSTEM::Default};
SOLVER_TYPE solver_type{SOLVER_TYPE::GLUCOSE};
};
......@@ -101,7 +101,7 @@ namespace SUBool
static const StateValue ABORTED;
static const StateValue ERROR;
static const StateValue UNSAT;
static const StateValue SIMPLIFY;
static const StateValue MINIMIZE;
static const StateValue SOLVER_INTERRUPTED;
static const StateValue TIMED_OUT;
......
......@@ -22,12 +22,11 @@ const SUBool::AbsComp::StateValue SUBool::AbsIncrementalComp::INPROCESSING{
const SUBool::AbsComp::StateValue SUBool::AbsIncrementalComp::PROCESS_LEARNED{
"PROCESS_LEARNED", SUBool::AbsComp::RESULT::UNFINISHED};
SUBool::AbsIncrementalComp::AbsIncrementalComp(CNF cnf,
MINIMIZE_METHOD minimize_method,
LIT_IMPL_SYSTEM impl_system_kind)
SUBool::AbsIncrementalComp::AbsIncrementalComp(
CNF cnf, MINIMIZE_METHOD minimize_method, LIT_IMPL_SYSTEM impl_system_kind)
: AbsComp(cnf, minimize_method, impl_system_kind), mCntEmpowering(0),
mCntEmpoweringSAT(0), mCntLearned(0), mCntLearnedEmpowering(0),
mCntAdded(0), mLastSimplifyCnt(0), mCPUTime(), mRTime()
mCntAdded(0), mLastMinimizationCnt(0), mCPUTime(), mRTime()
{
}
......@@ -52,15 +51,15 @@ SUBool::AbsIncrementalComp::CompilePreprocessed()
State(TIMED_OUT);
break;
}
Simplify();
MinimizeHypothesis();
if (!emp && !CheckerSAT().WillIncreaseLevel())
{
State(FINISHED);
}
}
if (!CheckState(TIMED_OUT) && GetBaseConfig().final_simplify)
if (!CheckState(TIMED_OUT) && GetBaseConfig().final_minimize)
{
mHypothesis.SimplifyHypothesis();
mHypothesis.MinimizeHypothesis();
}
PrintStatistics(1);
}
......@@ -71,10 +70,10 @@ SUBool::AbsIncrementalComp::FindEmpowering()
CPUTime cpu_time;
mTimeTillTheLastSATEqCheck = mCPUTime.TimeSpan();
auto emp =
mHypothesis.FindEmpowering(CheckerSAT(), GetBaseConfig().level_simplify);
if (mHypothesis.HypSimplified())
mHypothesis.FindEmpowering(CheckerSAT(), GetBaseConfig().level_minimize);
if (mHypothesis.HypMinimized())
{
mLastSimplifyCnt = mCntAdded;
mLastMinimizationCnt = mCntAdded;
}
mTimeOfLastSATEqCheck = cpu_time.TimeSpan();
return emp;
......@@ -195,24 +194,24 @@ SUBool::AbsIncrementalComp::PrintStatistics(unsigned level) const
}
void
SUBool::AbsIncrementalComp::Simplify()
SUBool::AbsIncrementalComp::MinimizeHypothesis()
{
if (ShouldSimplify() && State(SIMPLIFY))
if (ShouldMinimize() && State(MINIMIZE))
{
mLastSimplifyCnt = mCntAdded;
mHypothesis.SimplifyHypothesis();
mLastMinimizationCnt = mCntAdded;
mHypothesis.MinimizeHypothesis();
}
}
bool
SUBool::AbsIncrementalComp::ShouldSimplify()
SUBool::AbsIncrementalComp::ShouldMinimize()
{
if (GetBaseConfig().level_simplify && CheckerSAT().WillIncreaseLevel())
if (GetBaseConfig().level_minimize && CheckerSAT().WillIncreaseLevel())
{
return true;
}
unsigned steps = GetBaseConfig().simp_steps;
return (steps > 0 && (mCntAdded - mLastSimplifyCnt) >= steps);
unsigned steps = GetBaseConfig().minimize_steps;
return (steps > 0 && (mCntAdded - mLastMinimizationCnt) >= steps);
}
void
......@@ -237,6 +236,6 @@ SUBool::AbsIncrementalComp::ProcessLearned()
logs.TLog(3) << "... not empowering any more" << std::endl;
}
}
Simplify();
MinimizeHypothesis();
}
......@@ -37,8 +37,8 @@ namespace SUBool
std::atomic<unsigned> mCntLearned;
std::atomic<unsigned> mCntLearnedEmpowering;
std::atomic<unsigned> mCntAdded; // excluding preprocessing
unsigned mLastSimplifyCnt; // Value of mCntAdded at the time of the last
// simplification.
unsigned mLastMinimizationCnt; // Value of mCntAdded at the time of the
// last minimization.
CPUTime mCPUTime;
RealTime mRTime;
......@@ -51,8 +51,8 @@ namespace SUBool
virtual std::string ResultDesc() const override;
virtual std::string Annotation() const override;
virtual void Simplify();
virtual bool ShouldSimplify();
virtual void MinimizeHypothesis();
virtual bool ShouldMinimize();
virtual void CompilePreprocessed() override;
virtual std::optional<Clause> FindEmpowering();
......@@ -61,7 +61,7 @@ namespace SUBool
public:
AbsIncrementalComp(CNF cnf, MINIMIZE_METHOD minimize_method,
LIT_IMPL_SYSTEM impl_system_kind);
LIT_IMPL_SYSTEM impl_system_kind);
virtual ~AbsIncrementalComp() = default;
virtual void PrintStatistics(unsigned level) const override;
......
......@@ -12,37 +12,36 @@
#include "cpuutil.h"
#include "propagate.h"
SUBool::CompHypothesis::CompHypothesis(MINIMIZE_METHOD minimize_method,
LIT_IMPL_SYSTEM impl_system_kind)
SUBool::CompHypothesis::CompHypothesis(
MINIMIZE_METHOD minimize_method, LIT_IMPL_SYSTEM impl_system_kind)
: mRepresentation(), mHypothesis(), mSolver(), mSafe(false),
mOneProveRepr(mRepresentation), mOneProveHyp(mHypothesis),
mMinSubimplicant(&mRepresentation),
mSemPropagator(mSolver.GetSolverPtr(), &(mOneProveRepr.UP()),
&mMinSubimplicant),
mSemPropagator(
mSolver.GetSolverPtr(), &(mOneProveRepr.UP()), &mMinSubimplicant),
mMutex(), mMinimizeMethod(minimize_method),
mImplSystemKind(impl_system_kind)
{
}
SUBool::CompHypothesis::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)
: mRepresentation(std::move(repr)), mHypothesis(std::move(cnf)),
mSolver(safe ? mHypothesis : mRepresentation), mSafe(safe),
mOneProveRepr(mRepresentation), mOneProveHyp(mHypothesis),
mMinSubimplicant(safe ? &mHypothesis : &mRepresentation),
mSemPropagator(mSolver.GetSolverPtr(),
safe ? &(mOneProveHyp.UP()) : &(mOneProveRepr.UP()),
&mMinSubimplicant),
safe ? &(mOneProveHyp.UP()) : &(mOneProveRepr.UP()),
&mMinSubimplicant),
mMutex(), mMinimizeMethod(minimize_method),
mImplSystemKind(impl_system_kind)
{
}
size_t
SUBool::CompHypothesis::SimplifyLogProgress(size_t cnf_size)
SUBool::CompHypothesis::MinimizationLogProgress(size_t cnf_size)
{
if (cnf_size < kSimpLogThreshold)
if (cnf_size < kMinimizationLogThreshold)
{
return 0;
}
......@@ -55,13 +54,13 @@ SUBool::CompHypothesis::ResetSemPropagator()
if (mSafe)
{
mMinSubimplicant.Reset(&mHypothesis);
mSemPropagator.Reset(mSolver.GetSolverPtr(), &(mOneProveHyp.UP()),
&mMinSubimplicant);
mSemPropagator.Reset(
mSolver.GetSolverPtr(), &(mOneProveHyp.UP()), &mMinSubimplicant);
return;
}
mMinSubimplicant.Reset(&mRepresentation);
mSemPropagator.Reset(mSolver.GetSolverPtr(), &(mOneProveRepr.UP()),
&mMinSubimplicant);
mSemPropagator.Reset(
mSolver.GetSolverPtr(), &(mOneProveRepr.UP()), &mMinSubimplicant);
}
void
......@@ -78,7 +77,7 @@ SUBool::CompHypothesis::ClearHypothesis()
std::lock_guard<SharedMutex> lock(mMutex);
mHypothesis.Clear();
mSafe = false;
mHypSimplified = true;
mHypMinimized = true;
mOneProveHyp = OneProveM();
mImplSystemInitialized = false;
mSCCGraphInitialized = false;
......@@ -90,7 +89,7 @@ SUBool::CompHypothesis::SetHypothesis(CNF cnf, bool safe)
{
std::lock_guard<SharedMutex> lock(mMutex);
mHypothesis = std::move(cnf);
mHypSimplified = false;
mHypMinimized = false;
mOneProveHyp = OneProveM(mHypothesis);
mSafe = safe;
mImplSystemInitialized = false;
......@@ -103,7 +102,7 @@ SUBool::CompHypothesis::SetHypothesisToRepresentation()
{
SetHypothesis(GetRepresentation(false), true);
std::lock_guard<SharedMutex> lock(mMutex);
mHypSimplified = mReprSimplified;
mHypMinimized = mReprMinimized;
}
SUBool::CNF
......@@ -142,7 +141,7 @@ void
SUBool::CompHypothesis::InnerSetRepresentation(CNF cnf)
{
mRepresentation = std::move(cnf);
mReprSimplified = false;
mReprMinimized = false;
mSafe = false;
mOneProveRepr = OneProveM(mRepresentation);
ResetSolver();
......@@ -308,8 +307,8 @@ SUBool::CompHypothesis::CompressLearnts(const PartialAssignment &alpha)
}
break;
case PartialValue::FALSE:
throw InvariantFailedException("CompHypothesis::CompressLearnts",
"Formula is unsatisfiable");
throw InvariantFailedException(
"CompHypothesis::CompressLearnts", "Formula is unsatisfiable");
case PartialValue::TRUE:
default:
break;
......@@ -330,8 +329,8 @@ SUBool::CompHypothesis::CompressLearnts(const PartialAssignment &alpha)
++queue_cnt;
break;
case PartialValue::FALSE:
throw InvariantFailedException("CompHypothesis::CompressLearnts",
"Formula is unsatisfiable");
throw InvariantFailedException(
"CompHypothesis::CompressLearnts", "Formula is unsatisfiable");
case PartialValue::TRUE:
default:
break;
......@@ -353,9 +352,9 @@ SUBool::CompHypothesis::PropagatePartialAssignment(
mCompressor = CNFCompressor(mRepresentation);
mRepresentation = mCompressor.CompressCNF(std::move(mRepresentation));
mHypothesis = mCompressor.CompressCNF(std::move(mHypothesis));
mReprSimplified = false;
mReprMinimized = false;
mOneProveRepr = OneProveM(mRepresentation);
mHypSimplified = false;
mHypMinimized = false;
mOneProveHyp = OneProveM(mHypothesis);
mImplSystemInitialized = false;
mSCCGraphInitialized = false;
......@@ -418,35 +417,35 @@ SUBool::CompHypothesis::EmpoweredLiteral(const Clause &clause)
}
bool
SUBool::CompHypothesis::InnerSimplifyHypothesis()
SUBool::CompHypothesis::InnerMinimizeHypothesis()
{
if (mHypSimplified)
if (mHypMinimized)
{
return false;
}
SimplifyCNF(true);
mHypSimplified = true;
MinimizeCNF(true);
mHypMinimized = true;
mImplSystemInitialized = false;
return true;
}
bool
SUBool::CompHypothesis::SimplifyHypothesis()
SUBool::CompHypothesis::MinimizeHypothesis()
{
std::lock_guard<SharedMutex> lock(mMutex);
return InnerSimplifyHypothesis();
return InnerMinimizeHypothesis();
}
bool
SUBool::CompHypothesis::SimplifyRepresentation()
SUBool::CompHypothesis::MinimizeRepresentation()
{
std::lock_guard<SharedMutex> lock(mMutex);
if (mReprSimplified)
if (mReprMinimized)
{
return false;
}
SimplifyCNF(false);
mReprSimplified = true;
MinimizeCNF(false);
mReprMinimized = true;
return true;
}
......@@ -455,14 +454,14 @@ SUBool::CompHypothesis::MinimizeReprWithCollectingEmpowered(bool collect_all)
{
std::lock_guard<SharedMutex> lock(mMutex);
auto clauses_with_emp = mOneProveRepr.MinimizeWithCollectingEmpowered(
collect_all, SimplifyLogProgress(mRepresentation.Size()));
collect_all, MinimizationLogProgress(mRepresentation.Size()));
mRepresentation = mOneProveRepr.ExtractCNF();
mReprSimplified = true;
mReprMinimized = true;
return clauses_with_emp;
}
void
SUBool::CompHypothesis::SimplifyCNF(bool use_hypothesis)
SUBool::CompHypothesis::MinimizeCNF(bool use_hypothesis)
{
CPUTime cpu_time;
auto name = (use_hypothesis ? "hypothesis" : "representation");
......@@ -474,19 +473,19 @@ SUBool::CompHypothesis::SimplifyCNF(bool use_hypothesis)
switch (mMinimizeMethod)
{
case MINIMIZE_METHOD::FULL:
op.MinimizeFull(SimplifyLogProgress(cnf.Size()));
op.MinimizeFull(MinimizationLogProgress(cnf.Size()));
break;
case MINIMIZE_METHOD::SIMPLE_INCREMENTAL:
reprocess = false;
[[fallthrough]];
case MINIMIZE_METHOD::FULL_INCREMENTAL:
op = OneProveM();
op.AddWithIncrementalMinimization(cnf, reprocess,
SimplifyLogProgress(cnf.Size()));
op.AddWithIncrementalMinimization(
cnf, reprocess, MinimizationLogProgress(cnf.Size()));
break;
default:
throw InvariantFailedException("CompHypothesis::SimplifyCNF",
"unknown minimization method");
throw InvariantFailedException(
"CompHypothesis::MinimizeCNF", "unknown minimization method");
}
cnf = op.ExtractCNF();
if (use_hypothesis == mSafe)
......@@ -513,13 +512,12 @@ SUBool::CompHypothesis::IsImplicate(const Clause &clause) const
}
std::optional<SUBool::Clause>
SUBool::CompHypothesis::PrimeSubimplicate(const Clause &clause,
unsigned ignore_var,
bool promised_sat) const
SUBool::CompHypothesis::PrimeSubimplicate(
const Clause &clause, unsigned ignore_var, bool promised_sat) const
{
SharedLockGuard lock(mMutex);
return prime_subimplicate(mSolver.Solver(), clause, ignore_var,
promised_sat);
return prime_subimplicate(
mSolver.Solver(), clause, ignore_var, promised_sat);
}
void
......@@ -578,17 +576,17 @@ SUBool::CompHypothesis::FindEmpoweringQuery(AbsCheckerSAT &checker)
}
std::optional<SUBool::Clause>
SUBool::CompHypothesis::FindEmpowering(AbsCheckerSAT &checker,
bool level_simplify)
SUBool::CompHypothesis::FindEmpowering(
AbsCheckerSAT &checker, bool level_minimize)
{
std::optional<Clause> emp_result = FindEmpoweringQuery(checker);
if (emp_result || !checker.WillIncreaseLevel())
{
return emp_result;
}
if (level_simplify)
if (level_minimize)
{
SimplifyHypothesis();
MinimizeHypothesis();
}
return FindEmpoweringQuery(checker);
}
......@@ -601,7 +599,7 @@ SUBool::CompHypothesis::PushBack(Clause c)
// adding it to the solver is always safe
mSolver.Solver().AddClause(c);
mHypothesis.PushBack(c);
mHypSimplified = false;
mHypMinimized = false;
AddClauseToImplSystem(c);
mOneProveHyp.AddClause(std::move(c));
if (mSafe)
......@@ -611,8 +609,8 @@ SUBool::CompHypothesis::PushBack(Clause c)
}
bool
SUBool::CompHypothesis::PushIfEmpowering(const Clause &c,
bool find_prime_subimplicate)
SUBool::CompHypothesis::PushIfEmpowering(
const Clause &c, bool find_prime_subimplicate)
{
auto l = EmpoweredLiteral(c);
if (!l)
......@@ -624,8 +622,8 @@ SUBool::CompHypothesis::PushIfEmpowering(const Clause &c,
auto prime = PrimeSubimplicate(c, l->Variable(), true);
if (!prime)
{
throw InvariantFailedException("CompHypothesis::PushIfEmpowering",
"Not an implicate");
throw InvariantFailedException(
"CompHypothesis::PushIfEmpowering", "Not an implicate");
}
PushBack(std::move(*prime));
}
......
......@@ -31,8 +31,8 @@ namespace SUBool
MinimalSubimplicant mMinSubimplicant;
Propagator mSemPropagator;
mutable SharedMutex mMutex;
bool mHypSimplified{false};
bool mReprSimplified{false};
bool mHypMinimized{false};
bool mReprMinimized{false};
MINIMIZE_METHOD mMinimizeMethod{MINIMIZE_METHOD::FULL};
LIT_IMPL_SYSTEM mImplSystemKind{LIT_IMPL_SYSTEM::Default};
std::vector<Literal> mBackbone{};
......@@ -47,8 +47,8 @@ namespace SUBool
const CNF &TheRightCNF() const;
static size_t SimplifyLogProgress(size_t cnf_size);
void SimplifyCNF(bool use_hypothesis);
static size_t MinimizationLogProgress(size_t cnf_size);
void MinimizeCNF(bool use_hypothesis);
void InnerSetRepresentation(CNF cnf);
void ResetSolver();
void ResetSemPropagator();
......@@ -56,7 +56,7 @@ namespace SUBool
void ExtractLearnts();
void CompressLearnts(const PartialAssignment &alpha);
bool AddLearnt(Clause clause);
bool InnerSimplifyHypothesis(); // true if simplification executed
bool InnerMinimizeHypothesis(); // true if minimization executed
void InitImplSystem();
void InitSCCGraph();
void AddClauseToImplSystem(const Clause &c);
......@@ -65,7 +65,7 @@ namespace SUBool
void PropagatePartialAssignment(const PartialAssignment &alpha);
public:
static const unsigned kSimpLogThreshold = 3000;
static const unsigned kMinimizationLogThreshold = 3000;
CompHypothesis(
MINIMIZE_METHOD minimize_method, LIT_IMPL_SYSTEM impl_system_kind);
......@@ -81,10 +81,10 @@ namespace SUBool
CNF GetRepresentation(bool uncompress) const &;
CNF GetRepresentation(bool uncompress) &&;
bool
HypSimplified() const
HypMinimized() const
{
SharedLockGuard lock(mMutex);
return mHypSimplified;
return mHypMinimized;
}
template <typename F>
auto
......@@ -115,8 +115,8 @@ namespace SUBool</