mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-12 14:10:54 +00:00
Code Activity

extract gomory cut functionality in one method

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

work on hnf

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

work in hnf

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

work in hnf

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

work in hnf

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

work in hnf

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

work on hnf

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

work on hnf

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

prepare calculate U in hnf

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

naive algorithm for HNF and m <= n

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

naive algorithm for HNF

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

introduces reverse matrix into Hermite Normal Form calculation

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

work on more efficient hnf

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

work on hnf

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

use smarter templates in lu.h

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

the new lu scheme compiles

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

simple test passes with the modified lu

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

fix the build on windows

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

playing with the example from cutting the mix

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

work on hnf, add extended_gcd_minimal_uv()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

work on extended_gcd_minimal_uv

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

work on hnf, add extended_gcd_minimal_uv()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

more tests and bug fixes in hnf

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

work on hnf modulo version

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

work on hnf modulo version, more tests pass

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

a rough version of hnf passed the tests

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

fix build in release

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

fixes in determinant calculations

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

work on hnf

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

work on hnf

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

work on hnf

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

work on hnf

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

create a stub for hnf_cuts

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

create a stub for hnf_cuts

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

create a stub for hnf_cuts

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

general_matrix etc.

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

general_matrix etc.

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

rename cut_solver to chase_cut_solver

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

rename cut_solver to chase_cut_solver

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

hnf_cutter

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-04-20 11:24:20 -07:00
parent c04bcb411d
commit 3b5337823a
35 changed files with 2178 additions and 760 deletions
Download patch file Download diff file Expand all files Collapse all files

171
src/util/lp/int_solver.cpp
View file

