mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 11:22:04 +00:00
Code Activity

new (and fixed) patcher

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-06-08 14:37:42 -07:00
parent e7065e3984
commit 37ec667102
3 changed files with 22 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

35
src/math/lp/int_solver.cpp
View file

@ -103,37 +103,42 @@ namespace lp {
mpq r = fractional_part(lra.get_value(v)); mpq r = fractional_part(lra.get_value(v));
SASSERT(0 < a && a < 1); SASSERT(0 < a && a < 1);
SASSERT(0 < r && r < 1); SASSERT(0 < r && r < 1);
if (!divides(denominator(a), denominator(r))) if (!divides(denominator(r), denominator(a)))
return false; return false;
// stronger filter for now: // stronger filter for now:
if (denominator(a) != denominator(r)) // if a = r = 1/2 then both patch directions are attempted.
if (a == r || a == 1 - r) {
if (try_patch_column(v, c.var(), mpq(1)))
return true;
if (try_patch_column(v, c.var(), mpq(-1)))
return true;
return false; return false;
if (a == r) {
if (try_patch_column(c.var(), mpq(a.is_pos() ? 1 : -1)))
return true;
}
if (a == 1 - r) {
if (try_patch_column(c.var(), mpq(a.is_pos() ? -1 : 1)))
return true;
} }
rational x, y; rational x, y;
rational g = gcd(numerator(a), denominator(a), x, y); rational g = gcd(numerator(a), denominator(a), x, y);
rational scale = denominator(a)/denominator(r);
VERIFY(scale.is_int() && scale > 0);
// g = numerator(a)*x + denominator(a)*y // g = numerator(a)*x + denominator(a)*y
x = abs(x); VERIFY(g == numerator(a)*x + denominator(a)*y);
if (divides(g, numerator(r))) { if (divides(g, numerator(r))) {
auto xs = a.is_pos() ? x : -x; if (try_patch_column(v, c.var(), scale*x*(numerator(r)/g)))
if (try_patch_column(c.var(), xs*(numerator(r)/g)))
return true; return true;
if (try_patch_column(v, c.var(), -scale*x*(numerator(r)/g)))
return true;
return false;
} }
if (divides(g, numerator(1 - r))) { if (divides(g, numerator(1 - r))) {
auto xs = a.is_pos() ? -x : x; if (try_patch_column(v, c.var(), scale*x*(numerator(1 - r)/g)))
if (try_patch_column(c.var(), xs*(numerator(r)/g)))
return true; return true;
if (try_patch_column(v, c.var(), -scale*x*(numerator(1 - r)/g)))
return true;
return false;
} }
return false; return false;
} }
bool int_solver::patcher::try_patch_column(unsigned j, mpq const& delta) { bool int_solver::patcher::try_patch_column(unsigned v, unsigned j, mpq const& delta) {
const auto & A = lra.A_r(); const auto & A = lra.A_r();
unsigned make_count = 0, break_count = 0; unsigned make_count = 0, break_count = 0;
if (delta < 0) { if (delta < 0) {

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

@ -51,11 +51,11 @@ class int_solver {
public: public:
patcher(int_solver& lia); patcher(int_solver& lia);
bool should_apply() const { return true; } bool should_apply() const { return true; }
lia_move operator()() { return patch_nbasic_columns(); } lia_move operator()() { return patch_basic_columns(); }
void patch_nbasic_column(unsigned j); void patch_nbasic_column(unsigned j);
bool patch_basic_column(unsigned v, row_cell<mpq> const& c); bool patch_basic_column(unsigned v, row_cell<mpq> const& c);
void patch_basic_column(unsigned j); void patch_basic_column(unsigned j);
bool try_patch_column(unsigned j, mpq const& delta); bool try_patch_column(unsigned v, unsigned j, mpq const& delta);
unsigned count_non_int(); unsigned count_non_int();
private: private:
void remove_fixed_vars_from_base(); void remove_fixed_vars_from_base();

3
src/smt/smt_context_pp.cpp
View file

@ -510,9 +510,6 @@ namespace smt {
#else #else
strm << "lemma_" << (++m_lemma_id) << ".smt2"; strm << "lemma_" << (++m_lemma_id) << ".smt2";
#endif #endif
if (m_lemma_id == 1303) {
verbose_stream() << "lemma\n";
}
return strm.str(); return strm.str();
} }