mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

add bailout option for code review #5208

Browse source 
@levnach
Could you review and maybe make this much more streamlined?
The patch is to simply bail out the iterator if it fails to find canonical monics.
If m_ff could produce the existing canonical monics up front this kind of bail-out could maybe avoided.
This commit is contained in:
Nikolaj Bjorner 2021-04-22 11:30:00 -07:00
parent a52b485d9c
commit d67919373e
2 changed files with 17 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/math/lp/factorization.cpp
View file

@ -23,21 +23,30 @@ bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const
std::sort(k_vars.begin(), k_vars.end()); std::sort(k_vars.begin(), k_vars.end());
std::sort(j_vars.begin(), j_vars.end()); std::sort(j_vars.begin(), j_vars.end());
if (false && m_num_failures > 10) {
for (bool& m : m_mask) m = true;
m_mask[0] = false;
m_full_factorization_returned = true;
return false;
}
if (k_vars.size() == 1) { if (k_vars.size() == 1) {
k.set(k_vars[0], factor_type::VAR); k.set(k_vars[0], factor_type::VAR);
} else { } else {
unsigned i; unsigned i;
if (!m_ff->find_canonical_monic_of_vars(k_vars, i)) { if (!m_ff->find_canonical_monic_of_vars(k_vars, i)) {
++m_num_failures;
return false; return false;
} }
k.set(i, factor_type::MON); k.set(i, factor_type::MON);
} }
m_num_failures = 0;
if (j_vars.size() == 1) { if (j_vars.size() == 1) {
j.set(j_vars[0], factor_type::VAR); j.set(j_vars[0], factor_type::VAR);
} else { } else {
unsigned i; unsigned i;
if (!m_ff->find_canonical_monic_of_vars(j_vars, i)) { if (!m_ff->find_canonical_monic_of_vars(j_vars, i)) {
++m_num_failures;
return false; return false;
} }
j.set(i, factor_type::MON); j.set(i, factor_type::MON);
@ -46,7 +55,7 @@ bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const
} }
factorization const_iterator_mon::operator*() const { factorization const_iterator_mon::operator*() const {
if (m_full_factorization_returned == false) { if (!m_full_factorization_returned) {
return create_full_factorization(m_ff->m_monic); return create_full_factorization(m_ff->m_monic);
} }
factor j, k; rational sign; factor j, k; rational sign;

13
src/math/lp/factorization.h
View file

@ -30,12 +30,12 @@ struct factorization_factory;
enum class factor_type { VAR, MON }; enum class factor_type { VAR, MON };
class factor { class factor {
lpvar m_var; lpvar m_var{ UINT_MAX };
factor_type m_type; factor_type m_type{ factor_type::VAR };
bool m_sign; bool m_sign{ false };
public: public:
factor(): factor(false) {} factor(): factor(false) {}
factor(bool sign): m_var(UINT_MAX), m_type(factor_type::VAR), m_sign(sign) {} factor(bool sign): m_sign(sign) {}
explicit factor(lpvar v, factor_type t) : m_var(v), m_type(t), m_sign(false) {} explicit factor(lpvar v, factor_type t) : m_var(v), m_type(t), m_sign(false) {}
unsigned var() const { return m_var; } unsigned var() const { return m_var; }
factor_type type() const { return m_type; } factor_type type() const { return m_type; }
@ -77,9 +77,10 @@ public:
struct const_iterator_mon { struct const_iterator_mon {
// fields // fields
bool_vector m_mask; mutable bool_vector m_mask;
const factorization_factory * m_ff; const factorization_factory * m_ff;
bool m_full_factorization_returned; mutable bool m_full_factorization_returned;
mutable unsigned m_num_failures{ 0 };
// typedefs // typedefs
typedef const_iterator_mon self_type; typedef const_iterator_mon self_type;