mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

cleanup cancelation logic

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-11 12:35:35 -08:00 • committed by Christoph M. Wintersteiger
parent 325d516825
commit f2f9578c0a
37 changed files with 93 additions and 198 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/api/api_datalog.cpp
View file

@ -130,12 +130,6 @@ namespace api {
m_context.display_smt2(num_queries, queries, str);
return str.str();
}
void cancel() {
m_context.cancel();
}
void reset_cancel() {
m_context.reset_cancel();
}
unsigned get_num_levels(func_decl* pred) {
return m_context.get_num_levels(pred);
}
@ -285,13 +279,13 @@ extern "C" {
LOG_Z3_fixedpoint_query(c, d, q);
RESET_ERROR_CODE();
lbool r = l_undef;
cancel_eh<api::fixedpoint_context> eh(*to_fixedpoint_ref(d));
unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
unsigned rlimit = to_fixedpoint(d)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
api::context::set_interruptable si(*(mk_c(c)), eh);
{
scoped_timer timer(timeout, &eh);
scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
cancel_eh<reslimit> eh(mk_c(c)->m().limit());
api::context::set_interruptable si(*(mk_c(c)), eh);
scoped_timer timer(timeout, &eh);
try {
r = to_fixedpoint_ref(d)->ctx().query(to_expr(q));
}
@ -313,7 +307,7 @@ extern "C" {
RESET_ERROR_CODE();
lbool r = l_undef;
unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
cancel_eh<api::fixedpoint_context> eh(*to_fixedpoint_ref(d));
cancel_eh<reslimit> eh(mk_c(c)->m().limit());
api::context::set_interruptable si(*(mk_c(c)), eh);
{
scoped_timer timer(timeout, &eh);