mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

reworking cancellation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-11 16:21:24 -08:00
parent 981f8226fe
commit baee4225a7
145 changed files with 172 additions and 958 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/math/interval/interval.h
View file

@ -21,6 +21,7 @@ Revision History:
#include"mpq.h"
#include"ext_numeral.h"
#include"rlimit.h"
/**
\brief Default configuration for interval manager.
@ -110,6 +111,7 @@ public:
typedef typename numeral_manager::numeral numeral;
typedef typename C::interval interval;
private:
reslimit& m_limit;
C m_c;
numeral m_result_lower;
numeral m_result_upper;
@ -127,7 +129,6 @@ private:
interval m_3_pi_div_2;
interval m_2_pi;
volatile bool m_cancel;
void round_to_minus_inf() { m_c.round_to_minus_inf(); }
void round_to_plus_inf() { m_c.round_to_plus_inf(); }
@ -161,11 +162,9 @@ private:
void checkpoint();
public:
interval_manager(C const & c);
interval_manager(reslimit& lim, C const & c);
~interval_manager();
void set_cancel(bool f) { m_cancel = f; }
numeral_manager & m() const { return m_c.m(); }
void del(interval & a);

5
src/math/interval/interval_def.h
View file

@ -30,11 +30,10 @@ Revision History:
// #define TRACE_NTH_ROOT
template<typename C>
interval_manager<C>::interval_manager(C const & c):m_c(c) {
interval_manager<C>::interval_manager(reslimit& lim, C const & c): m_limit(lim), m_c(c) {
m().set(m_minus_one, -1);
m().set(m_one, 1);
m_pi_n = 0;
m_cancel = false;
}
template<typename C>
@ -63,7 +62,7 @@ void interval_manager<C>::del(interval & a) {
template<typename C>
void interval_manager<C>::checkpoint() {
if (m_cancel)
if (m_limit.canceled())
throw default_exception("canceled");
cooperate("interval");
}

18
src/math/polynomial/algebraic_numbers.cpp
View file

@ -83,7 +83,6 @@ namespace algebraic_numbers {
scoped_upoly m_add_tmp;
polynomial::var m_x;
polynomial::var m_y;
volatile bool m_cancel;
// configuration
int m_min_magnitude;
@ -104,8 +103,8 @@ namespace algebraic_numbers {
m_qmanager(m),
m_bqmanager(m),
m_bqimanager(m_bqmanager),
m_pmanager(m, &a),
m_upmanager(m),
m_pmanager(lim, m, &a),
m_upmanager(lim, m),
m_is_rational_tmp(m),
m_isolate_tmp1(upm()),
m_isolate_tmp2(upm()),
@ -118,7 +117,6 @@ namespace algebraic_numbers {
m_add_tmp(upm()) {
updt_params(p);
reset_statistics();
m_cancel = false;
m_x = pm().mk_var();
m_y = pm().mk_var();
}
@ -126,14 +124,8 @@ namespace algebraic_numbers {
~imp() {
}
void set_cancel(bool f) {
m_cancel = f;
pm().set_cancel(f);
upm().set_cancel(f);
}
void checkpoint() {
if (m_cancel)
if (!m_limit.inc())
throw algebraic_exception("canceled");
cooperate("algebraic");
}
@ -2785,10 +2777,6 @@ namespace algebraic_numbers {
void manager::updt_params(params_ref const & p) {
}
void manager::set_cancel(bool f) {
m_imp->set_cancel(f);
}
unsynch_mpq_manager & manager::qm() const {
return m_imp->qm();
}

4
src/math/polynomial/algebraic_numbers.h
View file

@ -64,10 +64,6 @@ namespace algebraic_numbers {
static void get_param_descrs(param_descrs & r);
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);
unsynch_mpq_manager & qm() const;

32
src/math/polynomial/polynomial.cpp
View file

@ -1829,6 +1829,7 @@ namespace polynomial {
typedef _scoped_numeral<numeral_manager> scoped_numeral;
typedef _scoped_numeral_vector<numeral_manager> scoped_numeral_vector;
reslimit& m_limit;
manager & m_wrapper;
numeral_manager m_manager;
up_manager m_upm;
@ -1847,7 +1848,6 @@ namespace polynomial {
unsigned_vector m_degree2pos;
bool m_use_sparse_gcd;
bool m_use_prs_gcd;
volatile bool m_cancel;
// Debugging method: check if the coefficients of p are in the numeral_manager.
bool consistent_coeffs(polynomial const * p) {
@ -2323,13 +2323,13 @@ namespace polynomial {
inc_ref(m_unit_poly);
m_use_sparse_gcd = true;
m_use_prs_gcd = false;
m_cancel = false;
}
imp(manager & w, unsynch_mpz_manager & m, monomial_manager * mm):
imp(reslimit& lim, manager & w, unsynch_mpz_manager & m, monomial_manager * mm):
m_limit(lim),
m_wrapper(w),
m_manager(m),
m_upm(m) {
m_upm(lim, m) {
if (mm == 0)
mm = alloc(monomial_manager);
m_monomial_manager = mm;
@ -2337,10 +2337,11 @@ namespace polynomial {
init();
}
imp(manager & w, unsynch_mpz_manager & m, small_object_allocator * a):
imp(reslimit& lim, manager & w, unsynch_mpz_manager & m, small_object_allocator * a):
m_limit(lim),
m_wrapper(w),
m_manager(m),
m_upm(m) {
m_upm(lim, m) {
m_monomial_manager = alloc(monomial_manager, a);
m_monomial_manager->inc_ref();
init();
@ -2371,13 +2372,8 @@ namespace polynomial {
m_monomial_manager->dec_ref();
}
void set_cancel(bool f) {
m_cancel = f;
m_upm.set_cancel(f);
}
void checkpoint() {
if (m_cancel) {
if (!m_limit.inc()) {
throw polynomial_exception("canceled");
}
cooperate("polynomial");
@ -6883,12 +6879,12 @@ namespace polynomial {
}
};
manager::manager(numeral_manager & m, monomial_manager * mm) {
m_imp = alloc(imp, *this, m, mm);
manager::manager(reslimit& lim, numeral_manager & m, monomial_manager * mm) {
m_imp = alloc(imp, lim, *this, m, mm);
}
manager::manager(numeral_manager & m, small_object_allocator * a) {
m_imp = alloc(imp, *this, m, a);
manager::manager(reslimit& lim, numeral_manager & m, small_object_allocator * a) {
m_imp = alloc(imp, lim, *this, m, a);
}
manager::~manager() {
@ -6927,10 +6923,6 @@ namespace polynomial {
return m_imp->mm().allocator();
}
void manager::set_cancel(bool f) {
m_imp->set_cancel(f);
}
void manager::add_del_eh(del_eh * eh) {
m_imp->add_del_eh(eh);
}

9
src/math/polynomial/polynomial.h
View file

@ -28,6 +28,7 @@ Notes:
#include"scoped_numeral_vector.h"
#include"params.h"
#include"mpbqi.h"
#include"rlimit.h"
class small_object_allocator;
@ -190,8 +191,8 @@ namespace polynomial {
private:
imp * m_imp;
public:
manager(numeral_manager & m, monomial_manager * mm = 0);
manager(numeral_manager & m, small_object_allocator * a);
manager(reslimit& lim, numeral_manager & m, monomial_manager * mm = 0);
manager(reslimit& lim, numeral_manager & m, small_object_allocator * a);
~manager();
numeral_manager & m() const;
@ -218,10 +219,6 @@ namespace polynomial {
void set_zp(numeral const & p);
void set_zp(uint64 p);
void set_cancel(bool f);
void cancel() { set_cancel(true); }
void reset_cancel() { set_cancel(false); }
/**
\brief Abstract event handler.
*/

