mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +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:37:43 -07:00
parent 45adfc6a66
commit ab3b387076
2 changed files with 15 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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;

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

@ -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)
{}