From ab3b3870762d89727c146091ce1333040fd38ac0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 1 Jun 2021 20:37:43 -0700
Subject: [PATCH] na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/math/lp/int_gcd_test.cpp | 22 +++++++++++++---------
src/math/lp/int_gcd_test.h | 4 ++--
2 files changed, 15 insertions(+), 11 deletions(-)
diff --git a/src/math/lp/int_gcd_test.cpp b/src/math/lp/int_gcd_test.cpp
index b5b4b9547..55dedf151 100644
--- a/src/math/lp/int_gcd_test.cpp
+++ b/src/math/lp/int_gcd_test.cpp
@@ -278,16 +278,16 @@ namespace lp {
if (modulus == 0)
return true;
SASSERT(modulus.is_int());
- mpq parity = m_consts / m_least_coeff;
- if (!parity.is_int())
+ mpq offset = m_consts / m_least_coeff;
+ if (!offset.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";);
+ offset = mod(offset, modulus);
+ if (!least_sign && offset != 0)
+ offset = modulus - offset;
+ TRACE("gcd_test", tout << least_idx << " modulus: " << modulus << " consts: " << m_consts << " sign " << least_sign << " offset: " << offset << "\n";);
- SASSERT(0 <= parity && parity < modulus);
- return insert_parity(least_idx, row, parity, modulus);
+ SASSERT(0 <= offset && offset < modulus);
+ return insert_parity(least_idx, row, offset, modulus);
}
void int_gcd_test::reset_test() {
@@ -306,7 +306,11 @@ namespace lp {
// incomplete parity check.
for (auto const& p : m_parities[j]) {
- if (p.m_modulo == modulo && offset != p.m_parity) {
+ if (p.m_modulo != modulo)
+ continue;
+ if (p.m_offset == offset)
+ return true;
+ else {
fill_explanation_from_fixed_columns(r);
fill_explanation_from_fixed_columns(*p.m_row);
return false;
diff --git a/src/math/lp/int_gcd_test.h b/src/math/lp/int_gcd_test.h
index 7aa4a1151..28ac2f7b3 100644
--- a/src/math/lp/int_gcd_test.h
+++ b/src/math/lp/int_gcd_test.h
@@ -34,11 +34,11 @@ namespace lp {
class int_gcd_test {
struct parity {
- mpq m_parity;
+ mpq m_offset;
mpq m_modulo;
const row_strip<mpq>* m_row = nullptr;
parity(mpq const& p, mpq const& m, row_strip<mpq> const& r):
- m_parity(p),
+ m_offset(p),
m_modulo(m),
m_row(&r)
{}