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

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-09 08:38:07 -08:00
parent 2512a958b9
commit 5964969f29
5 changed files with 41 additions and 53 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -31,7 +31,7 @@ class create_cut {
explanation* m_ex; // the conflict explanation
unsigned m_inf_col; // a basis column which has to be an integer but has a non integral value
const row_strip<mpq>& m_row;
const int_solver& m_int_solver;
const int_solver& lia;
mpq m_lcm_den;
mpq m_f;
mpq m_one_minus_f;
@ -42,18 +42,18 @@ class create_cut {
#endif
struct found_big {};
const impq & get_value(unsigned j) const { return m_int_solver.get_value(j); }
bool is_real(unsigned j) const { return m_int_solver.is_real(j); }
bool at_lower(unsigned j) const { return m_int_solver.at_lower(j); }
bool at_upper(unsigned j) const { return m_int_solver.at_upper(j); }
const impq & lower_bound(unsigned j) const { return m_int_solver.lower_bound(j); }
const impq & upper_bound(unsigned j) const { return m_int_solver.upper_bound(j); }
constraint_index column_lower_bound_constraint(unsigned j) const { return m_int_solver.column_lower_bound_constraint(j); }
constraint_index column_upper_bound_constraint(unsigned j) const { return m_int_solver.column_upper_bound_constraint(j); }
bool column_is_fixed(unsigned j) const { return m_int_solver.lra.column_is_fixed(j); }
const impq & get_value(unsigned j) const { return lia.get_value(j); }
bool is_real(unsigned j) const { return lia.is_real(j); }
bool at_lower(unsigned j) const { return lia.at_lower(j); }
bool at_upper(unsigned j) const { return lia.at_upper(j); }
const impq & lower_bound(unsigned j) const { return lia.lower_bound(j); }
const impq & upper_bound(unsigned j) const { return lia.upper_bound(j); }
constraint_index column_lower_bound_constraint(unsigned j) const { return lia.column_lower_bound_constraint(j); }
constraint_index column_upper_bound_constraint(unsigned j) const { return lia.column_upper_bound_constraint(j); }
bool column_is_fixed(unsigned j) const { return lia.lra.column_is_fixed(j); }
void int_case_in_gomory_cut(unsigned j) {
lp_assert(m_int_solver.column_is_int(j) && m_fj.is_pos());
lp_assert(lia.column_is_int(j) && m_fj.is_pos());
TRACE("gomory_cut_detail",
tout << " k = " << m_k;
tout << ", fj: " << m_fj << ", ";
@ -131,7 +131,7 @@ class create_cut {
if (pol.size() == 1) {
TRACE("gomory_cut_detail", tout << "pol.size() is 1" << std::endl;);
unsigned v = pol[0].second;
lp_assert(m_int_solver.column_is_int(v));
lp_assert(lia.column_is_int(v));
const mpq& a = pol[0].first;
m_k /= a;
if (a.is_pos()) { // we have av >= k
@ -153,7 +153,7 @@ class create_cut {
// normalize coefficients of integer parameters to be integers.
for (auto & pi: pol) {
pi.first *= m_lcm_den;
SASSERT(!m_int_solver.column_is_int(pi.second) || pi.first.is_int());
SASSERT(!lia.column_is_int(pi.second) || pi.first.is_int());
}
m_k *= m_lcm_den;
}
@ -207,7 +207,7 @@ class create_cut {
}
void dump_declaration(std::ostream& out, unsigned v) const {
out << "(declare-const " << var_name(v) << (m_int_solver.column_is_int(v) ? " Int" : " Real") << ")\n";
out << "(declare-const " << var_name(v) << (lia.column_is_int(v) ? " Int" : " Real") << ")\n";
}
void dump_declarations(std::ostream& out) const {
@ -217,7 +217,7 @@ class create_cut {
}
for (const auto& p : m_t) {
unsigned v = p.var();
if (m_int_solver.lra.is_term(v)) {
if (lia.lra.is_term(v)) {
dump_declaration(out, v);
}
}
@ -276,7 +276,7 @@ public:
void dump(std::ostream& out) {
out << "applying cut at:\n"; print_linear_combination_indices_only<row_strip<mpq>, mpq>(m_row, out); out << std::endl;
for (auto & p : m_row) {
m_int_solver.lra.m_mpq_lar_core_solver.m_r_solver.print_column_info(p.var(), out);
lia.lra.m_mpq_lar_core_solver.m_r_solver.print_column_info(p.var(), out);
}
out << "inf_col = " << m_inf_col << std::endl;
}
@ -334,20 +334,20 @@ public:
return report_conflict_from_gomory_cut();
if (some_int_columns)
adjust_term_and_k_for_some_ints_case_gomory();
lp_assert(m_int_solver.current_solution_is_inf_on_cut());
lp_assert(lia.current_solution_is_inf_on_cut());
TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout););
m_int_solver.lra.subs_term_columns(m_t);
lia.lra.subs_term_columns(m_t);
TRACE("gomory_cut", print_linear_combination_of_column_indices_only(m_t.coeffs_as_vector(), tout << "gomory cut:"); tout << " <= " << m_k << std::endl;);
return lia_move::cut;
}
create_cut(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_int_j, const row_strip<mpq>& row, const int_solver& int_slv ) :
create_cut(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_int_j, const row_strip<mpq>& row, const int_solver& lia) :
m_t(t),
m_k(k),
m_ex(ex),
m_inf_col(basic_inf_int_j),
m_row(row),
m_int_solver(int_slv),
lia(lia),
m_lcm_den(1),
m_f(fractional_part(get_value(basic_inf_int_j).x)),
m_one_minus_f(1 - m_f) {}
@ -359,7 +359,6 @@ lia_move gomory::cut(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_
return cc.cut();
}
bool gomory::is_gomory_cut_target(const row_strip<mpq>& row) {
// All non base variables must be at their bounds and assigned to rationals (that is, infinitesimals are not allowed).
unsigned j;

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

@ -158,7 +158,7 @@ namespace lp {
// u += ncoeff * lower_bound(j).get_rational();
u.addmul(ncoeff, lra.column_lower_bound(j).x);
}
lia.add_to_explanation_from_fixed_or_boxed_column(j);
add_to_explanation_from_fixed_or_boxed_column(j);
}
else if (gcds.is_zero()) {
gcds = abs_ncoeff;
@ -186,7 +186,15 @@ namespace lp {
void int_gcd_test::fill_explanation_from_fixed_columns(const row_strip<mpq> & row) {
for (const auto & c : row) {
if (lra.column_is_fixed(c.var()))
lia.add_to_explanation_from_fixed_or_boxed_column(c.var());
add_to_explanation_from_fixed_or_boxed_column(c.var());
}
}
void int_gcd_test::add_to_explanation_from_fixed_or_boxed_column(unsigned j) {
constraint_index lc, uc;
lra.get_bound_constraint_witnesses_for_column(j, lc, uc);
lia.m_ex->push_justification(lc);
lia.m_ex->push_justification(uc);
}
}

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

@ -9,6 +9,15 @@ Abstract:
Gcd_Test heuristic
gcd test
5*x + 3*y + 6*z = 5
suppose x is fixed at 2.
so we have 10 + 3(y + 2z) = 5
5 = -3(y + 2z)
this is unsolvable because 5/3 is not an integer.
so we create a lemma that rules out this condition.
Author:
Nikolaj Bjorner (nbjorner)
Lev Nachmanson (levnach)
@ -33,7 +42,7 @@ namespace lp {
mpq const & lcm_den,
mpq const & consts);
void fill_explanation_from_fixed_columns(const row_strip<mpq> & row);
void add_to_explanation_from_fixed_or_boxed_column(unsigned j);
public:
int_gcd_test(int_solver& lia);
~int_gcd_test() {}

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

@ -312,12 +312,6 @@ lia_move int_solver::patch_nbasic_columns() {
}
// TBD: move to gcd-test
void int_solver::add_to_explanation_from_fixed_or_boxed_column(unsigned j) {
constraint_index lc, uc;
lra.get_bound_constraint_witnesses_for_column(j, lc, uc);
m_ex->push_justification(lc);
m_ex->push_justification(uc);
}
int_solver::int_solver(lar_solver& lar_slv) :

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

@ -52,6 +52,7 @@ public:
// methods
int_solver(lar_solver& lp);
// 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 *);
@ -69,31 +70,8 @@ public:
bool at_upper(unsigned j) const;
private:
// how to tighten bounds for integer variables.
bool gcd_test_for_row(static_matrix<mpq, numeric_pair<mpq>> & A, unsigned i);
// gcd test
// 5*x + 3*y + 6*z = 5
// suppose x is fixed at 2.
// so we have 10 + 3(y + 2z) = 5
// 5 = -3(y + 2z)
// this is unsolvable because 5/3 is not an integer.
// so we create a lemma that rules out this condition.
//
bool gcd_test(); // returns false in case of failure. Creates a theory lemma in case of failure.
bool branch(const lp_constraint<mpq, mpq> & new_inequality);
bool ext_gcd_test(const row_strip<mpq>& row,
mpq const & least_coeff,
mpq const & lcm_den,
mpq const & consts);
void fill_explanation_from_fixed_columns(const row_strip<mpq> & row);
void add_to_explanation_from_fixed_or_boxed_column(unsigned j);
lia_move patch_nbasic_columns();
bool get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m);
private:
bool is_boxed(unsigned j) const;
bool is_fixed(unsigned j) const;
bool is_free(unsigned j) const;