mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-06-01 20:31:05 -07:00
parent 0e6d530518
commit 45adfc6a66
2 changed files with 57 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

68
src/math/lp/int_gcd_test.cpp
View file

@ -75,19 +75,36 @@ namespace lp {
} }
bool int_gcd_test::gcd_test() { bool int_gcd_test::gcd_test() {
reset_parities(); reset_test();
const auto & A = lra.A_r(); // getting the matrix const auto & A = lra.A_r(); // getting the matrix
for (unsigned i = 0; i < A.row_count(); i++) for (unsigned i = 0; i < A.row_count(); i++) {
unsigned basic_var = lra.r_basis()[i];
if (!lia.column_is_int(basic_var))
continue;
if (lia.get_value(basic_var).is_int())
continue;
if (!gcd_test_for_row(A, i)) if (!gcd_test_for_row(A, i))
return false; return false;
mark_visited(i);
}
for (unsigned i = m_inserted_vars.size(); i-- > 0; ) {
unsigned j = m_inserted_vars[i];
for (const auto & c : lra.get_column(j)) {
unsigned r = c.var();
if (is_visited(r))
continue;
mark_visited(r);
if (!gcd_test_for_row(A, r))
return false;
}
}
return true; return true;
} }
static mpq get_denominators_lcm(const row_strip<mpq> & row) { static mpq get_denominators_lcm(const row_strip<mpq> & row) {
mpq r(1); mpq r(1);
for (auto & c : row) { for (auto & c : row)
r = lcm(r, denominator(c.coeff())); r = lcm(r, denominator(c.coeff()));
}
return r; return r;
} }
@ -130,8 +147,8 @@ namespace lp {
least_coeff_is_unique = true; least_coeff_is_unique = true;
least_coeff_index = j; least_coeff_index = j;
} }
else if (least_coeff_is_bounded && aux == m_least_coeff) { else if (aux == m_least_coeff) {
least_coeff_is_bounded = lra.column_is_bounded(j); least_coeff_is_bounded &= lra.column_is_bounded(j);
least_coeff_is_unique = false; least_coeff_is_unique = false;
} }
} }
@ -154,16 +171,8 @@ namespace lp {
fill_explanation_from_fixed_columns(A.m_rows[i]); fill_explanation_from_fixed_columns(A.m_rows[i]);
return false; return false;
} }
if (least_coeff_is_bounded && !m_least_coeff.is_one() && !ext_gcd_test(A.m_rows[i]))
if (m_least_coeff.is_one() && !least_coeff_is_bounded) {
SASSERT(gcds.is_one());
if (!least_coeff_is_unique)
return true;
return accumulate_parity(row, least_coeff_index);
}
if (least_coeff_is_bounded && !ext_gcd_test(A.m_rows[i]))
return false; return false;
if (!least_coeff_is_unique) if (!least_coeff_is_unique)
@ -278,28 +287,33 @@ namespace lp {
TRACE("gcd_test", tout << least_idx << " modulus: " << modulus << " consts: " << m_consts << " sign " << least_sign << " parity: " << parity << "\n";); TRACE("gcd_test", tout << least_idx << " modulus: " << modulus << " consts: " << m_consts << " sign " << least_sign << " parity: " << parity << "\n";);
SASSERT(0 <= parity && parity < modulus); SASSERT(0 <= parity && parity < modulus);
return insert_row_parity(least_idx, row, parity, modulus); return insert_parity(least_idx, row, parity, modulus);
} }
void int_gcd_test::reset_parities() { void int_gcd_test::reset_test() {
for (auto j : m_inserted_rows) for (auto j : m_inserted_vars)
m_row_parities[j].pop_back(); m_parities[j].pop_back();
m_inserted_rows.reset(); m_inserted_vars.reset();
m_visited_ts++;
if (m_visited_ts == 0) {
m_visited.reset();
m_visited_ts++;
}
} }
bool int_gcd_test::insert_row_parity(unsigned j, row_strip<mpq> const& r, mpq const& parity, mpq const& modulo) { bool int_gcd_test::insert_parity(unsigned j, row_strip<mpq> const& r, mpq const& offset, mpq const& modulo) {
m_row_parities.reserve(j + 1); m_parities.reserve(j + 1);
// incomplete parity check. // incomplete parity check.
for (auto const& p : m_row_parities[j]) { for (auto const& p : m_parities[j]) {
if (p.m_modulo == modulo && parity != p.m_parity) { if (p.m_modulo == modulo && offset != p.m_parity) {
fill_explanation_from_fixed_columns(r); fill_explanation_from_fixed_columns(r);
fill_explanation_from_fixed_columns(*p.m_row); fill_explanation_from_fixed_columns(*p.m_row);
return false; return false;
} }
} }
m_inserted_rows.push_back(j); m_inserted_vars.push_back(j);
m_row_parities[j].push_back(row_parity(parity, modulo, r)); m_parities[j].push_back(parity(offset, modulo, r));
return true; return true;
} }

27
src/math/lp/int_gcd_test.h
View file

@ -33,11 +33,11 @@ namespace lp {
class lar_solver; class lar_solver;
class int_gcd_test { class int_gcd_test {
struct row_parity { struct parity {
mpq m_parity; mpq m_parity;
mpq m_modulo; mpq m_modulo;
const row_strip<mpq>* m_row = nullptr; const row_strip<mpq>* m_row = nullptr;
row_parity(mpq const& p, mpq const& m, row_strip<mpq> const& r): parity(mpq const& p, mpq const& m, row_strip<mpq> const& r):
m_parity(p), m_parity(p),
m_modulo(m), m_modulo(m),
m_row(&r) m_row(&r)
@ -45,16 +45,21 @@ namespace lp {
}; };
class int_solver& lia; class int_solver& lia;
class lar_solver& lra; class lar_solver& lra;
unsigned m_next_gcd; unsigned m_next_gcd = 0;
unsigned m_delay; unsigned m_delay = 0;
mpq m_consts; mpq m_consts;
mpq m_least_coeff; mpq m_least_coeff;
mpq m_lcm_den; mpq m_lcm_den;
unsigned_vector m_inserted_rows; unsigned_vector m_inserted_vars;
vector<vector<row_parity>> m_row_parities; vector<vector<parity>> m_parities;
unsigned_vector m_visited;
unsigned m_visited_ts = 0;
void reset_parities(); bool is_visited(unsigned i) { return m_visited.get(i, 0) == m_visited_ts; }
bool insert_row_parity(unsigned j, row_strip<mpq> const& r, mpq const& parity, mpq const& modulo); void mark_visited(unsigned i) { m_visited.setx(i, m_visited_ts, 0); }
void reset_test();
bool insert_parity(unsigned j, row_strip<mpq> const& r, mpq const& parity, mpq const& modulo);
bool gcd_test(); bool gcd_test();
bool gcd_test_for_row(const static_matrix<mpq, numeric_pair<mpq>> & A, unsigned i); bool gcd_test_for_row(const static_matrix<mpq, numeric_pair<mpq>> & A, unsigned i);