mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

prepare for calling diophantine equations

Browse source
This commit is contained in:
Lev Nachmanson 2024-08-13 13:20:45 -10:00 committed by Lev Nachmanson
parent 097a25ebfe
commit 3d6cc64e2e
3 changed files with 112 additions and 115 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -11,14 +11,53 @@
#include "math/lp/int_cube.h"
namespace lp {
bool get_patching_deltas(const rational& x, const rational& alpha,
rational& delta_plus, rational& delta_minus);
class imp {
int_solver& lia;
lar_solver& lra;
lar_core_solver& lrac;
public:
imp(int_solver& lia): lia(lia), lra(lia.lra), lrac(lia.lrac) {}
bool should_apply() const { return true; }
void patch_basic_column(unsigned v) {
SASSERT(!lia.is_fixed(v));
for (auto const& c : lra.basic2row(v))
if (patch_basic_column_on_row_cell(v, c))
return;
}
bool try_patch_column(unsigned v, unsigned j, mpq const& delta) {
const auto & A = lra.A_r();
if (delta < 0) {
if (lia.has_lower(j) && lia.get_value(j) + impq(delta) < lra.get_lower_bound(j))
return false;
}
else {
if (lia.has_upper(j) && lia.get_value(j) + impq(delta) > lra.get_upper_bound(j))
return false;
}
for (auto const& c : A.column(j)) {
unsigned row_index = c.var();
unsigned bj = lrac.m_r_basis[row_index];
auto old_val = lia.get_value(bj);
auto new_val = old_val - impq(c.coeff()*delta);
if (lia.has_lower(bj) && new_val < lra.get_lower_bound(bj))
return false;
if (lia.has_upper(bj) && new_val > lra.get_upper_bound(bj))
return false;
if (old_val.is_int() && !new_val.is_int()){
return false; // do not waste resources on this case
}
// if bj == v, then, because we are patching the lra.get_value(v),
// we just need to assert that the lra.get_value(v) would be integral.
lp_assert(bj != v || lra.from_model_in_impq_to_mpq(new_val).is_int());
}
int_solver::patcher::patcher(int_solver& lia):
lia(lia),
lra(lia.lra),
lrac(lia.lrac)
{}
lra.set_value_for_nbasic_column(j, lia.get_value(j) + impq(delta));
return true;
}
unsigned int_solver::patcher::count_non_int() {
unsigned count_non_int() {
unsigned non_int = 0;
for (auto j : lra.r_basis())
if (lra.column_is_int(j) && !lra.column_value_is_int(j))
@ -26,7 +65,30 @@ namespace lp {
return non_int;
}
lia_move int_solver::patcher::patch_basic_columns() {
bool patch_basic_column_on_row_cell(unsigned v, row_cell<mpq> const& c) {
if (v == c.var())
return false;
if (!lra.column_is_int(c.var())) // could use real to patch integer
return false;
if (c.coeff().is_int())
return false;
mpq a = fractional_part(c.coeff());
mpq r = fractional_part(lra.get_value(v));
lp_assert(0 < r && r < 1);
lp_assert(0 < a && a < 1);
mpq delta_plus, delta_minus;
if (!get_patching_deltas(r, a, delta_plus, delta_minus))
return false;
if (lia.random() % 2)
return try_patch_column(v, c.var(), delta_plus) ||
try_patch_column(v, c.var(), delta_minus);
else
return try_patch_column(v, c.var(), delta_minus) ||
try_patch_column(v, c.var(), delta_plus);
}
lia_move patch_basic_columns() {
lia.settings().stats().m_patches++;
lra.remove_fixed_vars_from_base();
lp_assert(lia.is_feasible());
@ -40,6 +102,16 @@ namespace lp {
return lia_move::undef;
}
bool should_solve_dioph_eq() { return lia.settings().dioph_eq(); }
lia_move solve_dioph_eq() {
return lia_move::undef;
}
};
// clang-format on
/**
* \brief find integral and minimal, in the absolute values, deltas such that x - alpha*delta is integral too.
@ -80,82 +152,22 @@ namespace lp {
return true;
}
/**
* \brief try to patch the basic column v
*/
bool int_solver::patcher::patch_basic_column_on_row_cell(unsigned v, row_cell<mpq> const& c) {
if (v == c.var())
return false;
if (!lra.column_is_int(c.var())) // could use real to patch integer
return false;
if (c.coeff().is_int())
return false;
mpq a = fractional_part(c.coeff());
mpq r = fractional_part(lra.get_value(v));
lp_assert(0 < r && r < 1);
lp_assert(0 < a && a < 1);
mpq delta_plus, delta_minus;
if (!get_patching_deltas(r, a, delta_plus, delta_minus))
return false;
if (lia.random() % 2)
return try_patch_column(v, c.var(), delta_plus) ||
try_patch_column(v, c.var(), delta_minus);
else
return try_patch_column(v, c.var(), delta_minus) ||
try_patch_column(v, c.var(), delta_plus);
}
bool int_solver::patcher::try_patch_column(unsigned v, unsigned j, mpq const& delta) {
const auto & A = lra.A_r();
if (delta < 0) {
if (lia.has_lower(j) && lia.get_value(j) + impq(delta) < lra.get_lower_bound(j))
return false;
}
else {
if (lia.has_upper(j) && lia.get_value(j) + impq(delta) > lra.get_upper_bound(j))
return false;
}
for (auto const& c : A.column(j)) {
unsigned row_index = c.var();
unsigned bj = lrac.m_r_basis[row_index];
auto old_val = lia.get_value(bj);
auto new_val = old_val - impq(c.coeff()*delta);
if (lia.has_lower(bj) && new_val < lra.get_lower_bound(bj))
return false;
if (lia.has_upper(bj) && new_val > lra.get_upper_bound(bj))
return false;
if (old_val.is_int() && !new_val.is_int()){
return false; // do not waste resources on this case
}
// if bj == v, then, because we are patching the lra.get_value(v),
// we just need to assert that the lra.get_value(v) would be integral.
lp_assert(bj != v || lra.from_model_in_impq_to_mpq(new_val).is_int());
}
lra.set_value_for_nbasic_column(j, lia.get_value(j) + impq(delta));
return true;
}
void int_solver::patcher::patch_basic_column(unsigned v) {
SASSERT(!lia.is_fixed(v));
for (auto const& c : lra.basic2row(v))
if (patch_basic_column_on_row_cell(v, c))
return;
}
int_solver::int_solver(lar_solver& lar_slv) :
lra(lar_slv),
lrac(lra.m_mpq_lar_core_solver),
m_gcd(*this),
m_patcher(*this),
m_number_of_calls(0),
m_hnf_cutter(*this),
m_hnf_cut_period(settings().hnf_cut_period()) {
m_imp = alloc(imp, *this);
lra.set_int_solver(this);
}
int_solver::~int_solver() { dealloc(m_imp); }
// this will allow to enable and disable tracking of the pivot rows
struct check_return_helper {
lar_solver& lra;
@ -193,9 +205,9 @@ namespace lp {
return lia_move::undef;
++m_number_of_calls;
if (r == lia_move::undef && m_patcher.should_apply()) r = m_patcher();
if (r == lia_move::undef && m_imp->should_apply()) r = m_imp->patch_basic_columns();
if (r == lia_move::undef && should_find_cube()) r = int_cube(*this)();
// if (r == lia_move::undef && should_solve_dioph_eq()) r = solve_dioph_eq();
if (r == lia_move::undef && m_imp->should_solve_dioph_eq()) r = m_imp->solve_dioph_eq();
if (r == lia_move::undef) lra.move_non_basic_columns_to_bounds();
if (r == lia_move::undef && should_hnf_cut()) r = hnf_cut();

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

@ -31,7 +31,7 @@ Revision History:
namespace lp {
class lar_solver;
class lar_core_solver;
class patcher;
class int_solver {
friend struct create_cut;
friend class gomory;
@ -39,27 +39,12 @@ class int_solver {
friend class int_branch;
friend class int_gcd_test;
friend class hnf_cutter;
class patcher {
int_solver& lia;
lar_solver& lra;
lar_core_solver& lrac;
public:
patcher(int_solver& lia);
bool should_apply() const { return true; }
lia_move operator()() { return patch_basic_columns(); }
void patch_basic_column(unsigned j);
bool try_patch_column(unsigned v, unsigned j, mpq const& delta);
unsigned count_non_int();
private:
bool patch_basic_column_on_row_cell(unsigned v, row_cell<mpq> const& c);
lia_move patch_basic_columns();
};
friend class imp;
lar_solver& lra;
lar_core_solver& lrac;
int_gcd_test m_gcd;
patcher m_patcher;
imp *m_imp;
unsigned m_number_of_calls;
lar_term m_t; // the term to return in the cut
mpq m_k; // the right side of the cut
@ -72,7 +57,7 @@ class int_solver {
vector<equality> m_equalities;
public:
int_solver(lar_solver& lp);
~int_solver();
// main function to check that the solution provided by lar_solver is valid for integral values,
// or provide a way of how it can be adjusted.
lia_move check(explanation *);

2
src/math/lp/lp_settings.h
View file

@ -236,7 +236,7 @@ public:
void set_hnf_cut_period(unsigned period) { m_hnf_cut_period = period; }
unsigned random_next() { return m_rand(); }
unsigned random_next(unsigned u ) { return m_rand(u); }
bool dioph_eq() { return m_dioph_eq; }
void set_random_seed(unsigned s) { m_rand.set_seed(s); }
bool bound_progation() const {