mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-28 19:01:29 +00:00
Code Activity

Add fallback lemma

Browse source
This commit is contained in:
Jakob Rath 2021-09-06 18:00:21 +02:00
parent 381d13993c
commit 15c094fa32
3 changed files with 52 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/solver.h
View file

@ -168,6 +168,7 @@ namespace polysat {
void assign_core(pvar v, rational const& val, justification const& j);
bool is_assigned(pvar v) const { return !m_justification[v].is_unassigned(); }
bool is_decision(search_item const& item) const;
bool should_search();
@ -216,6 +217,7 @@ namespace polysat {
void resolve_bool(sat::literal lit);
void revert_decision(pvar v);
void revert_bool_decision(sat::literal lit);
clause_ref mk_fallback_lemma(unsigned lvl);
void report_unsat();
void learn_lemma(pvar v, clause_ref lemma);