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

Refactoring

parent f1993a9b
......@@ -547,14 +547,7 @@ SUBool::CompHypothesis::FindEmpoweringQuery(AbsCheckerSAT &checker)
{
SharedLockGuard lock(mMutex);
ClausesToLiterals cl2lit(mHypothesis);
if (!mImplSystemInitialized)
{
logs.TLog(3) << "[CompHypothesis::FindEmpoweringQuery] Initializing "
"the implication system"
<< std::endl;
mImplSystemProvider->Cleanup(mHypothesis);
mImplSystemInitialized = true;
}
UpdateISProvider();
if (checker.RequiresSCCGraph())
{
mImplSystemProvider->RebuildSCCGraph();
......@@ -562,8 +555,8 @@ SUBool::CompHypothesis::FindEmpoweringQuery(AbsCheckerSAT &checker)
return checker.FindEmpowering(mHypothesis, cl2lit, mImplSystemProvider);
}
const SUBool::EncISProvider &
SUBool::CompHypothesis::ImplSystemProvider()
void
SUBool::CompHypothesis::UpdateISProvider()
{
if (!mImplSystemInitialized)
{
......@@ -573,6 +566,13 @@ SUBool::CompHypothesis::ImplSystemProvider()
mImplSystemProvider->Cleanup(mHypothesis);
mImplSystemInitialized = true;
}
}
const SUBool::EncISProvider &
SUBool::CompHypothesis::ImplSystemProvider()
{
SharedLockGuard lock(mMutex);
UpdateISProvider();
return *mImplSystemProvider;
}
......
......@@ -81,7 +81,7 @@ namespace SUBool
void CompressLearnts(const PartialAssignment &alpha);
bool AddLearnt(Clause clause);
bool InnerMinimizeHypothesis(); // true if minimization executed
void InitImplSystem();
void UpdateISProvider();
std::optional<Clause> FindEmpoweringQuery(AbsCheckerSAT &checker);
bool PropagateBackbones(bool use_sat);
void PropagatePartialAssignment(const PartialAssignment &alpha);
......
......@@ -55,7 +55,7 @@ namespace SUBool
PCLearnComp::INITIAL_NEGATIVES::BODY_MINIMAL};
PCLearnComp::CANDIDATES_FROM_NEGATIVE_POLICY
kDefaultCandidatesFromNegativePolicy{
PCLearnComp::CANDIDATES_FROM_NEGATIVE_POLICY::UNITPROP};
PCLearnComp::CANDIDATES_FROM_NEGATIVE_POLICY::SYNCHRONIZE};
private:
EnumOption<PCLearnComp::INITIAL_NEGATIVES> mInitialNegativesOption;
......
......@@ -73,7 +73,7 @@ namespace SUBool
double cache_time_logging_threshold{0.001};
INITIAL_NEGATIVES initial_negatives{INITIAL_NEGATIVES::BODY_MINIMAL};
CANDIDATES_FROM_NEGATIVE_POLICY candidates_from_negative_policy{
CANDIDATES_FROM_NEGATIVE_POLICY::UNITPROP};
CANDIDATES_FROM_NEGATIVE_POLICY::SYNCHRONIZE};
bool use_cnf_hypothesis_for_empowerment{false};
Config() noexcept {}
......
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