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

a version where cut variables are excluded from recursive branch and cuts

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-03-03 07:43:37 -08:00
parent 7eb401b891
commit 9eb19b56c7
4 changed files with 26 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/math/lp/gomory.cpp
View file

@ -323,7 +323,7 @@ public:
m_dep = nullptr;
for (auto c : *m_ex)
m_dep = lia.lra.join_deps(lia.lra.dep_manager().mk_leaf(c.ci()), m_dep);
m_dep = lia.lra.join_deps(lia.lra.dep_manager().mk_leaf(c.ci()), m_dep);
TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout);
lia.lra.display(tout));
@ -354,6 +354,9 @@ public:
// 1) c is integral and x integral varible with an integral value
// 2) the value of x is at a bound and has no infinitesimals.
if (lia.is_cut_var(k))
return false;
unsigned j;
for (const auto & p : row) {
@ -491,6 +494,7 @@ public:
};
auto add_cut = [&](const lar_term& t, const mpq& k, u_dependency * dep) {
lp::lpvar j = lra.add_term(t.coeffs_as_vector(), UINT_MAX);
lia.add_cut_var(j);
lra.update_column_type_and_bound(j, lp::lconstraint_kind::GE, k, dep);
};
auto _check_feasible = [&](void) {

2
src/math/lp/int_branch.cpp
View file

@ -74,6 +74,8 @@ int int_branch::find_inf_int_base_column() {
j = lra.r_basis()[k];
if (!lia.column_is_int_inf(j))
continue;
if (lia.is_cut_var(j))
continue;
usage = lra.usage_in_terms(j);
if (lia.is_boxed(j) && (range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage)) <= small_value) {
result = j;

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

@ -584,6 +584,22 @@ namespace lp {
return lra.column_count();
}
void int_solver::add_cut_var(unsigned j) {
struct insert : public trail {
uint_set& s;
unsigned j;
insert(uint_set& s, unsigned j): s(s), j(j) {}
void undo() override { s.remove(j); }
};
m_cut_vars.insert(j);
lra.trail().push(insert(m_cut_vars, j));
}
bool int_solver::is_cut_var(unsigned j) const {
return m_cut_vars.contains(j);
}
static void set_lower(impq & l, bool & inf_l, impq const & v ) {
if (inf_l || v > l) {

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

@ -46,6 +46,7 @@ class int_solver {
lar_core_solver& lrac;
imp* m_imp;
vector<equality> m_equalities;
uint_set m_cut_vars;
bool get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m);
bool is_boxed(unsigned j) const;
bool is_free(unsigned j) const;
@ -86,6 +87,8 @@ public:
u_dependency* column_upper_bound_constraint(unsigned j) const;
u_dependency* column_lower_bound_constraint(unsigned j) const;
bool current_solution_is_inf_on_cut() const;
void add_cut_var(unsigned j);
bool is_cut_var(unsigned j) const;
bool shift_var(unsigned j, unsigned range);
std::ostream& display_row_info(std::ostream & out, unsigned row_index) const;