mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

local

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-04-02 17:40:34 -07:00
parent ff6d703c05
commit 6360798a53
2 changed files with 15 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/smt/smt_context.cpp
View file

@ -86,8 +86,7 @@ namespace smt {
m_generation(0), m_generation(0),
m_last_search_result(l_undef), m_last_search_result(l_undef),
m_last_search_failure(UNKNOWN), m_last_search_failure(UNKNOWN),
m_searching(false), m_searching(false) {
m_propagating(false) {
SASSERT(m_scope_lvl == 0); SASSERT(m_scope_lvl == 0);
SASSERT(m_base_lvl == 0); SASSERT(m_base_lvl == 0);
@ -134,11 +133,10 @@ namespace smt {
/** /**
\brief retrieve flag for when cancelation is possible. \brief retrieve flag for when cancelation is possible.
Cancelation is not safe during propagation at base level because
congruences cannot be retracted to a consistent state.
*/ */
bool context::get_cancel_flag() { bool context::get_cancel_flag() {
return !m_manager.limit().inc() && !(at_base_level() && m_propagating); return !m_manager.limit().inc();
} }
void context::updt_params(params_ref const& p) { void context::updt_params(params_ref const& p) {
@ -1701,8 +1699,13 @@ namespace smt {
!m_th_diseq_propagation_queue.empty(); !m_th_diseq_propagation_queue.empty();
} }
/**
\brief unit propagation.
Cancelation is not safe during propagation at base level because
congruences cannot be retracted to a consistent state.
*/
bool context::propagate() { bool context::propagate() {
flet<bool> _prop(m_propagating, true); scoped_suspend_rlimit _suspend_cancel(m_manager.limit(), at_base_level());
TRACE("propagate", tout << "propagating... " << m_qhead << ":" << m_assigned_literals.size() << "\n";); TRACE("propagate", tout << "propagating... " << m_qhead << ":" << m_assigned_literals.size() << "\n";);
while (true) { while (true) {
if (inconsistent()) if (inconsistent())

5
src/util/rlimit.h
View file

@ -71,6 +71,11 @@ public:
m_suspend = r.m_suspend; m_suspend = r.m_suspend;
r.m_suspend = true; r.m_suspend = true;
} }
scoped_suspend_rlimit(reslimit& r, bool do_suspend): m_limit(r) {
m_suspend = r.m_suspend;
r.m_suspend |= do_suspend;
}
~scoped_suspend_rlimit() { ~scoped_suspend_rlimit() {
m_limit.m_suspend = m_suspend; m_limit.m_suspend = m_suspend;
} }