mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

fix a bug in nla_intervals

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-06-17 17:06:32 -07:00
parent f24bd352e1
commit 73e63e1ad9
3 changed files with 24 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/math/lp/nla_intervals.cpp
View file

@ -37,7 +37,8 @@ void intervals::get_lemma_for_zero_interval(monomial const& m) {
interval signs_a = mul_signs_with_deps(m.vars()); interval signs_a = mul_signs_with_deps(m.vars());
add_empty_lemma(); add_empty_lemma();
svector<lp::constraint_index> expl; svector<lp::constraint_index> expl;
m_dep_manager.linearize(signs_a.m_lower_dep, expl); m_dep_manager.linearize(signs_a.m_lower_dep, expl);
TRACE("nla_solver", print_vector(expl, tout) << "\n";);
_().current_expl().add_expl(expl); _().current_expl().add_expl(expl);
mk_ineq(m.var(), llc::EQ); mk_ineq(m.var(), llc::EQ);
TRACE("nla_solver", _().print_lemma(tout); ); TRACE("nla_solver", _().print_lemma(tout); );
@ -90,7 +91,7 @@ bool intervals::get_lemma_for_upper(const monomial& m, const interval& a) {
bool intervals::get_lemma(monomial const& m) { bool intervals::get_lemma(monomial const& m) {
interval b, c, d; interval b, c, d;
interval a = mul(m.vars()); interval a = mul(m.vars());
if (m_config.is_zero(a)) { if (m_imanager.is_zero(a)) {
get_lemma_for_zero_interval(m); get_lemma_for_zero_interval(m);
return true; return true;
} }
@ -206,6 +207,22 @@ lp::impq intervals::get_lower_bound_of_monomial(lpvar j) const {
return r; return r;
} }
std::ostream& intervals::display(std::ostream& out, const interval& i) const {
if (m_imanager.lower_is_inf(i)) {
out << "(-oo";
} else {
out << (m_imanager.lower_is_open(i)? "(":"[") << rational(m_imanager.lower(i));
}
out << ",";
if (m_imanager.upper_is_inf(i)) {
out << "oo)";
} else {
out << rational(m_imanager.upper(i)) << (m_imanager.lower_is_open(i)? ")":"]");
}
return out;
}
intervals::interval intervals::mul(const svector<lpvar>& vars) const { intervals::interval intervals::mul(const svector<lpvar>& vars) const {
interval a; interval a;
m_imanager.set(a, mpq(1)); m_imanager.set(a, mpq(1));

6
src/math/lp/nla_intervals.h
View file

@ -145,8 +145,9 @@ class intervals : common {
mutable interval_manager<im_config> m_imanager; mutable interval_manager<im_config> m_imanager;
region m_region; region m_region;
public:
typedef interval_manager<im_config>::interval interval; typedef interval_manager<im_config>::interval interval;
private:
void set_var_interval(lpvar v, interval & b) const; void set_var_interval(lpvar v, interval & b) const;
void set_var_interval_signs(lpvar v, interval & b) const; void set_var_interval_signs(lpvar v, interval & b) const;
@ -184,6 +185,7 @@ public:
void push(); void push();
void pop(unsigned k); void pop(unsigned k);
void init(); void init();
std::ostream& display(std::ostream& out, const intervals::interval& i) const;
}; };
} // end of namespace nla } // end of namespace nla

1
src/smt/smt_context_pp.cpp
View file

@ -493,6 +493,7 @@ namespace smt {
TRACE("lemma", tout << strm.str() << "\n";); TRACE("lemma", tout << strm.str() << "\n";);
display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic); display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic);
out.close(); out.close();
return m_lemma_id; return m_lemma_id;
} }