Skip to content

Commit

Permalink
#4702
Browse files Browse the repository at this point in the history 
initial gcd test implementation for accumulated parity constraints
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Jun 1, 2021
1 parent 5127014 commit 2156c74
Show file tree
Hide file tree
Showing 3 changed files with 130 additions and 42 deletions.
143 changes: 107 additions & 36 deletions src/math/lp/int_gcd_test.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,8 @@ Module Name:
- Otherwise accumulate x = (c1 * lcm(b1,b2) / b2) + (c2 * lcm(b1,b2) / b1) mod lcm(b,b2)
and accumulate the rows from R1, R2
--*/

#include "math/lp/int_solver.h"
Expand All @@ -53,10 +55,7 @@ namespace lp {
int_gcd_test::int_gcd_test(int_solver& lia): lia(lia), lra(lia.lra), m_next_gcd(0), m_delay(0) {}

bool int_gcd_test::should_apply() {

if (!lia.settings().int_run_gcd_test())
return false;
return true;
return lia.settings().int_run_gcd_test();
}

lia_move int_gcd_test::operator()() {
Expand All @@ -76,6 +75,8 @@ namespace lp {
}

bool int_gcd_test::gcd_test() {
std::cout << "gcd-test\n";
reset_parities();
const auto & A = lra.A_r(); // getting the matrix
for (unsigned i = 0; i < A.row_count(); i++)
if (!gcd_test_for_row(A, i))
Expand All @@ -95,44 +96,50 @@ namespace lp {
auto const& row = A.m_rows[i];
unsigned basic_var = lra.r_basis()[i];

if (!lia.column_is_int(basic_var) || lia.get_value(basic_var).is_int())
if (!lia.column_is_int(basic_var))
return true;
mpq lcm_den = get_denominators_lcm(row);
mpq consts(0);
m_lcm_den = get_denominators_lcm(row);
m_consts = 0;
mpq gcds(0);
mpq least_coeff(0);
bool least_coeff_is_bounded = false;
unsigned j;
m_least_coeff = 0;
bool least_coeff_is_bounded = false;
bool least_coeff_is_unique = false;
unsigned least_coeff_index = 0;
for (auto &c : A.m_rows[i]) {
j = c.var();
unsigned j = c.var();
const mpq& a = c.coeff();
if (lra.column_is_fixed(j)) {
mpq aux = lcm_den * a;
consts += aux * lra.column_lower_bound(j).x;
mpq aux = m_lcm_den * a;
m_consts += aux * lra.column_lower_bound(j).x;
}
else if (lra.column_is_real(j)) {
return true;
}
else if (gcds.is_zero()) {
gcds = abs(lcm_den * a);
least_coeff = gcds;
gcds = abs(m_lcm_den * a);
m_least_coeff = gcds;
least_coeff_is_bounded = lra.column_is_bounded(j);
least_coeff_is_unique = true;
least_coeff_index = j;
}
else {
mpq aux = abs(lcm_den * a);
mpq aux = abs(m_lcm_den * a);
gcds = gcd(gcds, aux);
if (aux < least_coeff) {
least_coeff = aux;
if (aux < m_least_coeff) {
m_least_coeff = aux;
least_coeff_is_bounded = lra.column_is_bounded(j);
least_coeff_is_unique = true;
least_coeff_index = j;
}
else if (least_coeff_is_bounded && aux == least_coeff) {
else if (least_coeff_is_bounded && aux == m_least_coeff) {
least_coeff_is_bounded = lra.column_is_bounded(j);
least_coeff_is_unique = false;
}
}
SASSERT(gcds.is_int());
SASSERT(least_coeff.is_int());
SASSERT(m_least_coeff.is_int());
TRACE("gcd_test_bug", tout << "coeff: " << a << ", gcds: " << gcds
<< " least_coeff: " << least_coeff << " consts: " << consts << "\n";);
<< " least_coeff: " << m_least_coeff << " consts: " << m_consts << "\n";);

}

Expand All @@ -143,31 +150,36 @@ namespace lp {
return true;
}

if (!(consts / gcds).is_int()) {
if (!(m_consts / gcds).is_int()) {
TRACE("gcd_test", tout << "row failed the GCD test:\n"; lia.display_row_info(tout, i););
fill_explanation_from_fixed_columns(A.m_rows[i]);
return false;
}

if (!least_coeff_is_unique)
lia.display_row(std::cout << "non-unique ", row);

if (least_coeff.is_one() && !least_coeff_is_bounded) {
if (m_least_coeff.is_one() && !least_coeff_is_bounded) {
SASSERT(gcds.is_one());
return true;
if (!least_coeff_is_unique)
return true;
return accumulate_parity(row, least_coeff_index);
}

if (least_coeff_is_bounded) {
return ext_gcd_test(A.m_rows[i], least_coeff, lcm_den, consts);
}
return true;
if (least_coeff_is_bounded && !ext_gcd_test(A.m_rows[i]))
return false;

if (!least_coeff_is_unique)
return true;

return accumulate_parity(row, least_coeff_index);
}

bool int_gcd_test::ext_gcd_test(const row_strip<mpq> & row,
mpq const & least_coeff,
mpq const & lcm_den,
mpq const & consts) {
bool int_gcd_test::ext_gcd_test(const row_strip<mpq> & row) {
TRACE("ext_gcd_test", tout << "row = "; lra.print_row(row, tout););
mpq gcds(0);
mpq l(consts);
mpq u(consts);
mpq l(m_consts);
mpq u(m_consts);

mpq a;
unsigned j;
Expand All @@ -178,10 +190,10 @@ namespace lp {
if (lra.column_is_fixed(j))
continue;
SASSERT(!lra.column_is_real(j));
mpq ncoeff = lcm_den * a;
mpq ncoeff = m_lcm_den * a;
SASSERT(ncoeff.is_int());
mpq abs_ncoeff = abs(ncoeff);
if (abs_ncoeff == least_coeff) {
if (abs_ncoeff == m_least_coeff) {
SASSERT(lra.column_is_bounded(j));
if (ncoeff.is_pos()) {
// l += ncoeff * lra.column_lower_bound(j).x;
Expand Down Expand Up @@ -235,4 +247,63 @@ namespace lp {
lia.m_ex->push_back(uc);
}

bool int_gcd_test::accumulate_parity(const row_strip<mpq> & row, unsigned least_idx) {

This comment has been minimized.

Sign in to view

Copy link
@NikolajBjorner

NikolajBjorner Jun 2, 2021

Author Contributor

@levnach - could you review the new functionality?

// remove this line to enable new functionality.
return true;

mpq modulus(0);
bool least_sign = false;
for (const auto & c : row) {
unsigned j = c.var();
const mpq& a = c.coeff();
if (j == least_idx)
least_sign = a.is_neg();
else if (!lra.column_is_fixed(j)) {
mpq aux = abs(m_lcm_den * a);
if (gcd(m_least_coeff, aux) != m_least_coeff)
return true;
modulus = modulus == 0 ? aux : gcd(modulus, aux);
if (modulus.is_one())
return true;
}
}
modulus /= m_least_coeff;
if (modulus == 0)
return true;
SASSERT(modulus.is_int());
mpq parity = m_consts / m_least_coeff;
if (!parity.is_int())
return true;
parity = mod(parity, modulus);
if (!least_sign && parity != 0)
parity = modulus - parity;
TRACE("gcd_test", tout << least_idx << " modulus: " << modulus << " consts: " << m_consts << " sign " << least_sign << " parity: " << parity << "\n";);

SASSERT(0 <= parity && parity < modulus);
return insert_row_parity(least_idx, row, parity, modulus);
}

void int_gcd_test::reset_parities() {
for (auto j : m_inserted_rows)
m_row_parities[j].pop_back();
m_inserted_rows.reset();
}

bool int_gcd_test::insert_row_parity(unsigned j, row_strip<mpq> const& r, mpq const& parity, mpq const& modulo) {
m_row_parities.reserve(j + 1);

// incomplete parity check.
for (auto const& p : m_row_parities[j]) {
if (p.m_modulo == modulo && parity != p.m_parity) {
fill_explanation_from_fixed_columns(r);
fill_explanation_from_fixed_columns(*p.m_row);
return false;
}
}
m_inserted_rows.push_back(j);
m_row_parities[j].push_back(row_parity(parity, modulo, r));
return true;
}

}
25 changes: 21 additions & 4 deletions src/math/lp/int_gcd_test.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,19 +32,36 @@ namespace lp {
class int_solver;
class lar_solver;
class int_gcd_test {

struct row_parity {
mpq m_parity;
mpq m_modulo;
const row_strip<mpq>* m_row = nullptr;
row_parity(mpq const& p, mpq const& m, row_strip<mpq> const& r):
m_parity(p),
m_modulo(m),
m_row(&r)
{}
};
class int_solver& lia;
class lar_solver& lra;
unsigned m_next_gcd;
unsigned m_delay;
mpq m_consts;
mpq m_least_coeff;
mpq m_lcm_den;
unsigned_vector m_inserted_rows;
vector<vector<row_parity>> m_row_parities;

void reset_parities();
bool insert_row_parity(unsigned j, row_strip<mpq> const& r, mpq const& parity, mpq const& modulo);

bool gcd_test();
bool gcd_test_for_row(const static_matrix<mpq, numeric_pair<mpq>> & A, unsigned i);
bool ext_gcd_test(const row_strip<mpq> & row,
mpq const & least_coeff,
mpq const & lcm_den,
mpq const & consts);
bool ext_gcd_test(const row_strip<mpq> & row);
void fill_explanation_from_fixed_columns(const row_strip<mpq> & row);
void add_to_explanation_from_fixed_or_boxed_column(unsigned j);
bool accumulate_parity(const row_strip<mpq> & row, unsigned least_coeff_index);
public:
int_gcd_test(int_solver& lia);
lia_move operator()();
Expand Down
4 changes: 2 additions & 2 deletions src/smt/theory_lra.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1541,8 +1541,8 @@ class theory_lra::imp {

switch (is_sat) {
case l_true:
TRACE("arith", /*display(tout);*/
ctx().display(tout);
TRACE("arith", display(tout);
/* ctx().display(tout);*/
);

switch (check_lia()) {
Expand Down

0 comments on commit 2156c74

Please sign in to comment.