From 47324af210500af2d840595e8d1b493c5f7b1c90 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 29 Dec 2022 11:08:57 +0000 Subject: [PATCH] be nicer when memout is reached in SMT internalize: return undef rather than crashing --- src/smt/smt_context.cpp | 41 ++++++++++++++++++++++++++---------- src/smt/smt_context.h | 2 ++ src/smt/smt_internalizer.cpp | 2 +- 3 files changed, 33 insertions(+), 12 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index d1cf2d87521..01e0aba7c81 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -2961,7 +2961,11 @@ namespace smt { pop_to_base_lvl(); setup_context(false); bool was_consistent = !inconsistent(); - internalize_assertions(); // internalize assertions before invoking m_asserted_formulas.push_scope + try { + internalize_assertions(); // internalize assertions before invoking m_asserted_formulas.push_scope + } catch (cancel_exception&) { + throw default_exception("Resource limits hit in push"); + } if (!m.inc()) throw default_exception("push canceled"); scoped_suspend_rlimit _suspend_cancel(m.limit()); @@ -3556,7 +3560,12 @@ namespace smt { return p(asms); } - internalize_assertions(); + try { + internalize_assertions(); + } catch (cancel_exception&) { + VERIFY(resource_limits_exceeded()); + return l_undef; + } expr_ref_vector theory_assumptions(m); add_theory_assumptions(theory_assumptions); if (!theory_assumptions.empty()) { @@ -3620,10 +3629,15 @@ namespace smt { do { pop_to_base_lvl(); expr_ref_vector asms(m, num_assumptions, assumptions); - internalize_assertions(); - add_theory_assumptions(asms); - TRACE("unsat_core_bug", tout << asms << "\n";); - init_assumptions(asms); + try { + internalize_assertions(); + add_theory_assumptions(asms); + TRACE("unsat_core_bug", tout << asms << '\n';); + init_assumptions(asms); + } catch (cancel_exception&) { + VERIFY(resource_limits_exceeded()); + return l_undef; + } TRACE("before_search", display(tout);); r = search(); r = mk_unsat_core(r); @@ -3641,11 +3655,16 @@ namespace smt { do { pop_to_base_lvl(); expr_ref_vector asms(cube); - internalize_assertions(); - add_theory_assumptions(asms); - // introducing proxies: if (!validate_assumptions(asms)) return l_undef; - for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef; - init_assumptions(asms); + try { + internalize_assertions(); + add_theory_assumptions(asms); + // introducing proxies: if (!validate_assumptions(asms)) return l_undef; + for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef; + init_assumptions(asms); + } catch (cancel_exception&) { + VERIFY(resource_limits_exceeded()); + return l_undef; + } for (auto const& clause : clauses) init_clause(clause); r = search(); r = mk_unsat_core(r); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index b6bf04a20e2..7a267fdeca1 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -62,6 +62,8 @@ namespace smt { class model_generator; + struct cancel_exception {}; + class context { friend class model_generator; friend class lookahead; diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 26e23d92d93..3a7b95e2c49 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -353,7 +353,7 @@ namespace smt { */ void context::internalize(expr * n, bool gate_ctx) { if (memory::above_high_watermark()) - throw default_exception("resource limit exceeded during internalization"); + throw cancel_exception(); internalize_deep(n); internalize_rec(n, gate_ctx); }