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

tidy

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-03-19 17:57:52 -10:00 committed by Lev Nachmanson
parent a41bd38a3a
commit 7fb40e86eb
1 changed files with 13 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/math/lp/dioph_eq.cpp
View file

@ -63,9 +63,10 @@ namespace lp {
class bijection { class bijection {
std::unordered_map<unsigned, unsigned> m_map; std::unordered_map<unsigned, unsigned> m_map;
std::unordered_map<unsigned, unsigned> m_rev_map; std::unordered_map<unsigned, unsigned> m_rev_map;
public:
auto map_begin() const { return m_map.begin(); } auto map_begin() const { return m_map.begin(); }
auto map_end() const { return m_map.end(); } auto map_end() const { return m_map.end(); }
public:
// Iterator helper // Iterator helper
struct map_it { struct map_it {
@ -1707,14 +1708,13 @@ namespace lp {
} }
} }
// m_espace contains the coefficients of the term // m_espace contains the coefficients of the term
// m_c contains the fixed part of the term // m_c contains the fixed part of the term
// m_tmp_l is the linear combination of the equations that removes the // m_tmp_l is the linear combination of the equations that removes the
// substituted variables. // substituted variables.
// g is the common gcd // g is the common gcd
// returns true iff the conflict is found // returns true iff the conflict is found
lia_move tighten_one_bound_for_common_gcd(const mpq& g, unsigned j, lia_move tighten_one_bound_for_common_gcd(const mpq& g, unsigned j, bool is_upper) {
bool is_upper) {
mpq rs; mpq rs;
bool is_strict; bool is_strict;
u_dependency* b_dep = nullptr; u_dependency* b_dep = nullptr;
@ -1723,15 +1723,11 @@ namespace lp {
if (lra.has_bound_of_type(j, b_dep, rs, is_strict, is_upper)) { if (lra.has_bound_of_type(j, b_dep, rs, is_strict, is_upper)) {
TRACE("dio", TRACE("dio",
tout << "current " << (is_upper? "upper":"lower") << " bound for x" << j << ":" tout << "current " << (is_upper? "upper":"lower") << " bound for x" << j << ":"
<< rs << std::endl;); << rs << " rs/ g" << rs / g << std::endl;);
rs = rs / g; rs = rs / g;
TRACE("dio", tout << "rs / g:" << rs << std::endl;); CTRACE("dio", rs.is_int(), tout << "no improvement in the bound\n";);
if (!rs.is_int()) { if (!rs.is_int() && tighten_bound_kind_for_common_gcd(g, j, rs, is_upper))
if (tighten_bound_kind_for_common_gcd(g, j, rs, is_upper)) return lia_move::conflict;
return lia_move::conflict;
} else {
TRACE("dio", tout << "no improvement in the bound\n";);
}
} }
return lia_move::undef; return lia_move::undef;
} }
@ -1764,7 +1760,8 @@ namespace lp {
} }
return lia_move::undef; return lia_move::undef;
} }
// returns true only on a conflict
// returns true only on a conflict
bool tighten_bound_kind_for_common_gcd(const mpq& g, unsigned j, const mpq& ub, bool upper) { bool tighten_bound_kind_for_common_gcd(const mpq& g, unsigned j, const mpq& ub, bool upper) {
// ub = upper_bound(j)/g. // ub = upper_bound(j)/g.
// we have xj = t = g*t_<= upper_bound(j), then // we have xj = t = g*t_<= upper_bound(j), then
@ -1802,10 +1799,10 @@ namespace lp {
lra.update_column_type_and_bound(j, kind, bound, dep); lra.update_column_type_and_bound(j, kind, bound, dep);
lp_status st = lra.find_feasible_solution(); lp_status st = lra.find_feasible_solution();
if ((int)st >= (int)lp::lp_status::FEASIBLE) { if (st == lp_status::CANCELLED)
return false; return false;
} if ((int)st >= (int)lp::lp_status::FEASIBLE)
if (st == lp_status::CANCELLED) return false; return false;
lra.get_infeasibility_explanation(m_infeas_explanation); lra.get_infeasibility_explanation(m_infeas_explanation);
return true; return true;
} }