2
src/math/polynomial/rpolynomial.cpp
View file

@ -58,7 +58,6 @@ namespace rpolynomial {
numeral_manager & m_manager;
small_object_allocator * m_allocator;
bool m_own_allocator;
volatile bool m_cancel;
imp(manager & w, numeral_manager & m, small_object_allocator * a):
m_wrapper(w),
@ -67,7 +66,6 @@ namespace rpolynomial {
m_own_allocator(a == 0) {
if (a == 0)
m_allocator = alloc(small_object_allocator, "rpolynomial");
m_cancel = false;
}
~imp() {

2
src/math/polynomial/rpolynomial.h
View file

@ -57,8 +57,6 @@ namespace rpolynomial {
numeral_manager & m() const;
small_object_allocator & allocator() const;
void set_cancel(bool f);
/**
\brief Create a new variable.
*/

10
src/math/polynomial/upolynomial.cpp
View file

@ -134,9 +134,9 @@ namespace upolynomial {
std::swap(m_total_degree, other.m_total_degree);
}
core_manager::core_manager(unsynch_mpz_manager & m):
core_manager::core_manager(reslimit& lim, unsynch_mpz_manager & m):
m_limit(lim),
m_manager(m) {
m_cancel = false;
}
core_manager::~core_manager() {
@ -153,12 +153,8 @@ namespace upolynomial {
reset(m_pw_tmp);
}
void core_manager::set_cancel(bool f) {
m_cancel = f;
}
void core_manager::checkpoint() {
if (m_cancel)
if (!m_limit.inc())
throw upolynomial_exception("canceled");
cooperate("upolynomial");
}

10
src/math/polynomial/upolynomial.h
View file

@ -29,6 +29,7 @@ Notes:
#include"polynomial.h"
#include"z3_exception.h"
#include"mpbq.h"
#include"rlimit.h"
#define FACTOR_VERBOSE_LVL 1000
namespace upolynomial {
@ -101,6 +102,7 @@ namespace upolynomial {
};
protected:
reslimit& m_limit;
numeral_manager m_manager;
numeral_vector m_basic_tmp;
numeral_vector m_div_tmp1;
@ -114,7 +116,6 @@ namespace upolynomial {
numeral_vector m_sqf_tmp1;
numeral_vector m_sqf_tmp2;
numeral_vector m_pw_tmp;
volatile bool m_cancel;
static bool is_alias(numeral const * p, numeral_vector & buffer) { return buffer.c_ptr() != 0 && buffer.c_ptr() == p; }
void neg_core(unsigned sz1, numeral const * p1, numeral_vector & buffer);
@ -128,12 +129,12 @@ namespace upolynomial {
void CRA_combine_images(numeral_vector const & q, numeral const & p, numeral_vector & C, numeral & bound);
public:
core_manager(z_numeral_manager & m);
core_manager(reslimit& lim, z_numeral_manager & m);
~core_manager();
z_numeral_manager & zm() const { return m_manager.m(); }
numeral_manager & m() const { return const_cast<core_manager*>(this)->m_manager; }
reslimit& lim() const { return m_limit; }
/**
\brief Return true if Z_p[X]
*/
@ -156,7 +157,6 @@ namespace upolynomial {
void checkpoint();
void set_cancel(bool f);
/**
\brief set p size to 0. That is, p is the zero polynomial after this operation.
@ -576,7 +576,7 @@ namespace upolynomial {
bool factor_core(unsigned sz, numeral const * p, factors & r, factor_params const & params);
public:
manager(z_numeral_manager & m):core_manager(m) {}
manager(reslimit& lim, z_numeral_manager & m):core_manager(lim, m) {}
~manager();
void reset(numeral_vector & p) { core_manager::reset(p); }

12
src/math/polynomial/upolynomial_factorization.cpp
View file

@ -518,7 +518,7 @@ bool check_hansel_lift(z_manager & upm, numeral_vector const & C,
scoped_mpz br(nm);
nm.mul(b, r, br);
zp_manager br_upm(upm.zm());
zp_manager br_upm(upm.lim(), upm.zm());
br_upm.set_zp(br);
if (A_lifted.size() != A.size()) return false;
@ -543,7 +543,7 @@ bool check_hansel_lift(z_manager & upm, numeral_vector const & C,
return false;
}
zp_manager b_upm(nm);
zp_manager b_upm(upm.lim(), nm);
b_upm.set_zp(b);
// test2: A_lifted = A (mod b)
@ -596,7 +596,7 @@ void hensel_lift(z_manager & upm, numeral const & a, numeral const & b, numeral
tout << "C = "; upm.display(tout, C); tout << ")" << endl;
);
zp_manager r_upm(nm);
zp_manager r_upm(upm.lim(), nm);
r_upm.set_zp(r);
SASSERT(upm.degree(C) == upm.degree(A) + upm.degree(B));
@ -717,7 +717,7 @@ void hensel_lift_quadratic(z_manager& upm, numeral_vector const & C,
);
// we create a new Z_p manager, since we'll be changing the input one
zp_manager zp_upm(nm);
zp_manager zp_upm(upm.lim(), nm);
zp_upm.set_zp(zpe_upm.m().p());
// get the U, V, such that A*U + B*V = 1 (mod p)
@ -1055,7 +1055,7 @@ bool factor_square_free(z_manager & upm, numeral_vector const & f, factors & fs,
// the variables we'll be using and updating in Z_p
scoped_numeral p(nm);
nm.set(p, 2);
zp_manager zp_upm(nm.m());
zp_manager zp_upm(upm.lim(), nm.m());
zp_upm.set_zp(p);
zp_factors zp_fs(zp_upm);
scoped_numeral zp_fs_p(nm); nm.set(zp_fs_p, 2);
@ -1163,7 +1163,7 @@ bool factor_square_free(z_manager & upm, numeral_vector const & f, factors & fs,
);
// we got a prime factoring, so we do the lifting now
zp_manager zpe_upm(nm.m());
zp_manager zpe_upm(upm.lim(), nm.m());
zpe_upm.set_zp(zp_fs_p);
zp_numeral_manager & zpe_nm = zpe_upm.m();

19
src/math/realclosure/realclosure.cpp
View file

@ -369,6 +369,7 @@ namespace realclosure {
typedef sbuffer<int, REALCLOSURE_INI_BUFFER_SIZE> int_buffer;
typedef sbuffer<unsigned, REALCLOSURE_INI_BUFFER_SIZE> unsigned_buffer;
reslimit& m_limit;
small_object_allocator * m_allocator;
bool m_own_allocator;
unsynch_mpq_manager & m_qm;
@ -400,7 +401,6 @@ namespace realclosure {
bool m_in_aux_values; // True if we are computing SquareFree polynomials or Sturm sequences. That is, the values being computed will be discarded.
volatile bool m_cancel;
struct scoped_polynomial_seq {
typedef ref_buffer<value, imp, REALCLOSURE_INI_SEQ_SIZE> value_seq;
@ -494,7 +494,8 @@ namespace realclosure {
#define INC_DEPTH() ((void) 0)
#endif
imp(unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a):
imp(reslimit& lim, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a):
m_limit(lim),
m_allocator(a == 0 ? alloc(small_object_allocator, "realclosure") : a),
m_own_allocator(a == 0),
m_qm(qm),
@ -514,7 +515,6 @@ namespace realclosure {
m_in_aux_values = false;
m_cancel = false;
updt_params(p);
}
@ -547,7 +547,7 @@ namespace realclosure {
small_object_allocator & allocator() { return *m_allocator; }
void checkpoint() {
if (m_cancel)
if (!m_limit.inc())
throw exception("canceled");
cooperate("rcf");
}
@ -730,9 +730,6 @@ namespace realclosure {
return m_extensions[extension::ALGEBRAIC].size();
}
void set_cancel(bool f) {
m_cancel = f;
}
void updt_params(params_ref const & _p) {
rcf_params p(_p);
@ -6033,8 +6030,8 @@ namespace realclosure {
~save_interval_ctx() { m->restore_saved_intervals(); }
};
manager::manager(unsynch_mpq_manager & m, params_ref const & p, small_object_allocator * a) {
m_imp = alloc(imp, m, p, a);
manager::manager(reslimit& lim, unsynch_mpq_manager & m, params_ref const & p, small_object_allocator * a) {
m_imp = alloc(imp, lim, m, p, a);
}
manager::~manager() {
@ -6045,10 +6042,6 @@ namespace realclosure {
rcf_params::collect_param_descrs(r);
}
void manager::set_cancel(bool f) {
m_imp->set_cancel(f);
}
void manager::updt_params(params_ref const & p) {
m_imp->updt_params(p);
}

6
src/math/realclosure/realclosure.h
View file

@ -28,6 +28,7 @@ Notes:
#include"scoped_numeral_vector.h"
#include"interval.h"
#include"z3_exception.h"
#include"rlimit.h"
namespace realclosure {
class num;
@ -47,7 +48,7 @@ namespace realclosure {
friend class save_interval_ctx;
imp * m_imp;
public:
manager(unsynch_mpq_manager & m, params_ref const & p = params_ref(), small_object_allocator * a = 0);
manager(reslimit& lim, unsynch_mpq_manager & m, params_ref const & p = params_ref(), small_object_allocator * a = 0);
~manager();
typedef num numeral;
typedef svector<numeral> numeral_vector;
@ -57,9 +58,6 @@ namespace realclosure {
static void get_param_descrs(param_descrs & r);
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);

1
src/math/simplex/simplex.h
View file

@ -97,7 +97,6 @@ namespace simplex {
mutable eps_manager em;
mutable matrix M;
unsigned m_max_iterations;
volatile bool m_cancel;
var_heap m_to_patch;
vector<var_info> m_vars;
svector<var_t> m_row2base;

7
src/math/subpaving/subpaving_t.h
View file

@ -31,6 +31,7 @@ Revision History:
#include"statistics.h"
#include"lbool.h"
#include"id_gen.h"
#include"rlimit.h"
#ifdef _MSC_VER
#pragma warning(disable : 4200)
#pragma warning(disable : 4355)
@ -526,8 +527,6 @@ private:
numeral m_tmp1, m_tmp2, m_tmp3;
interval m_i_tmp1, m_i_tmp2, m_i_tmp3;
// Cancel flag
volatile bool m_cancel;
friend class node;
@ -759,7 +758,7 @@ private:
bool check_invariant() const;
public:
context_t(C const & c, params_ref const & p, small_object_allocator * a);
context_t(reslimit& lim, C const & c, params_ref const & p, small_object_allocator * a);
~context_t();
/**
@ -835,8 +834,6 @@ public:
void set_display_proc(display_var_proc * p) { m_display_proc = p; }
void set_cancel(bool f) { m_cancel = f; im().set_cancel(f); }
void updt_params(params_ref const & p);
static void collect_param_descrs(param_descrs & d);

3
src/math/subpaving/subpaving_t_def.h
View file

@ -431,7 +431,6 @@ context_t<C>::context_t(C const & c, params_ref const & p, small_object_allocato
m_node_selector = alloc(breadth_first_node_selector<C>, this);
m_var_selector = alloc(round_robing_var_selector<C>, this);
m_node_splitter = alloc(midpoint_node_splitter<C>, this);
m_cancel = false;
m_num_nodes = 0;
updt_params(p);
reset_statistics();
@ -459,7 +458,7 @@ context_t<C>::~context_t() {
template<typename C>
void context_t<C>::checkpoint() {
if (m_cancel)
if (m_limit.canceled())
throw default_exception("canceled");
if (memory::get_allocation_size() > m_max_memory)
throw default_exception(Z3_MAX_MEMORY_MSG);

10
src/math/subpaving/tactic/expr2subpaving.cpp
View file

@ -51,7 +51,6 @@ struct expr2subpaving::imp {
obj_map<expr, subpaving::ineq*> m_lit_cache;
volatile bool m_cancel;
imp(ast_manager & m, subpaving::context & s, expr2var * e2v):
m_manager(m),
@ -71,7 +70,6 @@ struct expr2subpaving::imp {
m_expr2var_owner = false;
}
m_cancel = false;
}
~imp() {
@ -95,7 +93,7 @@ struct expr2subpaving::imp {
}
void checkpoint() {
if (m_cancel)
if (m().canceled())
throw default_exception("canceled");
cooperate("expr2subpaving");
}
@ -357,9 +355,6 @@ struct expr2subpaving::imp {
return m_expr2var->is_var(t);
}
void set_cancel(bool f) {
m_cancel = f;
}
subpaving::var internalize_term(expr * t, mpz & n, mpz & d) {
return process(t, 0, n, d);
@ -386,9 +381,6 @@ bool expr2subpaving::is_var(expr * t) const {
return m_imp->is_var(t);
}
void expr2subpaving::set_cancel(bool f) {
m_imp->set_cancel(f);
}
subpaving::var expr2subpaving::internalize_term(expr * t, mpz & n, mpz & d) {
return m_imp->internalize_term(t, n, d);

7
src/math/subpaving/tactic/expr2subpaving.h
View file

@ -40,12 +40,7 @@ public:
\brief Return true if t was encoded as a variable by the translator.
*/
bool is_var(expr * t) const;
/**
\brief Cancel/Interrupt execution.
*/
void set_cancel(bool f);
/**
\brief Internalize a Z3 arithmetical expression into the subpaving data-structure.

6
src/math/subpaving/tactic/subpaving_tactic.cpp
View file

@ -124,7 +124,6 @@ class subpaving_tactic : public tactic {
}
void set_cancel(bool f) {
m_e2s->set_cancel(f);
m_ctx->set_cancel(f);
}
@ -279,11 +278,6 @@ public:
}
}
protected:
virtual void set_cancel(bool f) {
if (m_imp)
m_imp->set_cancel(f);
}
};