From a7e2fb31e3e7a19aa79ed482633d75252c2df946 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 12 Dec 2015 11:36:49 -0800 Subject: [PATCH] updates to resource exceptions, update master possibly handle pull request issue Signed-off-by: Nikolaj Bjorner --- src/ast/normal_forms/nnf.cpp | 2 +- src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h | 2 +- src/qe/qe.cpp | 2 +- src/qe/qe_lite.cpp | 10 +++++----- src/qe/qe_sat_tactic.cpp | 2 +- src/qe/qe_tactic.cpp | 2 +- src/sat/tactic/goal2sat.cpp | 4 ++-- src/smt/smt_model_finder.cpp | 2 +- src/smt/tactic/unit_subsumption_tactic.cpp | 2 +- src/smt/theory_seq.cpp | 7 +++++++ src/smt/theory_seq.h | 4 +--- src/tactic/aig/aig.cpp | 2 +- src/tactic/arith/arith_bounds_tactic.cpp | 2 +- src/tactic/arith/degree_shift_tactic.cpp | 2 +- src/tactic/arith/diff_neq_tactic.cpp | 2 +- src/tactic/arith/fm_tactic.cpp | 4 ++-- src/tactic/bv/bv_size_reduction_tactic.cpp | 2 +- src/tactic/bv/bvarray2uf_tactic.cpp | 2 +- src/tactic/core/cofactor_elim_term_ite.cpp | 2 +- src/tactic/core/ctx_simplify_tactic.cpp | 2 +- src/tactic/core/reduce_args_tactic.cpp | 2 +- src/tactic/core/solve_eqs_tactic.cpp | 4 ++-- src/tactic/sls/sls_engine.cpp | 2 +- src/tactic/ufbv/quasi_macros_tactic.cpp | 4 ++-- 24 files changed, 38 insertions(+), 33 deletions(-) diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index 0d8aa90e3..6b10e8c10 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -373,7 +373,7 @@ struct nnf::imp { if (memory::get_allocation_size() > m_max_memory) throw nnf_exception(Z3_MAX_MEMORY_MSG); if (m().canceled()) - throw nnf_exception(Z3_CANCELED_MSG); + throw nnf_exception(m().limit().get_cancel_msg()); } void set_new_child_flag() { diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index 74721d981..38a608f5f 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -28,7 +28,7 @@ void bit_blaster_tpl::checkpoint() { if (memory::get_allocation_size() > m_max_memory) throw rewriter_exception(Z3_MAX_MEMORY_MSG); if (m().canceled()) - throw rewriter_exception(Z3_CANCELED_MSG); + throw rewriter_exception(m().limit().get_cancel_msg()); cooperate("bit-blaster"); } diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index 846cb6c68..150198bab 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -2051,7 +2051,7 @@ namespace qe { void checkpoint() { if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); cooperate("qe"); } diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 4364d4a21..9a981cc9b 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -738,7 +738,7 @@ namespace eq { void checkpoint() { cooperate("der"); if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); } public: @@ -917,8 +917,8 @@ namespace ar { void checkpoint() { cooperate("der"); if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); - } + throw tactic_exception(m.limit().get_cancel_msg()); + } public: @@ -2207,7 +2207,7 @@ namespace fm { void checkpoint() { cooperate("fm"); if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); } public: @@ -2477,7 +2477,7 @@ class qe_lite_tactic : public tactic { void checkpoint() { if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); cooperate("qe-lite"); } diff --git a/src/qe/qe_sat_tactic.cpp b/src/qe/qe_sat_tactic.cpp index d3e145e1b..455c1d08e 100644 --- a/src/qe/qe_sat_tactic.cpp +++ b/src/qe/qe_sat_tactic.cpp @@ -662,7 +662,7 @@ namespace qe { void checkpoint() { if (m.canceled()) { - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); } cooperate("qe-sat"); } diff --git a/src/qe/qe_tactic.cpp b/src/qe/qe_tactic.cpp index d72727250..c8660b916 100644 --- a/src/qe/qe_tactic.cpp +++ b/src/qe/qe_tactic.cpp @@ -45,7 +45,7 @@ class qe_tactic : public tactic { void checkpoint() { if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); cooperate("qe"); } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index fbf34e741..b82f00a92 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -333,7 +333,7 @@ struct goal2sat::imp { loop: cooperate("goal2sat"); if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); frame & fr = m_frame_stack.back(); @@ -626,7 +626,7 @@ struct sat2goal::imp { void checkpoint() { if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); } diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 1f51e8bf2..2e260cbca 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -3318,7 +3318,7 @@ namespace smt { void model_finder::checkpoint(char const* msg) { cooperate(msg); if (m_context && m_context->get_cancel_flag()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m_context->get_manager().limit().get_cancel_msg()); } mf::quantifier_info * model_finder::get_quantifier_info(quantifier * q) const { diff --git a/src/smt/tactic/unit_subsumption_tactic.cpp b/src/smt/tactic/unit_subsumption_tactic.cpp index ab7b40a26..745bfa2de 100644 --- a/src/smt/tactic/unit_subsumption_tactic.cpp +++ b/src/smt/tactic/unit_subsumption_tactic.cpp @@ -58,7 +58,7 @@ struct unit_subsumption_tactic : public tactic { void checkpoint() { if (m.canceled()) { - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); } } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index a402437d3..f0b82adbb 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -86,6 +86,13 @@ void theory_seq::solution_map::display(std::ostream& out) const { } } +bool theory_seq::exclusion_table::contains(expr* e, expr* r) const { + if (e->get_id() > r->get_id()) { + std::swap(e, r); + } + return m_table.contains(std::make_pair(e, r)); +} + void theory_seq::exclusion_table::update(expr* e, expr* r) { if (e->get_id() > r->get_id()) { std::swap(e, r); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 28a35c564..72363772b 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -81,9 +81,7 @@ namespace smt { ~exclusion_table() { } bool empty() const { return m_table.empty(); } void update(expr* e, expr* r); - bool contains(expr* e, expr* r) { - return m_table.contains(std::make_pair(e, r)); - } + bool contains(expr* e, expr* r) const; void push_scope() { m_limit.push_back(m_lhs.size()); } void pop_scope(unsigned num_scopes); void display(std::ostream& out) const; diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp index 3f5e7bdfe..b84ae68f0 100644 --- a/src/tactic/aig/aig.cpp +++ b/src/tactic/aig/aig.cpp @@ -131,7 +131,7 @@ struct aig_manager::imp { if (memory::get_allocation_size() > m_max_memory) throw aig_exception(TACTIC_MAX_MEMORY_MSG); if (m().canceled()) - throw aig_exception(TACTIC_CANCELED_MSG); + throw aig_exception(m().limit().get_cancel_msg()); cooperate("aig"); } diff --git a/src/tactic/arith/arith_bounds_tactic.cpp b/src/tactic/arith/arith_bounds_tactic.cpp index 1111d7f1f..fe054aaea 100644 --- a/src/tactic/arith/arith_bounds_tactic.cpp +++ b/src/tactic/arith/arith_bounds_tactic.cpp @@ -37,7 +37,7 @@ struct arith_bounds_tactic : public tactic { void checkpoint() { if (m.canceled()) { - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); } } diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp index f4455e672..6c5527d12 100644 --- a/src/tactic/arith/degree_shift_tactic.cpp +++ b/src/tactic/arith/degree_shift_tactic.cpp @@ -100,7 +100,7 @@ class degree_shift_tactic : public tactic { void checkpoint() { if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); cooperate("degree_shift"); } diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp index 5cc021f6f..410185cf8 100644 --- a/src/tactic/arith/diff_neq_tactic.cpp +++ b/src/tactic/arith/diff_neq_tactic.cpp @@ -289,7 +289,7 @@ class diff_neq_tactic : public tactic { unsigned nvars = num_vars(); while (m_stack.size() < nvars) { if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); TRACE("diff_neq_tactic", display_model(tout);); var x = m_stack.size(); if (extend_model(x)) diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp index 4674459dd..698128e26 100644 --- a/src/tactic/arith/fm_tactic.cpp +++ b/src/tactic/arith/fm_tactic.cpp @@ -197,7 +197,7 @@ class fm_tactic : public tactic { clauses::iterator it = m_clauses[i].begin(); clauses::iterator end = m_clauses[i].end(); for (; it != end; ++it) { - if (m.canceled()) throw tactic_exception(TACTIC_CANCELED_MSG); + if (m.canceled()) throw tactic_exception(m.limit().get_cancel_msg()); switch (process(x, *it, u, ev, val)) { case NONE: TRACE("fm_mc", tout << "no bound for:\n" << mk_ismt2_pp(*it, m) << "\n";); @@ -1543,7 +1543,7 @@ class fm_tactic : public tactic { void checkpoint() { cooperate("fm"); if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); } diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index 8c93aeb90..25127cb90 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -176,7 +176,7 @@ struct bv_size_reduction_tactic::imp { void checkpoint() { if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); } void operator()(goal & g, model_converter_ref & mc) { diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp index 50063b8a5..42ceaf78c 100644 --- a/src/tactic/bv/bvarray2uf_tactic.cpp +++ b/src/tactic/bv/bvarray2uf_tactic.cpp @@ -50,7 +50,7 @@ class bvarray2uf_tactic : public tactic { void checkpoint() { if (m_manager.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m_manager.limit().get_cancel_msg()); } void operator()(goal_ref const & g, diff --git a/src/tactic/core/cofactor_elim_term_ite.cpp b/src/tactic/core/cofactor_elim_term_ite.cpp index 43e3559ba..15f0e06ea 100644 --- a/src/tactic/core/cofactor_elim_term_ite.cpp +++ b/src/tactic/core/cofactor_elim_term_ite.cpp @@ -36,7 +36,7 @@ struct cofactor_elim_term_ite::imp { if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); } // Collect atoms that contain term if-then-else diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index 987d5a48d..1cfaa78cf 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -96,7 +96,7 @@ struct ctx_simplify_tactic::imp { if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); } bool shared(expr * t) const { diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index 121dbeef3..cf83a5a10 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -94,7 +94,7 @@ struct reduce_args_tactic::imp { void checkpoint() { if (m_manager.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m_manager.limit().get_cancel_msg()); cooperate("reduce-args"); } diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index 01c4bc10b..f1ffe4b53 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -77,8 +77,8 @@ class solve_eqs_tactic : public tactic { void checkpoint() { if (m().canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); - cooperate("solve-eqs"); + throw tactic_exception(m().limit().get_cancel_msg()); + cooperate("solve-eqs"); } // Check if the number of occurrences of t is below the specified threshold :solve-eqs-max-occs diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp index d0798e375..4418808dd 100644 --- a/src/tactic/sls/sls_engine.cpp +++ b/src/tactic/sls/sls_engine.cpp @@ -95,7 +95,7 @@ void sls_engine::collect_statistics(statistics& st) const { void sls_engine::checkpoint() { if (m_manager.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m_manager.limit().get_cancel_msg()); cooperate("sls"); } diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp index 5a5cba1f0..d1320bc0d 100644 --- a/src/tactic/ufbv/quasi_macros_tactic.cpp +++ b/src/tactic/ufbv/quasi_macros_tactic.cpp @@ -77,8 +77,8 @@ class quasi_macros_tactic : public tactic { while (more) { // CMW: use repeat(...) ? if (m().canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); - + throw tactic_exception(m().limit().get_cancel_msg()); + new_forms.reset(); new_proofs.reset(); more = qm(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs);