mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 14:23:40 +00:00
Code Activity

neatify

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-06-13 15:20:21 -07:00
parent 5ee9edf46b
commit 53e49eb428
1 changed files with 18 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

40
src/smt/theory_lra.cpp
View file

@ -3160,27 +3160,25 @@ public:
unsigned get_num_vars() const { return th.get_num_vars(); } unsigned get_num_vars() const { return th.get_num_vars(); }
void report_equality_of_fixed_vars(unsigned vi1, unsigned vi2) { void report_equality_of_fixed_vars(unsigned vi1, unsigned vi2) {
rational bound;
lp::constraint_index ci1, ci2, ci3, ci4; lp::constraint_index ci1, ci2, ci3, ci4;
theory_var v1 = lp().local_to_external(vi1); theory_var v1 = lp().local_to_external(vi1);
theory_var v2 = lp().local_to_external(vi2); theory_var v2 = lp().local_to_external(vi2);
TRACE("arith", tout << "fixed: " << mk_pp(get_owner(v1), m) << " " << mk_pp(get_owner(v2), m) << "\n";);
// we expect lp() to ensure that none of these returns happen.
if (is_equal(v1, v2)) if (is_equal(v1, v2))
return; return;
SASSERT(is_int(v1) == is_int(v2)); if (is_int(v1) != is_int(v2))
lp::mpq bound;
TRACE("arith",
bool hlb = has_lower_bound(vi2, ci3, bound); // has_lower_bound in turn trace "arith"
tout << "fixed: " << mk_pp(get_owner(v1), m) << " " << mk_pp(get_owner(v2), m) << " " << bound << " " << hlb << std::endl;);
if (!(has_lower_bound(vi2, ci3, bound)
&&
has_upper_bound(vi2, ci4, bound)
&&
has_lower_bound(vi1, ci1, bound)
&&
has_upper_bound(vi1, ci2, bound))) {
TRACE("arith", tout << "strange\n";);
return; return;
} if (!has_lower_bound(vi1, ci1, bound))
return;
if (!has_upper_bound(vi1, ci2, bound))
return;
if (!has_lower_bound(vi2, ci3, bound))
return;
if (!has_upper_bound(vi2, ci4, bound))
return;
++m_stats.m_fixed_eqs; ++m_stats.m_fixed_eqs;
reset_evidence(); reset_evidence();
set_evidence(ci1, m_core, m_eqs); set_evidence(ci1, m_core, m_eqs);
@ -3195,13 +3193,11 @@ public:
get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), x, y, 0, nullptr)); get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), x, y, 0, nullptr));
TRACE("arith", TRACE("arith",
for (unsigned i = 0; i < m_core.size(); ++i) { tout << "bound " << bound << "\n";
ctx().display_detailed_literal(tout, m_core[i]); for (auto c : m_core)
tout << "\n"; ctx().display_detailed_literal(tout, c) << "\n";
} for (auto e : m_eqs)
for (unsigned i = 0; i < m_eqs.size(); ++i) { tout << mk_pp(e.first->get_owner(), m) << " = " << mk_pp(e.second->get_owner(), m) << "\n";
tout << mk_pp(m_eqs[i].first->get_owner(), m) << " = " << mk_pp(m_eqs[i].second->get_owner(), m) << "\n";
}
tout << " ==> "; tout << " ==> ";
tout << mk_pp(x->get_owner(), m) << " = " << mk_pp(y->get_owner(), m) << "\n"; tout << mk_pp(x->get_owner(), m) << " = " << mk_pp(y->get_owner(), m) << "\n";
); );