mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 04:43:39 +00:00
Code Activity

Fix set_interruptable usage

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-03-25 16:52:08 -07:00
parent 7e9715f3e6
commit b417ca657d
7 changed files with 10 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/api_algebraic.cpp
View file

@ -373,7 +373,7 @@ extern "C" {
scoped_anum_vector roots(_am); scoped_anum_vector roots(_am);
{ {
cancel_eh<algebraic_numbers::manager> eh(_am); cancel_eh<algebraic_numbers::manager> eh(_am);
api::context::set_interruptable(*(mk_c(c)), eh); api::context::set_interruptable si(*(mk_c(c)), eh);
scoped_timer timer(mk_c(c)->params().m_timeout, &eh); scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
vector_var2anum v2a(as); vector_var2anum v2a(as);
_am.isolate_roots(_p, v2a, roots); _am.isolate_roots(_p, v2a, roots);
@ -408,7 +408,7 @@ extern "C" {
} }
{ {
cancel_eh<algebraic_numbers::manager> eh(_am); cancel_eh<algebraic_numbers::manager> eh(_am);
api::context::set_interruptable(*(mk_c(c)), eh); api::context::set_interruptable si(*(mk_c(c)), eh);
scoped_timer timer(mk_c(c)->params().m_timeout, &eh); scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
vector_var2anum v2a(as); vector_var2anum v2a(as);
int r = _am.eval_sign_at(_p, v2a); int r = _am.eval_sign_at(_p, v2a);

2
src/api/api_ast.cpp
View file

@ -681,7 +681,7 @@ extern "C" {
th_rewriter m_rw(m, p); th_rewriter m_rw(m, p);
expr_ref result(m); expr_ref result(m);
cancel_eh<th_rewriter> eh(m_rw); cancel_eh<th_rewriter> eh(m_rw);
api::context::set_interruptable(*(mk_c(c)), eh); api::context::set_interruptable si(*(mk_c(c)), eh);
{ {
scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
scoped_timer timer(timeout, &eh); scoped_timer timer(timeout, &eh);

4
src/api/api_datalog.cpp
View file

@ -266,7 +266,7 @@ extern "C" {
lbool r = l_undef; lbool r = l_undef;
cancel_eh<api::fixedpoint_context> eh(*to_fixedpoint_ref(d)); 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 timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
api::context::set_interruptable(*(mk_c(c)), eh); api::context::set_interruptable si(*(mk_c(c)), eh);
{ {
scoped_timer timer(timeout, &eh); scoped_timer timer(timeout, &eh);
try { try {
@ -291,7 +291,7 @@ extern "C" {
lbool r = l_undef; lbool r = l_undef;
unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); 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<api::fixedpoint_context> eh(*to_fixedpoint_ref(d));
api::context::set_interruptable(*(mk_c(c)), eh); api::context::set_interruptable si(*(mk_c(c)), eh);
{ {
scoped_timer timer(timeout, &eh); scoped_timer timer(timeout, &eh);
try { try {

2
src/api/api_polynomial.cpp
View file

@ -67,7 +67,7 @@ extern "C" {
expr_ref _r(mk_c(c)->m()); expr_ref _r(mk_c(c)->m());
{ {
cancel_eh<polynomial::manager> eh(pm); cancel_eh<polynomial::manager> eh(pm);
api::context::set_interruptable(*(mk_c(c)), eh); api::context::set_interruptable si(*(mk_c(c)), eh);
scoped_timer timer(mk_c(c)->params().m_timeout, &eh); scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
pm.psc_chain(_p, _q, v_x, rs); pm.psc_chain(_p, _q, v_x, rs);
} }

2
src/api/api_solver.cpp
View file

@ -243,7 +243,7 @@ extern "C" {
unsigned timeout = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); unsigned timeout = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", false); bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", false);
cancel_eh<solver> eh(*to_solver_ref(s)); cancel_eh<solver> eh(*to_solver_ref(s));
api::context::set_interruptable(*(mk_c(c)), eh); api::context::set_interruptable si(*(mk_c(c)), eh);
lbool result; lbool result;
{ {
scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);

4
src/api/api_solver_old.cpp
View file

@ -73,7 +73,7 @@ extern "C" {
RESET_ERROR_CODE(); RESET_ERROR_CODE();
CHECK_SEARCHING(c); CHECK_SEARCHING(c);
cancel_eh<smt::kernel> eh(mk_c(c)->get_smt_kernel()); cancel_eh<smt::kernel> eh(mk_c(c)->get_smt_kernel());
api::context::set_interruptable(*(mk_c(c)), eh); api::context::set_interruptable si(*(mk_c(c)), eh);
flet<bool> _model(mk_c(c)->fparams().m_model, true); flet<bool> _model(mk_c(c)->fparams().m_model, true);
lbool result; lbool result;
try { try {
@ -123,7 +123,7 @@ extern "C" {
expr * const* _assumptions = to_exprs(assumptions); expr * const* _assumptions = to_exprs(assumptions);
flet<bool> _model(mk_c(c)->fparams().m_model, true); flet<bool> _model(mk_c(c)->fparams().m_model, true);
cancel_eh<smt::kernel> eh(mk_c(c)->get_smt_kernel()); cancel_eh<smt::kernel> eh(mk_c(c)->get_smt_kernel());
api::context::set_interruptable(*(mk_c(c)), eh); api::context::set_interruptable si(*(mk_c(c)), eh);
lbool result; lbool result;
result = mk_c(c)->get_smt_kernel().check(num_assumptions, _assumptions); result = mk_c(c)->get_smt_kernel().check(num_assumptions, _assumptions);
if (result != l_false && m) { if (result != l_false && m) {

2
src/api/api_tactic.cpp
View file

@ -410,7 +410,7 @@ extern "C" {
to_tactic_ref(t)->updt_params(p); to_tactic_ref(t)->updt_params(p);
api::context::set_interruptable(*(mk_c(c)), eh); api::context::set_interruptable si(*(mk_c(c)), eh);
{ {
scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
scoped_timer timer(timeout, &eh); scoped_timer timer(timeout, &eh);