mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
pass algebraic manager to arith-plugin mk-numeral because rational check may overwrite the argument using the current manager deals with crash as part of #4532
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
ac39ddb43f
commit
c7704ef9af
|
@ -134,7 +134,7 @@ extern "C" {
|
|||
_am.set(_av, av.to_mpq()); \
|
||||
scoped_anum _r(_am); \
|
||||
_am.IRAT_OP(_av, bv, _r); \
|
||||
r = au(c).mk_numeral(_r, false); \
|
||||
r = au(c).mk_numeral(_am, _r, false); \
|
||||
} \
|
||||
} \
|
||||
else { \
|
||||
|
@ -145,13 +145,13 @@ extern "C" {
|
|||
_am.set(_bv, bv.to_mpq()); \
|
||||
scoped_anum _r(_am); \
|
||||
_am.IRAT_OP(av, _bv, _r); \
|
||||
r = au(c).mk_numeral(_r, false); \
|
||||
r = au(c).mk_numeral(_am, _r, false); \
|
||||
} \
|
||||
else { \
|
||||
algebraic_numbers::anum const & bv = get_irrational(c, b); \
|
||||
scoped_anum _r(_am); \
|
||||
_am.IRAT_OP(av, bv, _r); \
|
||||
r = au(c).mk_numeral(_r, false); \
|
||||
r = au(c).mk_numeral(_am, _r, false); \
|
||||
} \
|
||||
} \
|
||||
mk_c(c)->save_ast_trail(r); \
|
||||
|
@ -226,7 +226,7 @@ extern "C" {
|
|||
algebraic_numbers::anum const & av = get_irrational(c, a);
|
||||
_am.root(av, k, _r);
|
||||
}
|
||||
expr * r = au(c).mk_numeral(_r, false);
|
||||
expr * r = au(c).mk_numeral(_am, _r, false);
|
||||
mk_c(c)->save_ast_trail(r);
|
||||
RETURN_Z3(of_ast(r));
|
||||
Z3_CATCH_RETURN(nullptr);
|
||||
|
@ -248,7 +248,7 @@ extern "C" {
|
|||
algebraic_numbers::anum const & av = get_irrational(c, a);
|
||||
_am.power(av, k, _r);
|
||||
}
|
||||
expr * r = au(c).mk_numeral(_r, false);
|
||||
expr * r = au(c).mk_numeral(_am, _r, false);
|
||||
mk_c(c)->save_ast_trail(r);
|
||||
RETURN_Z3(of_ast(r));
|
||||
Z3_CATCH_RETURN(nullptr);
|
||||
|
@ -380,7 +380,7 @@ extern "C" {
|
|||
Z3_ast_vector_ref* result = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
|
||||
mk_c(c)->save_object(result);
|
||||
for (unsigned i = 0; i < roots.size(); i++) {
|
||||
result->m_ast_vector.push_back(au(c).mk_numeral(roots.get(i), false));
|
||||
result->m_ast_vector.push_back(au(c).mk_numeral(_am, roots.get(i), false));
|
||||
}
|
||||
RETURN_Z3(of_ast_vector(result));
|
||||
Z3_CATCH_RETURN(nullptr);
|
||||
|
|
|
@ -39,11 +39,11 @@ struct arith_decl_plugin::algebraic_numbers_wrapper {
|
|||
|
||||
unsigned mk_id(algebraic_numbers::anum const & val) {
|
||||
SASSERT(!m_amanager.is_rational(val));
|
||||
unsigned new_id = m_id_gen.mk();
|
||||
m_nums.reserve(new_id+1);
|
||||
m_amanager.set(m_nums[new_id], val);
|
||||
TRACE("algebraic2expr", tout << "mk_id -> " << new_id << "\n"; m_amanager.display(tout, val); tout << "\n";);
|
||||
return new_id;
|
||||
unsigned idx = m_id_gen.mk();
|
||||
m_nums.reserve(idx+1);
|
||||
m_amanager.set(m_nums[idx], val);
|
||||
TRACE("algebraic2expr", tout << "mk_id -> " << idx << "\n"; m_amanager.display(tout, val); tout << "\n";);
|
||||
return idx;
|
||||
}
|
||||
|
||||
void recycle_id(unsigned idx) {
|
||||
|
@ -66,8 +66,8 @@ struct arith_decl_plugin::algebraic_numbers_wrapper {
|
|||
};
|
||||
|
||||
arith_decl_plugin::algebraic_numbers_wrapper & arith_decl_plugin::aw() const {
|
||||
if (m_aw == nullptr)
|
||||
const_cast<arith_decl_plugin*>(this)->m_aw = alloc(algebraic_numbers_wrapper, m_manager->limit());
|
||||
if (m_aw == nullptr)
|
||||
const_cast<arith_decl_plugin*>(this)->m_aw = alloc(algebraic_numbers_wrapper, m_manager->limit());
|
||||
return *m_aw;
|
||||
}
|
||||
|
||||
|
@ -75,10 +75,10 @@ algebraic_numbers::manager & arith_decl_plugin::am() const {
|
|||
return aw().m_amanager;
|
||||
}
|
||||
|
||||
app * arith_decl_plugin::mk_numeral(algebraic_numbers::anum const & val, bool is_int) {
|
||||
if (am().is_rational(val)) {
|
||||
app * arith_decl_plugin::mk_numeral(algebraic_numbers::manager& m, algebraic_numbers::anum const & val, bool is_int) {
|
||||
if (m.is_rational(val)) {
|
||||
rational rval;
|
||||
am().to_rational(val, rval);
|
||||
m.to_rational(val, rval);
|
||||
return mk_numeral(rval, is_int);
|
||||
}
|
||||
else {
|
||||
|
@ -103,7 +103,7 @@ app * arith_decl_plugin::mk_numeral(algebraic_numbers::anum const & val, bool is
|
|||
app * arith_decl_plugin::mk_numeral(sexpr const * p, unsigned i) {
|
||||
scoped_anum r(am());
|
||||
am().mk_root(p, i, r);
|
||||
return mk_numeral(r, false);
|
||||
return mk_numeral(am(), r, false);
|
||||
}
|
||||
|
||||
void arith_decl_plugin::del(parameter const & p) {
|
||||
|
|
|
@ -195,7 +195,7 @@ public:
|
|||
|
||||
app * mk_numeral(rational const & n, bool is_int);
|
||||
|
||||
app * mk_numeral(algebraic_numbers::anum const & val, bool is_int);
|
||||
app * mk_numeral(algebraic_numbers::manager& m, algebraic_numbers::anum const & val, bool is_int);
|
||||
|
||||
// Create a (real) numeral that is the i-th root of the polynomial encoded using the given sexpr.
|
||||
app * mk_numeral(sexpr const * p, unsigned i);
|
||||
|
@ -401,8 +401,8 @@ public:
|
|||
SASSERT(is_int(s) || is_real(s));
|
||||
return mk_numeral(val, is_int(s));
|
||||
}
|
||||
app * mk_numeral(algebraic_numbers::anum const & val, bool is_int) {
|
||||
return plugin().mk_numeral(val, is_int);
|
||||
app * mk_numeral(algebraic_numbers::manager& m, algebraic_numbers::anum const & val, bool is_int) {
|
||||
return plugin().mk_numeral(m, val, is_int);
|
||||
}
|
||||
app * mk_numeral(sexpr const * p, unsigned i) {
|
||||
return plugin().mk_numeral(p, i);
|
||||
|
|
|
@ -755,7 +755,7 @@ br_status arith_rewriter::mk_add_core(unsigned num_args, expr * const * args, ex
|
|||
for (unsigned i = 0; i < num_args; i ++) {
|
||||
unsigned d = am.degree(r);
|
||||
if (d > 1 && d > m_max_degree) {
|
||||
new_args.push_back(m_util.mk_numeral(r, false));
|
||||
new_args.push_back(m_util.mk_numeral(am, r, false));
|
||||
am.set(r, 0);
|
||||
}
|
||||
|
||||
|
@ -777,11 +777,11 @@ br_status arith_rewriter::mk_add_core(unsigned num_args, expr * const * args, ex
|
|||
}
|
||||
|
||||
if (new_args.empty()) {
|
||||
result = m_util.mk_numeral(r, false);
|
||||
result = m_util.mk_numeral(am, r, false);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
new_args.push_back(m_util.mk_numeral(r, false));
|
||||
new_args.push_back(m_util.mk_numeral(am, r, false));
|
||||
br_status st = poly_rewriter<arith_rewriter_core>::mk_add_core(new_args.size(), new_args.c_ptr(), result);
|
||||
if (st == BR_FAILED) {
|
||||
result = m().mk_app(get_fid(), OP_ADD, new_args.size(), new_args.c_ptr());
|
||||
|
@ -805,7 +805,7 @@ br_status arith_rewriter::mk_mul_core(unsigned num_args, expr * const * args, ex
|
|||
for (unsigned i = 0; i < num_args; i ++) {
|
||||
unsigned d = am.degree(r);
|
||||
if (d > 1 && d > m_max_degree) {
|
||||
new_args.push_back(m_util.mk_numeral(r, false));
|
||||
new_args.push_back(m_util.mk_numeral(am, r, false));
|
||||
am.set(r, 1);
|
||||
}
|
||||
|
||||
|
@ -826,10 +826,10 @@ br_status arith_rewriter::mk_mul_core(unsigned num_args, expr * const * args, ex
|
|||
}
|
||||
|
||||
if (new_args.empty()) {
|
||||
result = m_util.mk_numeral(r, false);
|
||||
result = m_util.mk_numeral(am, r, false);
|
||||
return BR_DONE;
|
||||
}
|
||||
new_args.push_back(m_util.mk_numeral(r, false));
|
||||
new_args.push_back(m_util.mk_numeral(am, r, false));
|
||||
|
||||
br_status st = poly_rewriter<arith_rewriter_core>::mk_mul_core(new_args.size(), new_args.c_ptr(), result);
|
||||
if (st == BR_FAILED) {
|
||||
|
@ -857,7 +857,7 @@ br_status arith_rewriter::mk_div_irrat_rat(expr * arg1, expr * arg2, expr_ref &
|
|||
am.set(val2, rval2.to_mpq());
|
||||
scoped_anum r(am);
|
||||
am.div(val1, val2, r);
|
||||
result = m_util.mk_numeral(r, false);
|
||||
result = m_util.mk_numeral(am, r, false);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
@ -873,7 +873,7 @@ br_status arith_rewriter::mk_div_rat_irrat(expr * arg1, expr * arg2, expr_ref &
|
|||
anum const & val2 = m_util.to_irrational_algebraic_numeral(arg2);
|
||||
scoped_anum r(am);
|
||||
am.div(val1, val2, r);
|
||||
result = m_util.mk_numeral(r, false);
|
||||
result = m_util.mk_numeral(am, r, false);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
@ -890,7 +890,7 @@ br_status arith_rewriter::mk_div_irrat_irrat(expr * arg1, expr * arg2, expr_ref
|
|||
return BR_FAILED;
|
||||
scoped_anum r(am);
|
||||
am.div(val1, val2, r);
|
||||
result = m_util.mk_numeral(r, false);
|
||||
result = m_util.mk_numeral(am, r.get(), false);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
@ -1351,7 +1351,7 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
|
|||
am.root(r, u_den_y, r);
|
||||
if (is_neg_y)
|
||||
am.inv(r);
|
||||
result = m_util.mk_numeral(r, false);
|
||||
result = m_util.mk_numeral(am, r, false);
|
||||
return BR_DONE;
|
||||
}
|
||||
return BR_FAILED;
|
||||
|
@ -1370,7 +1370,7 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
|
|||
am.root(r, u_den_y, r);
|
||||
if (is_neg_y)
|
||||
am.inv(r);
|
||||
result = m_util.mk_numeral(r, false);
|
||||
result = m_util.mk_numeral(am, r, false);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
|
|
@ -449,7 +449,7 @@ namespace algebraic_numbers {
|
|||
}
|
||||
|
||||
void copy_poly(algebraic_cell * c, unsigned sz, mpz const * p) {
|
||||
SASSERT(c->m_p == 0);
|
||||
SASSERT(c->m_p == nullptr);
|
||||
SASSERT(c->m_p_sz == 0);
|
||||
c->m_p_sz = sz;
|
||||
c->m_p = static_cast<mpz*>(m_allocator.allocate(sizeof(mpz)*sz));
|
||||
|
@ -476,7 +476,7 @@ namespace algebraic_numbers {
|
|||
target->m_sign_lower = source->m_sign_lower;
|
||||
target->m_not_rational = source->m_not_rational;
|
||||
target->m_i = source->m_i;
|
||||
SASSERT(acell_inv(*source));
|
||||
//SASSERT(acell_inv(*source)); source could be owned by a different manager
|
||||
SASSERT(acell_inv(*target));
|
||||
}
|
||||
|
||||
|
|
|
@ -105,13 +105,13 @@ class nlsat_tactic : public tactic {
|
|||
continue;
|
||||
expr * v;
|
||||
try {
|
||||
v = util.mk_numeral(m_solver.value(x), util.is_int(t));
|
||||
v = util.mk_numeral(m_solver.am(), m_solver.value(x), util.is_int(t));
|
||||
}
|
||||
catch (z3_error & ex) {
|
||||
throw ex;
|
||||
}
|
||||
catch (z3_exception &) {
|
||||
v = util.mk_to_int(util.mk_numeral(m_solver.value(x), false));
|
||||
v = util.mk_to_int(util.mk_numeral(m_solver.am(), m_solver.value(x), false));
|
||||
ok = false;
|
||||
}
|
||||
md->register_decl(to_app(t)->get_decl(), v);
|
||||
|
|
|
@ -796,13 +796,13 @@ namespace qe {
|
|||
continue;
|
||||
expr * v;
|
||||
try {
|
||||
v = util.mk_numeral(s.m_rmodel0.value(x), util.is_int(t));
|
||||
v = util.mk_numeral(s.m_solver.am(), s.m_rmodel0.value(x), util.is_int(t));
|
||||
}
|
||||
catch (z3_error & ex) {
|
||||
throw ex;
|
||||
}
|
||||
catch (z3_exception &) {
|
||||
v = util.mk_to_int(util.mk_numeral(s.m_rmodel0.value(x), false));
|
||||
v = util.mk_to_int(util.mk_numeral(s.m_solver.am(), s.m_rmodel0.value(x), false));
|
||||
ok = false;
|
||||
}
|
||||
md->register_decl(to_app(t)->get_decl(), v);
|
||||
|
|
|
@ -3454,7 +3454,7 @@ public:
|
|||
if (a.is_int(o) && !m_nla->am().is_int(an)) {
|
||||
return alloc(expr_wrapper_proc, a.mk_numeral(rational::zero(), a.is_int(o)));
|
||||
}
|
||||
return alloc(expr_wrapper_proc, a.mk_numeral(nl_value(v, *m_a1), a.is_int(o)));
|
||||
return alloc(expr_wrapper_proc, a.mk_numeral(m_nla->am(), nl_value(v, *m_a1), a.is_int(o)));
|
||||
}
|
||||
else {
|
||||
rational r = get_value(v);
|
||||
|
|
|
@ -31,6 +31,7 @@ public:
|
|||
mpq():m_den(1) {}
|
||||
mpq(mpq &&) noexcept = default;
|
||||
mpq & operator=(mpq&&) = default;
|
||||
mpq & operator=(mpq const&) = delete;
|
||||
void swap(mpq & other) { m_num.swap(other.m_num); m_den.swap(other.m_den); }
|
||||
mpz const & numerator() const { return m_num; }
|
||||
mpz const & denominator() const { return m_den; }
|
||||
|
|
|
@ -202,12 +202,14 @@ mpz_cell * mpz_manager<SYNCH>::allocate(unsigned capacity) {
|
|||
}
|
||||
#endif
|
||||
cell->m_capacity = capacity;
|
||||
|
||||
return cell;
|
||||
}
|
||||
|
||||
template<bool SYNCH>
|
||||
void mpz_manager<SYNCH>::deallocate(bool is_heap, mpz_cell * ptr) {
|
||||
if (is_heap) {
|
||||
|
||||
#ifdef SINGLE_THREAD
|
||||
m_allocator.deallocate(cell_size(ptr->m_capacity), ptr);
|
||||
#else
|
||||
|
|
|
@ -106,6 +106,7 @@ public:
|
|||
std::swap(m_ptr, other.m_ptr);
|
||||
}
|
||||
|
||||
mpz& operator=(mpz const& other) = delete;
|
||||
mpz& operator=(mpz &&other) {
|
||||
swap(other);
|
||||
return *this;
|
||||
|
@ -535,13 +536,6 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
void set(mpz & target, mpz && source) {
|
||||
target.m_val = source.m_val;
|
||||
std::swap(target.m_ptr, source.m_ptr);
|
||||
auto o = target.m_owner; target.m_owner = source.m_owner; source.m_owner = o;
|
||||
auto k = target.m_kind; target.m_kind = source.m_kind; source.m_kind = k;
|
||||
}
|
||||
|
||||
void set(mpz & a, int val) {
|
||||
a.m_val = val;
|
||||
a.m_kind = mpz_small;
|
||||
|
@ -724,6 +718,7 @@ public:
|
|||
|
||||
// Store the digits of n into digits, and return the sign.
|
||||
bool decompose(mpz const & n, svector<digit_t> & digits);
|
||||
|
||||
};
|
||||
|
||||
#ifndef SINGLE_THREAD
|
||||
|
|
Loading…
Reference in a new issue