mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

Check more frequently for cancelation flags to address grep0095.stp.smt2 in issue #178. Z3 spends time in pre-processing simplification, which indicates there is some opportunity to tune this portion of the code

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-08-11 23:14:34 +02:00
parent 424f34d3d9
commit 702af71a2d
2 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_context.cpp
View file

@ -2773,6 +2773,7 @@ namespace smt {
} }
void context::assert_expr_core(expr * e, proof * pr) { void context::assert_expr_core(expr * e, proof * pr) {
if (m_cancel_flag) return;
SASSERT(is_well_sorted(m_manager, e)); SASSERT(is_well_sorted(m_manager, e));
TRACE("begin_assert_expr", tout << mk_pp(e, m_manager) << "\n";); TRACE("begin_assert_expr", tout << mk_pp(e, m_manager) << "\n";);
TRACE("begin_assert_expr_ll", tout << mk_ll_pp(e, m_manager) << "\n";); TRACE("begin_assert_expr_ll", tout << mk_ll_pp(e, m_manager) << "\n";);
@ -2802,6 +2803,7 @@ namespace smt {
} }
void context::internalize_assertions() { void context::internalize_assertions() {
if (m_cancel_flag) return;
TRACE("internalize_assertions", tout << "internalize_assertions()...\n";); TRACE("internalize_assertions", tout << "internalize_assertions()...\n";);
timeit tt(get_verbosity_level() >= 100, "smt.preprocessing"); timeit tt(get_verbosity_level() >= 100, "smt.preprocessing");
reduce_assertions(); reduce_assertions();

3
src/smt/tactic/smt_tactic.cpp
View file

@ -229,6 +229,9 @@ public:
m_ctx->assert_expr(in->form(i)); m_ctx->assert_expr(in->form(i));
} }
} }
if (m_ctx->canceled()) {
throw tactic_exception("smt_tactic canceled");
}
lbool r; lbool r;
if (assumptions.empty()) if (assumptions.empty())