@ -5,7 +5,7 @@
#include "util/lp/int_solver.h"
#include "util/lp/lar_solver.h"
#include "util/lp/cut_solver.h"
#include "util/lp/chase_cut_solver.h"
#include "util/lp/lp_utils.h"
#include <utility>
namespace lp {
@ -414,7 +414,7 @@ unsigned int_solver::row_of_basic_column(unsigned j) const {
// }
typedef cut_solver::monomial mono;
typedef chase_cut_solver::monomial mono;
// it produces an inequality coeff*x <= rs
template <typename T>
@ -456,33 +456,33 @@ struct pivoted_rows_tracking_control {
}
};
void int_solver::copy_explanations_from_cut_solver() {
void int_solver::copy_explanations_from_chase_cut_solver() {
TRACE("propagate_and_backjump_step_int",
for (unsigned j: m_cut_solver.m_explanation)
for (unsigned j: m_chase_cut_solver.m_explanation)
m_lar_solver->print_constraint(m_lar_solver->constraints()[j], tout););
for (unsigned j : m_cut_solver.m_explanation) {
for (unsigned j : m_chase_cut_solver.m_explanation) {
m_ex->push_justification(j);
}
m_cut_solver.m_explanation.clear();
m_chase_cut_solver.m_explanation.clear();
}
void int_solver::copy_values_from_cut_solver() {
for (unsigned j = 0; j < m_lar_solver->A_r().column_count() && j < m_cut_solver.number_of_vars(); j++) {
if (!m_cut_solver.var_is_active(j))
void int_solver::copy_values_from_chase_cut_solver() {
for (unsigned j = 0; j < m_lar_solver->A_r().column_count() && j < m_chase_cut_solver.number_of_vars(); j++) {
if (!m_chase_cut_solver.var_is_active(j))
continue;
if (!is_int(j)) {
continue;
}
m_lar_solver->m_mpq_lar_core_solver.m_r_x[j] = m_cut_solver.var_value(j);
m_lar_solver->m_mpq_lar_core_solver.m_r_x[j] = m_chase_cut_solver.var_value(j);
lp_assert(m_lar_solver->column_value_is_int(j));
}
}
void int_solver::catch_up_in_adding_constraints_to_cut_solver() {
lp_assert(m_cut_solver.number_of_asserts() <= m_lar_solver->constraints().size());
for (unsigned j = m_cut_solver.number_of_asserts(); j < m_lar_solver->constraints().size(); j++) {
add_constraint_to_cut_solver(j, m_lar_solver->constraints()[j]);
void int_solver::catch_up_in_adding_constraints_to_chase_cut_solver() {
lp_assert(m_chase_cut_solver.number_of_asserts() <= m_lar_solver->constraints().size());
for (unsigned j = m_chase_cut_solver.number_of_asserts(); j < m_lar_solver->constraints().size(); j++) {
add_constraint_to_chase_cut_solver(j, m_lar_solver->constraints()[j]);
}
}
@ -536,7 +536,7 @@ bool int_solver::tighten_terms_for_cube() {
}
bool int_solver::find_cube() {
if (m_branch_cut_counter % settings().m_int_find_cube_period != 0)
if (m_branch_cut_counter % settings().m_int_find_cube_period != 0)
return false;
settings().st().m_cube_calls++;
@ -557,13 +557,13 @@ bool int_solver::find_cube() {
m_lar_solver->pop();
move_non_basic_columns_to_bounds();
find_feasible_solution();
lp_assert(m_cut_solver.cancel() || is_feasible());
lp_assert(m_chase_cut_solver.cancel() || is_feasible());
// it can happen that we found an integer solution here
return !m_lar_solver->r_basis_has_inf_int();
}
m_lar_solver->pop();
m_lar_solver->round_to_integer_solution();
lp_assert(m_cut_solver.cancel() || is_feasible());
lp_assert(m_chase_cut_solver.cancel() || is_feasible());
return true;
}
@ -583,29 +583,29 @@ lia_move int_solver::run_gcd_test() {
return lia_move::undef;
}
lia_move int_solver::call_cut_solver() {
if ((m_branch_cut_counter) % settings().m_int_cut_solver_period != 0 || !all_columns_are_bounded())
lia_move int_solver::call_chase_cut_solver() {
if ((m_branch_cut_counter) % settings().m_int_chase_cut_solver_period != 0 || !all_columns_are_bounded())
return lia_move::undef;
TRACE("check_main_int", tout<<"cut_solver";);
catch_up_in_adding_constraints_to_cut_solver();
auto check_res = m_cut_solver.check();
settings().st().m_cut_solver_calls++;
TRACE("check_main_int", tout<<"chase_cut_solver";);
catch_up_in_adding_constraints_to_chase_cut_solver();
auto check_res = m_chase_cut_solver.check();
settings().st().m_chase_cut_solver_calls++;
switch (check_res) {
case cut_solver::lbool::l_false:
copy_explanations_from_cut_solver();
settings().st().m_cut_solver_false++;
case chase_cut_solver::lbool::l_false:
copy_explanations_from_chase_cut_solver();
settings().st().m_chase_cut_solver_false++;
return lia_move::conflict;
case cut_solver::lbool::l_true:
settings().st().m_cut_solver_true++;
copy_values_from_cut_solver();
case chase_cut_solver::lbool::l_true:
settings().st().m_chase_cut_solver_true++;
copy_values_from_chase_cut_solver();
lp_assert(m_lar_solver->all_constraints_hold());
return lia_move::sat;
case cut_solver::lbool::l_undef:
settings().st().m_cut_solver_undef++;
if (m_cut_solver.try_getting_cut(*m_t, *m_k, m_lar_solver->m_mpq_lar_core_solver.m_r_x)) {
case chase_cut_solver::lbool::l_undef:
settings().st().m_chase_cut_solver_undef++;
if (m_chase_cut_solver.try_getting_cut(*m_t, *m_k, m_lar_solver->m_mpq_lar_core_solver.m_r_x)) {
m_lar_solver->subs_term_columns(*m_t);
TRACE("cut_solver_cuts",
tout<<"precut from cut_solver:"; m_lar_solver->print_term(*m_t, tout); tout << " <= " << *m_k << std::endl;);
TRACE("chase_cut_solver_cuts",
tout<<"precut from chase_cut_solver:"; m_lar_solver->print_term(*m_t, tout); tout << " <= " << *m_k << std::endl;);
return lia_move::cut;
}
@ -614,6 +614,63 @@ lia_move int_solver::call_cut_solver() {
}
}
lia_move int_solver::gomory_cut() {
TRACE("check_main_int", tout << "gomory";);
if (move_non_basic_columns_to_bounds()) {
lp_status st = m_lar_solver->find_feasible_solution();
if (st != lp_status::FEASIBLE && st != lp_status::OPTIMAL) {
TRACE("arith_int", tout << "give_up\n";);
return lia_move::undef;
}
}
int j = find_inf_int_base_column();
if (j == -1) {
j = find_inf_int_nbasis_column();
return j == -1? lia_move::sat : create_branch_on_column(j);
}
lia_move r = proceed_with_gomory_cut(j);
if (r != lia_move::undef)
return r;
return create_branch_on_column(j);
}
void int_solver::try_add_term_to_A_for_hnf(unsigned i) {
mpq rs;
const lar_term* t = m_lar_solver->terms()[i];
for (const auto & p : *t) {
if (!is_int(p.var()))
return; // todo : the mix case!
}
if (!m_lar_solver->get_equality_for_term_on_corrent_x(i, rs))
return;
m_hnf_cutter.add_term_to_A_for_hnf(t, rs);
}
bool int_solver::hnf_matrix_is_empty() const { return true; }
bool int_solver::prepare_matrix_A_for_hnf_cut() {
m_hnf_cutter.clear();
for (unsigned i = 0; i < m_lar_solver->terms().size(); i++)
try_add_term_to_A_for_hnf(i);
m_hnf_cutter.print(std::cout);
return ! hnf_matrix_is_empty();
}
lia_move int_solver::make_hnf_cut() {
if( !prepare_matrix_A_for_hnf_cut())
return lia_move::undef;
return lia_move::undef;
}
lia_move int_solver::hnf_cut() {
if ((m_branch_cut_counter) % settings().m_hnf_cut_period == 0) {
return make_hnf_cut();
}
return lia_move::undef;
}
lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex, bool & upper) {
if (!has_inf_int())
return lia_move::sat;
@ -634,35 +691,17 @@ lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex, bool & upper) {
return lia_move::sat;
}
lia_move r = call_cut_solver();
lia_move r = call_chase_cut_solver();
if (r != lia_move::undef)
return r;
r = hnf_cut();
if (r != lia_move::undef)
return r;
if ((m_branch_cut_counter) % settings().m_int_gomory_cut_period == 0) {
TRACE("check_main_int", tout << "gomory";);
if (move_non_basic_columns_to_bounds()) {
lp_status st = m_lar_solver->find_feasible_solution();
lp_assert(non_basic_columns_are_at_bounds());
if (st != lp_status::FEASIBLE && st != lp_status::OPTIMAL) {
TRACE("arith_int", tout << "give_up\n";);
return lia_move::undef;
}
}
int j = find_inf_int_base_column();
if (j == -1) {
j = find_inf_int_nbasis_column();
return j == -1? lia_move::sat : create_branch_on_column(j);
}
TRACE("arith_int", tout << "j = " << j << " does not have an integer assignment: " << get_value(j) << "\n";);
r = proceed_with_gomory_cut(j);
if (r != lia_move::undef)
return r;
return create_branch_on_column(j);
return gomory_cut();
}
TRACE("check_main_int", tout << "branch"; );
int j = find_inf_int_base_column();
if (j == -1) {
j = find_inf_int_nbasis_column();
@ -969,7 +1008,7 @@ linear_combination_iterator<mpq> * int_solver::get_column_iterator(unsigned j) {
int_solver::int_solver(lar_solver* lar_slv) :
m_lar_solver(lar_slv),
m_branch_cut_counter(0),
m_cut_solver([this](unsigned j) {return m_lar_solver->get_column_name(j);},
m_chase_cut_solver([this](unsigned j) {return m_lar_solver->get_column_name(j);},
[this](unsigned j, std::ostream &o) {m_lar_solver->print_constraint(j, o);},
[this]() {return m_lar_solver->A_r().column_count();},
[this](unsigned j) {return get_value(j);},
@ -1328,21 +1367,21 @@ bool int_solver::is_term(unsigned j) const {
return m_lar_solver->column_corresponds_to_term(j);
}
void int_solver::add_constraint_to_cut_solver(unsigned ci, const lar_base_constraint * c) {
void int_solver::add_constraint_to_chase_cut_solver(unsigned ci, const lar_base_constraint * c) {
vector<mono> coeffs;
mpq rs;
get_int_coeffs_from_constraint<mpq>(c, coeffs, rs);
m_cut_solver.add_ineq(coeffs, -rs, ci);
m_chase_cut_solver.add_ineq(coeffs, -rs, ci);
}
void int_solver::pop(unsigned k) {
m_cut_solver.pop_trail(k);
while (m_cut_solver.number_of_asserts() > m_lar_solver->constraints().size())
m_cut_solver.pop_last_assert();
m_cut_solver.pop_constraints();
m_chase_cut_solver.pop_trail(k);
while (m_chase_cut_solver.number_of_asserts() > m_lar_solver->constraints().size())
m_chase_cut_solver.pop_last_assert();
m_chase_cut_solver.pop_constraints();
}
void int_solver::push() { m_cut_solver.push(); }
void int_solver::push() { m_chase_cut_solver.push(); }
unsigned int_solver::column_count() const { return m_lar_solver->column_count(); }