mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-03 11:25:40 +00:00
Code Activity

return diagnostics

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-04-25 13:47:02 -07:00
parent d8156aeff3
commit d4fa990b6e
1 changed files with 12 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/math/lp/bound_analyzer_on_row.h
View file

@ -54,32 +54,40 @@ public :
{} {}
static void analyze_row(const C & row, static unsigned analyze_row(const C & row,
unsigned bj, // basis column for the row unsigned bj, // basis column for the row
const numeric_pair<mpq>& rs, const numeric_pair<mpq>& rs,
unsigned row_or_term_index, unsigned row_or_term_index,
B & bp) { B & bp) {
bound_analyzer_on_row a(row, bj, rs, row_or_term_index, bp); bound_analyzer_on_row a(row, bj, rs, row_or_term_index, bp);
a.analyze(); return a.analyze();
} }
private: private:
void analyze() { unsigned analyze() {
unsigned num_prop = 0;
for (const auto & c : m_row) { for (const auto & c : m_row) {
if ((m_column_of_l == -2) && (m_column_of_u == -2)) if ((m_column_of_l == -2) && (m_column_of_u == -2))
return; return 0;
analyze_bound_on_var_on_coeff(c.var(), c.coeff()); analyze_bound_on_var_on_coeff(c.var(), c.coeff());
} }
++num_prop;
if (m_column_of_u >= 0) if (m_column_of_u >= 0)
limit_monoid_u_from_below(); limit_monoid_u_from_below();
else if (m_column_of_u == -1) else if (m_column_of_u == -1)
limit_all_monoids_from_below(); limit_all_monoids_from_below();
else
--num_prop;
++num_prop;
if (m_column_of_l >= 0) if (m_column_of_l >= 0)
limit_monoid_l_from_above(); limit_monoid_l_from_above();
else if (m_column_of_l == -1) else if (m_column_of_l == -1)
limit_all_monoids_from_above(); limit_all_monoids_from_above();
else
--num_prop;
return num_prop;
} }
bool bound_is_available(unsigned j, bool lower_bound) { bool bound_is_available(unsigned j, bool lower_bound) {