mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix #4227

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-05-06 12:56:46 -07:00
parent 603b5552fa
commit 691759c9e2
3 changed files with 13 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/smt/old_interval.cpp
View file

@ -473,6 +473,14 @@ interval & interval::operator*=(interval const & other) {
return *this; return *this;
} }
bool interval::empty() const {
if (m_lower.is_infinite() || m_upper.is_infinite())
return false;
if (m_lower < m_upper)
return false;
return m_lower > m_upper || m_lower_open || m_upper_open;
}
bool interval::contains_zero() const { bool interval::contains_zero() const {
TRACE("interval_zero_bug", tout << "contains_zero info: " << *this << "\n"; TRACE("interval_zero_bug", tout << "contains_zero info: " << *this << "\n";
tout << "m_lower.is_neg(): " << m_lower.is_neg() << "\n"; tout << "m_lower.is_neg(): " << m_lower.is_neg() << "\n";

1
src/smt/old_interval.h
View file

@ -102,6 +102,7 @@ public:
bool operator==(old_interval const & other) const { return m_lower == other.m_lower && m_upper == other.m_upper && m_lower_open == other.m_lower_open && m_upper_open == other.m_upper_open; } bool operator==(old_interval const & other) const { return m_lower == other.m_lower && m_upper == other.m_upper && m_lower_open == other.m_lower_open && m_upper_open == other.m_upper_open; }
bool contains_zero() const; bool contains_zero() const;
bool contains(rational const& v) const; bool contains(rational const& v) const;
bool empty() const;
old_interval & inv(); old_interval & inv();
void expt(unsigned n); void expt(unsigned n);
void neg(); void neg();

8
src/smt/theory_arith_nl.h
View file

@ -226,23 +226,23 @@ interval theory_arith<Ext>::mk_interval_for(theory_var v) {
} }
return interval(m_dep_manager, return interval(m_dep_manager,
l->get_value().get_rational().to_rational(), l->get_value().get_rational().to_rational(),
!l->get_value().get_infinitesimal().to_rational().is_zero(), l->get_value().get_infinitesimal().to_rational().is_pos(),
m_dep_manager.mk_leaf(l), m_dep_manager.mk_leaf(l),
u->get_value().get_rational().to_rational(), u->get_value().get_rational().to_rational(),
!u->get_value().get_infinitesimal().to_rational().is_zero(), u->get_value().get_infinitesimal().to_rational().is_neg(),
m_dep_manager.mk_leaf(u)); m_dep_manager.mk_leaf(u));
} }
else if (l) { else if (l) {
return interval(m_dep_manager, return interval(m_dep_manager,
l->get_value().get_rational().to_rational(), l->get_value().get_rational().to_rational(),
!l->get_value().get_infinitesimal().to_rational().is_zero(), l->get_value().get_infinitesimal().to_rational().is_pos(),
true, true,
m_dep_manager.mk_leaf(l)); m_dep_manager.mk_leaf(l));
} }
else if (u) { else if (u) {
return interval(m_dep_manager, return interval(m_dep_manager,
u->get_value().get_rational().to_rational(), u->get_value().get_rational().to_rational(),
!u->get_value().get_infinitesimal().to_rational().is_zero(), u->get_value().get_infinitesimal().to_rational().is_neg(),
false, false,
m_dep_manager.mk_leaf(u)); m_dep_manager.mk_leaf(u));
} }