cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Add interface to make theory solver aware of decision levels.

Browse Source
This commit is contained in:
chriseth 2022-03-23 19:21:36 +01:00
parent 0c89ef6863
commit 4171716e72
3 changed files with 13 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
libsolutil/BooleanLP.cpp
View File

@ -248,7 +248,7 @@ pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> cons
} }
set<size_t> previousConditionalConstraints; set<size_t> previousConditionalConstraints;
auto theorySolver = [&](map<size_t, bool> const& _booleanAssignment) -> optional<Clause> auto theorySolver = [&](size_t /*_decisionLevel*/, map<size_t, bool> const& _booleanAssignment) -> optional<Clause>
{ {
SolvingState lpStateToCheck = lpState; SolvingState lpStateToCheck = lpState;
set<size_t> conditionalConstraints; set<size_t> conditionalConstraints;
@ -281,8 +281,9 @@ pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> cons
else else
return nullopt; return nullopt;
}; };
auto backtrackNotify = [](size_t /*_decisionLevel*/) {};
auto optionalModel = CDCL{move(booleanVariables), clauses, theorySolver}.solve(); auto optionalModel = CDCL{move(booleanVariables), clauses, theorySolver, backtrackNotify}.solve();
if (!optionalModel) if (!optionalModel)
{ {
cout << "==============> CDCL final result: unsatisfiable." << endl; cout << "==============> CDCL final result: unsatisfiable." << endl;

8
libsolutil/CDCL.cpp
View File

@ -32,9 +32,11 @@ using namespace solidity::util;
CDCL::CDCL( CDCL::CDCL(
vector<string> _variables, vector<string> _variables,
vector<Clause> const& _clauses, vector<Clause> const& _clauses,
std::function<std::optional<Clause>(std::map<size_t, bool> const&)> _theorySolver std::function<std::optional<Clause>(size_t, std::map<size_t, bool> const&)> _theorySolver,
std::function<void(size_t)> _backtrackNotify
): ):
m_theorySolver(_theorySolver), m_theorySolver(_theorySolver),
m_backtrackNotify(_backtrackNotify),
m_variables(move(_variables)), m_variables(move(_variables)),
order(VarOrderLt(activity)) order(VarOrderLt(activity))
{ {
@ -69,7 +71,7 @@ bool CDCL::solve_loop(const uint32_t max_conflicts, CDCL::Model& model, int& sol
optional<Clause> conflictClause = propagate(); optional<Clause> conflictClause = propagate();
if (!conflictClause && m_theorySolver) if (!conflictClause && m_theorySolver)
{ {
conflictClause = m_theorySolver(m_assignments); conflictClause = m_theorySolver(currentDecisionLevel(), m_assignments);
// if (conflictClause) // if (conflictClause)
// cout << "Theory gave us conflict: " << toString(*conflictClause) << endl; // cout << "Theory gave us conflict: " << toString(*conflictClause) << endl;
} }
@ -323,6 +325,8 @@ void CDCL::cancelUntil(size_t _backtrackLevel)
} }
m_decisionPoints.resize(_backtrackLevel); m_decisionPoints.resize(_backtrackLevel);
m_assignmentQueuePointer = m_assignmentTrail.size(); m_assignmentQueuePointer = m_assignmentTrail.size();
if (m_backtrackNotify)
m_backtrackNotify(currentDecisionLevel());
solAssert(currentDecisionLevel() == _backtrackLevel); solAssert(currentDecisionLevel() == _backtrackLevel);
} }

6
libsolutil/CDCL.h
View File

@ -59,7 +59,8 @@ public:
CDCL( CDCL(
std::vector<std::string> _variables, std::vector<std::string> _variables,
std::vector<Clause> const& _clauses, std::vector<Clause> const& _clauses,
std::function<std::optional<Clause>(std::map<size_t, bool> const&)> _theoryPropagator = {} std::function<std::optional<Clause>(size_t, std::map<size_t, bool> const&)> _theorySolver = {},
std::function<void(size_t)> _backtrackNotify = {}
); );
std::optional<Model> solve(); std::optional<Model> solve();
@ -102,7 +103,8 @@ private:
/// Callback that receives an assignment and uses the theory to either returns nullopt ("satisfiable") /// Callback that receives an assignment and uses the theory to either returns nullopt ("satisfiable")
/// or a conflict clause, i.e. a clauses that is false in the theory with the given assignments. /// or a conflict clause, i.e. a clauses that is false in the theory with the given assignments.
std::function<std::optional<Clause>(std::map<size_t, bool>)> m_theorySolver; std::function<std::optional<Clause>(size_t, std::map<size_t, bool>)> m_theorySolver;
std::function<void(size_t)> m_backtrackNotify;
std::vector<std::string> m_variables; std::vector<std::string> m_variables;
/// includes the learnt clauses /// includes the learnt clauses