mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Fix incorrect uses of set_cancel()
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
f8014f54c1
commit
607fab486c
|
@ -55,6 +55,7 @@ namespace api {
|
|||
std::string get_last_status();
|
||||
std::string to_string(unsigned num_queries, expr*const* queries);
|
||||
void cancel() { m_context.cancel(); }
|
||||
void reset_cancel() { m_context.reset_cancel(); }
|
||||
|
||||
unsigned get_num_levels(func_decl* pred);
|
||||
expr_ref get_cover_delta(int level, func_decl* pred);
|
||||
|
|
|
@ -1404,6 +1404,8 @@ public:
|
|||
|
||||
// propagate cancellation signal to decl_plugins
|
||||
void set_cancel(bool f);
|
||||
void cancel() { set_cancel(true); }
|
||||
void reset_cancel() { set_cancel(false); }
|
||||
|
||||
bool has_trace_stream() const { return m_trace_stream != 0; }
|
||||
std::ostream & trace_stream() { SASSERT(has_trace_stream()); return *m_trace_stream; }
|
||||
|
|
|
@ -343,6 +343,13 @@ cmd_context::~cmd_context() {
|
|||
m_check_sat_result = 0;
|
||||
}
|
||||
|
||||
void cmd_context::set_cancel(bool f) {
|
||||
if (m_solver)
|
||||
m_solver->set_cancel(f);
|
||||
if (has_manager())
|
||||
m().set_cancel(f);
|
||||
}
|
||||
|
||||
void cmd_context::global_params_updated() {
|
||||
m_params.updt_params();
|
||||
if (m_solver) {
|
||||
|
|
|
@ -249,6 +249,9 @@ protected:
|
|||
public:
|
||||
cmd_context(bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
|
||||
~cmd_context();
|
||||
void set_cancel(bool f);
|
||||
void cancel() { set_cancel(true); }
|
||||
void reset_cancel() { set_cancel(false); }
|
||||
context_params & params() { return m_params; }
|
||||
void global_params_updated(); // this method should be invoked when global (and module) params are updated.
|
||||
void set_logic(symbol const & s);
|
||||
|
|
|
@ -2796,72 +2796,58 @@ namespace algebraic_numbers {
|
|||
}
|
||||
|
||||
void manager::del(numeral & a) {
|
||||
set_cancel(false);
|
||||
return m_imp->del(a);
|
||||
}
|
||||
|
||||
void manager::reset(numeral & a) {
|
||||
set_cancel(false);
|
||||
return m_imp->reset(a);
|
||||
}
|
||||
|
||||
bool manager::is_zero(numeral const & a) {
|
||||
set_cancel(false);
|
||||
return m_imp->is_zero(const_cast<numeral&>(a));
|
||||
}
|
||||
|
||||
bool manager::is_pos(numeral const & a) {
|
||||
set_cancel(false);
|
||||
return m_imp->is_pos(const_cast<numeral&>(a));
|
||||
}
|
||||
|
||||
bool manager::is_neg(numeral const & a) {
|
||||
set_cancel(false);
|
||||
return m_imp->is_neg(const_cast<numeral&>(a));
|
||||
}
|
||||
|
||||
bool manager::is_rational(numeral const & a) {
|
||||
set_cancel(false);
|
||||
return m_imp->is_rational(const_cast<numeral&>(a));
|
||||
}
|
||||
|
||||
bool manager::is_int(numeral const & a) {
|
||||
set_cancel(false);
|
||||
return m_imp->is_int(const_cast<numeral&>(a));
|
||||
}
|
||||
|
||||
unsigned manager::degree(numeral const & a) {
|
||||
set_cancel(false);
|
||||
return m_imp->degree(const_cast<numeral&>(a));
|
||||
}
|
||||
|
||||
void manager::to_rational(numeral const & a, mpq & r) {
|
||||
set_cancel(false);
|
||||
return m_imp->to_rational(const_cast<numeral&>(a), r);
|
||||
}
|
||||
|
||||
void manager::to_rational(numeral const & a, rational & r) {
|
||||
set_cancel(false);
|
||||
return m_imp->to_rational(const_cast<numeral&>(a), r);
|
||||
}
|
||||
|
||||
void manager::swap(numeral & a, numeral & b) {
|
||||
set_cancel(false);
|
||||
return m_imp->swap(a, b);
|
||||
}
|
||||
|
||||
void manager::int_lt(numeral const & a, numeral & b) {
|
||||
set_cancel(false);
|
||||
m_imp->int_lt(const_cast<numeral&>(a), b);
|
||||
}
|
||||
|
||||
void manager::int_gt(numeral const & a, numeral & b) {
|
||||
set_cancel(false);
|
||||
m_imp->int_gt(const_cast<numeral&>(a), b);
|
||||
}
|
||||
|
||||
void manager::select(numeral const & prev, numeral const & curr, numeral & result) {
|
||||
set_cancel(false);
|
||||
m_imp->select(const_cast<numeral&>(prev), const_cast<numeral&>(curr), result);
|
||||
}
|
||||
|
||||
|
@ -2878,55 +2864,45 @@ namespace algebraic_numbers {
|
|||
}
|
||||
|
||||
void manager::set(numeral & a, mpq const & n) {
|
||||
set_cancel(false);
|
||||
m_imp->set(a, n);
|
||||
}
|
||||
|
||||
void manager::set(numeral & a, numeral const & n) {
|
||||
set_cancel(false);
|
||||
m_imp->set(a, n);
|
||||
}
|
||||
|
||||
void manager::isolate_roots(polynomial_ref const & p, numeral_vector & roots) {
|
||||
set_cancel(false);
|
||||
m_imp->isolate_roots(p, roots);
|
||||
}
|
||||
|
||||
void manager::isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots) {
|
||||
set_cancel(false);
|
||||
m_imp->isolate_roots(p, x2v, roots);
|
||||
}
|
||||
|
||||
void manager::isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector<int> & signs) {
|
||||
set_cancel(false);
|
||||
m_imp->isolate_roots(p, x2v, roots, signs);
|
||||
}
|
||||
|
||||
void manager::mk_root(polynomial_ref const & p, unsigned i, numeral & r) {
|
||||
set_cancel(false);
|
||||
m_imp->mk_root(p, i, r);
|
||||
}
|
||||
|
||||
void manager::mk_root(sexpr const * p, unsigned i, numeral & r) {
|
||||
set_cancel(false);
|
||||
m_imp->mk_root(p, i, r);
|
||||
}
|
||||
|
||||
void manager::root(numeral const & a, unsigned k, numeral & b) {
|
||||
set_cancel(false);
|
||||
m_imp->root(const_cast<numeral&>(a), k, b);
|
||||
}
|
||||
|
||||
void manager::power(numeral const & a, unsigned k, numeral & b) {
|
||||
TRACE("anum_detail", display_root(tout, a); tout << "^" << k << "\n";);
|
||||
set_cancel(false);
|
||||
m_imp->power(const_cast<numeral&>(a), k, b);
|
||||
TRACE("anum_detail", tout << "^ result: "; display_root(tout, b); tout << "\n";);
|
||||
}
|
||||
|
||||
void manager::add(numeral const & a, numeral const & b, numeral & c) {
|
||||
TRACE("anum_detail", display_root(tout, a); tout << " + "; display_root(tout, b); tout << "\n";);
|
||||
set_cancel(false);
|
||||
m_imp->add(const_cast<numeral&>(a), const_cast<numeral&>(b), c);
|
||||
TRACE("anum_detail", tout << "+ result: "; display_root(tout, c); tout << "\n";);
|
||||
}
|
||||
|
@ -2939,45 +2915,37 @@ namespace algebraic_numbers {
|
|||
|
||||
void manager::sub(numeral const & a, numeral const & b, numeral & c) {
|
||||
TRACE("anum_detail", display_root(tout, a); tout << " - "; display_root(tout, b); tout << "\n";);
|
||||
set_cancel(false);
|
||||
m_imp->sub(const_cast<numeral&>(a), const_cast<numeral&>(b), c);
|
||||
TRACE("anum_detail", tout << "- result: "; display_root(tout, c); tout << "\n";);
|
||||
}
|
||||
|
||||
void manager::mul(numeral const & a, numeral const & b, numeral & c) {
|
||||
TRACE("anum_detail", display_root(tout, a); tout << " * "; display_root(tout, b); tout << "\n";);
|
||||
set_cancel(false);
|
||||
m_imp->mul(const_cast<numeral&>(a), const_cast<numeral&>(b), c);
|
||||
TRACE("anum_detail", tout << "* result: "; display_root(tout, c); tout << "\n";);
|
||||
}
|
||||
|
||||
void manager::div(numeral const & a, numeral const & b, numeral & c) {
|
||||
set_cancel(false);
|
||||
m_imp->div(const_cast<numeral&>(a), const_cast<numeral&>(b), c);
|
||||
}
|
||||
|
||||
void manager::neg(numeral & a) {
|
||||
set_cancel(false);
|
||||
m_imp->neg(a);
|
||||
}
|
||||
|
||||
void manager::inv(numeral & a) {
|
||||
set_cancel(false);
|
||||
m_imp->inv(a);
|
||||
}
|
||||
|
||||
int manager::compare(numeral const & a, numeral const & b) {
|
||||
set_cancel(false);
|
||||
return m_imp->compare(const_cast<numeral&>(a), const_cast<numeral&>(b));
|
||||
}
|
||||
|
||||
bool manager::eq(numeral const & a, numeral const & b) {
|
||||
set_cancel(false);
|
||||
return m_imp->eq(const_cast<numeral&>(a), const_cast<numeral&>(b));
|
||||
}
|
||||
|
||||
bool manager::eq(numeral const & a, mpq const & b) {
|
||||
set_cancel(false);
|
||||
return m_imp->eq(const_cast<numeral&>(a), b);
|
||||
}
|
||||
|
||||
|
@ -2988,12 +2956,10 @@ namespace algebraic_numbers {
|
|||
}
|
||||
|
||||
bool manager::lt(numeral const & a, numeral const & b) {
|
||||
set_cancel(false);
|
||||
return m_imp->lt(const_cast<numeral&>(a), const_cast<numeral&>(b));
|
||||
}
|
||||
|
||||
bool manager::lt(numeral const & a, mpq const & b) {
|
||||
set_cancel(false);
|
||||
return m_imp->lt(const_cast<numeral&>(a), b);
|
||||
}
|
||||
|
||||
|
@ -3004,7 +2970,6 @@ namespace algebraic_numbers {
|
|||
}
|
||||
|
||||
bool manager::gt(numeral const & a, mpq const & b) {
|
||||
set_cancel(false);
|
||||
return m_imp->gt(const_cast<numeral&>(a), b);
|
||||
}
|
||||
|
||||
|
@ -3073,38 +3038,31 @@ namespace algebraic_numbers {
|
|||
}
|
||||
|
||||
int manager::eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v) {
|
||||
set_cancel(false);
|
||||
SASSERT(&(x2v.m()) == this);
|
||||
return m_imp->eval_sign_at(p, x2v);
|
||||
}
|
||||
|
||||
void manager::display_interval(std::ostream & out, numeral const & a) const {
|
||||
const_cast<manager*>(this)->set_cancel(false);
|
||||
m_imp->display_interval(out, a);
|
||||
}
|
||||
|
||||
void manager::display_decimal(std::ostream & out, numeral const & a, unsigned precision) const {
|
||||
const_cast<manager*>(this)->set_cancel(false);
|
||||
m_imp->display_decimal(out, a, precision);
|
||||
}
|
||||
|
||||
void manager::display_root(std::ostream & out, numeral const & a) const {
|
||||
const_cast<manager*>(this)->set_cancel(false);
|
||||
m_imp->display_root(out, a);
|
||||
}
|
||||
|
||||
void manager::display_mathematica(std::ostream & out, numeral const & a) const {
|
||||
const_cast<manager*>(this)->set_cancel(false);
|
||||
m_imp->display_mathematica(out, a);
|
||||
}
|
||||
|
||||
void manager::display_root_smt2(std::ostream & out, numeral const & a) const {
|
||||
const_cast<manager*>(this)->set_cancel(false);
|
||||
m_imp->display_root_smt2(out, a);
|
||||
}
|
||||
|
||||
void manager::reset_statistics() {
|
||||
set_cancel(false);
|
||||
m_imp->reset_statistics();
|
||||
}
|
||||
|
||||
|
|
|
@ -64,8 +64,8 @@ namespace algebraic_numbers {
|
|||
static void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
|
||||
|
||||
void set_cancel(bool f);
|
||||
|
||||
void cancel() { set_cancel(true); }
|
||||
void reset_cancel() { set_cancel(false); }
|
||||
|
||||
void updt_params(params_ref const & p);
|
||||
|
||||
|
|
|
@ -2368,7 +2368,6 @@ namespace polynomial {
|
|||
|
||||
void checkpoint() {
|
||||
if (m_cancel) {
|
||||
set_cancel(false);
|
||||
throw polynomial_exception("canceled");
|
||||
}
|
||||
cooperate("polynomial");
|
||||
|
|
|
@ -220,6 +220,7 @@ namespace polynomial {
|
|||
|
||||
void set_cancel(bool f);
|
||||
void cancel() { set_cancel(true); }
|
||||
void reset_cancel() { set_cancel(false); }
|
||||
|
||||
/**
|
||||
\brief Abstract event handler.
|
||||
|
|
|
@ -244,10 +244,10 @@ unsigned model_evaluator::get_num_steps() const {
|
|||
return m_imp->get_num_steps();
|
||||
}
|
||||
|
||||
void model_evaluator::cancel() {
|
||||
void model_evaluator::set_cancel(bool f) {
|
||||
#pragma omp critical (model_evaluator)
|
||||
{
|
||||
m_imp->cancel();
|
||||
m_imp->set_cancel(f);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -41,7 +41,9 @@ public:
|
|||
|
||||
void operator()(expr * t, expr_ref & r);
|
||||
|
||||
void cancel();
|
||||
void set_cancel(bool f);
|
||||
void cancel() { set_cancel(true); }
|
||||
void reset_cancel() { set_cancel(false); }
|
||||
void cleanup(params_ref const & p = params_ref());
|
||||
void reset(params_ref const & p = params_ref());
|
||||
|
||||
|
|
|
@ -349,6 +349,7 @@ namespace datalog {
|
|||
void cancel();
|
||||
|
||||
void cleanup();
|
||||
void reset_cancel() { cleanup(); }
|
||||
|
||||
/**
|
||||
\brief check if query 'q' is satisfied under asserted rules and background.
|
||||
|
|
|
@ -390,6 +390,7 @@ namespace smt2 {
|
|||
void check_float(char const * msg) { if (!curr_is_float()) throw parser_exception(msg); }
|
||||
|
||||
void error(unsigned line, unsigned pos, char const * msg) {
|
||||
m_ctx.reset_cancel();
|
||||
if (use_vs_format()) {
|
||||
m_ctx.diagnostic_stream() << "Z3(" << line << ", " << pos << "): ERROR: " << msg;
|
||||
if (msg[strlen(msg)-1] != '\n')
|
||||
|
|
|
@ -253,12 +253,10 @@ namespace smt {
|
|||
}
|
||||
|
||||
lbool kernel::setup_and_check() {
|
||||
set_cancel(false);
|
||||
return m_imp->setup_and_check();
|
||||
}
|
||||
|
||||
lbool kernel::check(unsigned num_assumptions, expr * const * assumptions) {
|
||||
set_cancel(false);
|
||||
lbool r = m_imp->check(num_assumptions, assumptions);
|
||||
TRACE("smt_kernel", tout << "check result: " << r << "\n";);
|
||||
return r;
|
||||
|
|
|
@ -175,7 +175,6 @@ tactic * mk_fail_if_undecided_tactic() {
|
|||
|
||||
void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) {
|
||||
t.reset_statistics();
|
||||
t.reset_cancel();
|
||||
try {
|
||||
t(in, result, mc, pc, core);
|
||||
t.cleanup();
|
||||
|
|
|
@ -116,7 +116,6 @@ protected:
|
|||
m_t2->set_cancel(f);
|
||||
}
|
||||
|
||||
|
||||
template<typename T>
|
||||
tactic * translate_core(ast_manager & m) {
|
||||
tactic * new_t1 = m_t1->translate(m);
|
||||
|
|
|
@ -29,6 +29,7 @@ class cancel_eh : public event_handler {
|
|||
T & m_obj;
|
||||
public:
|
||||
cancel_eh(T & o):m_obj(o) {}
|
||||
~cancel_eh() { m_obj.reset_cancel(); }
|
||||
virtual void operator()() {
|
||||
m_obj.cancel();
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue