mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Cache isolating interval for better pretty printing

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-01-14 12:17:15 -08:00
parent 025cb2a2a8
commit 991a1528cd
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -281,7 +281,8 @@ namespace realclosure {
struct algebraic : public extension { struct algebraic : public extension {
polynomial m_p; polynomial m_p;
sign_det * m_sign_det; //!< != 0 if m_interval constains more than one root of m_p. mpbqi m_iso_interval;
sign_det * m_sign_det; //!< != 0 if m_iso_interval constains more than one root of m_p.
unsigned m_sc_idx; //!< != UINT_MAX if m_sign_det != 0, in this case m_sc_idx < m_sign_det->m_sign_conditions.size() unsigned m_sc_idx; //!< != UINT_MAX if m_sign_det != 0, in this case m_sc_idx < m_sign_det->m_sign_conditions.size()
bool m_depends_on_infinitesimals; //!< True if the polynomial p depends on infinitesimal extensions. bool m_depends_on_infinitesimals; //!< True if the polynomial p depends on infinitesimal extensions.
@ -292,6 +293,7 @@ namespace realclosure {
sign_det * sdt() const { return m_sign_det; } sign_det * sdt() const { return m_sign_det; }
unsigned sc_idx() const { return m_sc_idx; } unsigned sc_idx() const { return m_sc_idx; }
unsigned num_roots_inside_interval() const { return m_sign_det == 0 ? 1 : m_sign_det->num_roots(); } unsigned num_roots_inside_interval() const { return m_sign_det == 0 ? 1 : m_sign_det->num_roots(); }
mpbqi & iso_interval() { return m_iso_interval; }
}; };
struct transcendental : public extension { struct transcendental : public extension {
@ -808,6 +810,7 @@ namespace realclosure {
void del_algebraic(algebraic * a) { void del_algebraic(algebraic * a) {
reset_p(a->m_p); reset_p(a->m_p);
bqim().del(a->m_interval); bqim().del(a->m_interval);
bqim().del(a->m_iso_interval);
dec_ref_sign_det(a->m_sign_det); dec_ref_sign_det(a->m_sign_det);
allocator().deallocate(sizeof(algebraic), a); allocator().deallocate(sizeof(algebraic), a);
} }
@ -1793,6 +1796,7 @@ namespace realclosure {
set_p(r->m_p, p_sz, p); set_p(r->m_p, p_sz, p);
set_interval(r->m_interval, interval); set_interval(r->m_interval, interval);
set_interval(r->m_iso_interval, interval);
r->m_sign_det = sd; r->m_sign_det = sd;
inc_ref_sign_det(sd); inc_ref_sign_det(sd);
r->m_sc_idx = sc_idx; r->m_sc_idx = sc_idx;
@ -5603,7 +5607,7 @@ namespace realclosure {
out << "root("; out << "root(";
display_polynomial(out, a->p(), display_free_var_proc(), compact); display_polynomial(out, a->p(), display_free_var_proc(), compact);
out << ", "; out << ", ";
bqim().display(out, a->interval()); bqim().display(out, a->iso_interval());
out << ", "; out << ", ";
if (a->sdt() != 0) if (a->sdt() != 0)
display_sign_conditions(out, a->sdt()->sc(a->sc_idx()), a->sdt()->qs(), compact); display_sign_conditions(out, a->sdt()->sc(a->sc_idx()), a->sdt()->qs(), compact);