mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

moving to resource managed cancellation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-11 16:56:23 -08:00 • committed by Christoph M. Wintersteiger
parent a9723fb6c7
commit d4a90d7ec3
7 changed files with 13 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/api/api_polynomial.cpp
View file

@ -61,6 +61,7 @@ extern "C" {
polynomial_ref_vector rs(pm);
polynomial_ref r(pm);
expr_ref _r(mk_c(c)->m());
{
cancel_eh<reslimit> eh(mk_c(c)->poly_limit());
api::context::set_interruptable si(*(mk_c(c)), eh);

2
src/ast/rewriter/rewriter_def.h
View file

@ -575,7 +575,7 @@ template<bool ProofGen>
void rewriter_tpl<Config>::resume_core(expr_ref & result, proof_ref & result_pr) {
SASSERT(!frame_stack().empty());
while (!frame_stack().empty()) {
if (!m().canceled()) {
if (m().canceled()) {
if (m().limit().cancel_flag_set()) {
throw rewriter_exception(Z3_CANCELED_MSG);
}

2
src/muz/base/hnf.cpp
View file

@ -173,7 +173,7 @@ public:
}
bool checkpoint() {
return m.limit().inc();
return !m.canceled();
}
void set_name(symbol const& n) {

6
src/muz/bmc/dl_bmc_engine.cpp
View file

@ -483,7 +483,7 @@ namespace datalog {
}
proof_ref get_proof(model_ref& md, func_decl* pred, app* prop, unsigned level) {
if (!m.limit().inc()) {
if (m.canceled()) {
return proof_ref(0, m);
}
TRACE("bmc", tout << "Predicate: " << pred->get_name() << "\n";);
@ -1172,7 +1172,7 @@ namespace datalog {
private:
void get_model(unsigned level) {
if (!m.limit().inc()) {
if (m.canceled()) {
return;
}
rule_manager& rm = b.m_ctx.get_rule_manager();
@ -1509,7 +1509,7 @@ namespace datalog {
}
void bmc::checkpoint() {
if (!m.limit().inc()) {
if (m.canceled()) {
throw default_exception("bmc canceled");
}
}

2
src/muz/pdr/pdr_context.cpp
View file

@ -1911,7 +1911,7 @@ namespace pdr {
}
void context::checkpoint() {
if (!m.limit().inc()) {
if (m.canceled()) {
throw default_exception("pdr canceled");
}
}

10
src/muz/tab/tab_context.cpp
View file

@ -581,7 +581,7 @@ namespace tb {
// extract pre_cond => post_cond validation obligation from match.
bool find_match(unsigned& subsumer) {
for (unsigned i = 0; m.limit().inc() && i < m_index.size(); ++i) {
for (unsigned i = 0; !m.canceled() && i < m_index.size(); ++i) {
if (match_rule(i)) {
subsumer = m_index[i]->get_seqno();
return true;
@ -618,7 +618,7 @@ namespace tb {
app* q = g.get_predicate(predicate_index);
for (unsigned i = 0; m.limit().inc() && i < m_preds.size(); ++i) {
for (unsigned i = 0; !m.canceled() && i < m_preds.size(); ++i) {
app* p = m_preds[i].get();
m_subst.push_scope();
unsigned limit = m_sideconds.size();
@ -647,7 +647,7 @@ namespace tb {
expr_ref_vector fmls(m_sideconds);
m_subst.reset_cache();
for (unsigned i = 0; m.limit().inc() && i < fmls.size(); ++i) {
for (unsigned i = 0; !m.canceled() && i < fmls.size(); ++i) {
m_subst.apply(2, deltas, expr_offset(fmls[i].get(), 0), q);
fmls[i] = q;
}
@ -664,7 +664,7 @@ namespace tb {
}
}
m_rw.mk_and(fmls.size(), fmls.c_ptr(), postcond);
if (!m.limit().inc()) {
if (m.canceled()) {
return false;
}
if (m.is_false(postcond)) {
@ -1495,7 +1495,7 @@ namespace datalog {
m_status = l_undef;
while (true) {
IF_VERBOSE(2, verbose_stream() << m_instruction << "\n";);
if (!m.limit().inc()) {
if (m.canceled()) {
cleanup();
return l_undef;
}

2
src/muz/transforms/dl_mk_karr_invariants.cpp
View file

@ -208,7 +208,7 @@ namespace datalog {
get_invariants(*src_loop);
if (!m.limit().inc()) {
if (m.canceled()) {
return 0;
}