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

fix dump utility for cuts

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-09-19 14:32:56 -07:00
parent ed19af4c4e ac878698b9
commit 3c553c17e8
9 changed files with 165 additions and 61 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_arith_value.h
View file

@ -17,7 +17,7 @@ Author:
Revision History:
--*/
#pragma once;
#pragma once
#include "ast/arith_decl_plugin.h"
#include "smt/smt_context.h"

5
src/test/lp/gomory_test.h
View file

@ -1,4 +1,5 @@
namespace lp {
#include "util/lp/lp_utils.h"
struct gomory_test {
gomory_test(
std::function<std::string (unsigned)> name_function_p,
@ -88,7 +89,7 @@ struct gomory_test {
lp_assert(is_int(x_j));
lp_assert(!a.is_int());
lp_assert(f_0 > zero_of_type<mpq>() && f_0 < one_of_type<mpq>());
mpq f_j = int_solver::fractional_part(a);
mpq f_j = fractional_part(a);
TRACE("gomory_cut_detail",
tout << a << " x_j = " << x_j << ", k = " << k << "\n";
tout << "f_j: " << f_j << "\n";
@ -206,7 +207,7 @@ struct gomory_test {
unsigned x_j;
mpq a;
bool some_int_columns = false;
mpq f_0 = int_solver::fractional_part(get_value(inf_col));
mpq f_0 = fractional_part(get_value(inf_col));
mpq one_min_f_0 = 1 - f_0;
for ( auto pp : row) {
a = pp.first;

23
src/util/lp/column_namer.h
View file

@ -33,29 +33,6 @@ public:
print_linear_combination_of_column_indices(coeff, out);
}
template <typename T>
void print_linear_combination_of_column_indices_only(const vector<std::pair<T, unsigned>> & coeffs, std::ostream & out) const {
bool first = true;
for (const auto & it : coeffs) {
auto val = it.first;
if (first) {
first = false;
} else {
if (numeric_traits<T>::is_pos(val)) {
out << " + ";
} else {
out << " - ";
val = -val;
}
}
if (val == -numeric_traits<T>::one())
out << " - ";
else if (val != numeric_traits<T>::one())
out << T_to_string(val);
out << "v" << it.second;
}
}
template <typename T>

145
src/util/lp/gomory.cpp
View file

@ -20,6 +20,7 @@
#include "util/lp/gomory.h"
#include "util/lp/int_solver.h"
#include "util/lp/lar_solver.h"
#include "util/lp/lp_utils.h"
namespace lp {
class gomory::imp {
@ -40,35 +41,38 @@ class gomory::imp {
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.m_lar_solver->column_is_fixed(j); }
void int_case_in_gomory_cut(const mpq & a, unsigned j,
mpq & lcm_den, const mpq& f0, const mpq& one_minus_f0) {
mpq & lcm_den, const mpq& f0, const mpq& one_minus_f0) {
lp_assert(is_int(j) && !a.is_int());
mpq fj = int_solver::fractional_part(a);
lp_assert(fj.is_pos());
mpq fj = fractional_part(a);
TRACE("gomory_cut_detail",
tout << a << " j=" << j << " k = " << m_k;
tout << ", fj: " << fj << ", ";
tout << "f0: " << f0 << ", ";
tout << "1 - f0: " << 1 - f0 << ", ";
tout << "a - fj = " << a - fj << ", ";
tout << (at_lower(j)?"at_lower":"at_upper")<< std::endl;
);
lp_assert(fj.is_pos() && (a - fj).is_int());
mpq new_a;
mpq one_minus_fj = 1 - fj;
if (at_lower(j)) {
new_a = fj < one_minus_f0? fj / one_minus_f0 : one_minus_fj / f0;
new_a = fj <= one_minus_f0 ? fj / one_minus_f0 : ((1 - fj) / f0);
m_k.addmul(new_a, lower_bound(j).x);
// m_k += (new_a * lower_bound(j).x);
lp_assert(new_a.is_pos());
m_ex.push_justification(column_lower_bound_constraint(j), new_a);
}
else {
lp_assert(at_upper(j));
// the upper terms are inverted: therefore we have the minus
new_a = - (fj < f0? fj / f0 : one_minus_fj / one_minus_f0);
new_a = - (fj <= f0 ? fj / f0 : ((1 - fj) / one_minus_f0));
lp_assert(new_a.is_neg());
m_k.addmul(new_a, upper_bound(j).x);
// m_k += (new_a * upper_bound(j).x);
m_ex.push_justification(column_upper_bound_constraint(j), new_a);
}
TRACE("gomory_cut_detail", tout << "new_a: " << new_a << " k: " << m_k << "\n";);
m_t.add_monomial(new_a, j);
lcm_den = lcm(lcm_den, denominator(new_a));
TRACE("gomory_cut_detail", tout << "v" << j << " new_a = " << new_a << ", k = " << m_k << ", lcm_den = " << lcm_den << "\n";);
}
void real_case_in_gomory_cut(const mpq & a, unsigned x_j, const mpq& f0, const mpq& one_minus_f0) {
@ -111,6 +115,7 @@ class gomory::imp {
void adjust_term_and_k_for_some_ints_case_gomory(mpq &lcm_den) {
lp_assert(!m_t.is_empty());
// k = 1 + sum of m_t at bounds
auto pol = m_t.coeffs_as_vector();
m_t.clear();
if (pol.size() == 1) {
@ -131,9 +136,9 @@ class gomory::imp {
m_t.add_monomial(mpq(1), v);
}
} else {
TRACE("gomory_cut_detail", tout << "pol.size() > 1" << std::endl;);
lcm_den = lcm(lcm_den, denominator(m_k));
lp_assert(lcm_den.is_pos());
TRACE("gomory_cut_detail", tout << "pol.size() > 1 den: " << lcm_den << std::endl;);
if (!lcm_den.is_one()) {
// normalize coefficients of integer parameters to be integers.
for (auto & pi: pol) {
@ -143,17 +148,114 @@ class gomory::imp {
m_k *= lcm_den;
}
// negate everything to return -pol <= -m_k
for (const auto & pi: pol)
for (const auto & pi: pol) {
TRACE("gomory_cut", tout << pi.first << "* " << "v" << pi.second << "\n";);
m_t.add_monomial(-pi.first, pi.second);
}
m_k.neg();
}
TRACE("gomory_cut_detail", tout << "k = " << m_k << std::endl;);
lp_assert(m_k.is_int());
}
std::string var_name(unsigned j) const {
return std::string("x") + std::to_string(j);
}
std::ostream& dump_coeff_val(std::ostream & out, const mpq & a) const {
if (a.is_int()) {
out << a;
}
else if ( a >= zero_of_type<mpq>())
out << "(/ " << numerator(a) << " " << denominator(a) << ")";
else {
out << "(- ( / " << numerator(-a) << " " << denominator(-a) << "))";
}
return out;
}
template <typename T>
void dump_coeff(std::ostream & out, const T& c) const {
out << "( * ";
dump_coeff_val(out, c.coeff());
out << " " << var_name(c.var()) << ")";
}
std::ostream& dump_row_coefficients(std::ostream & out) const {
mpq lc(1);
for (const auto& p : m_row) {
lc = lcm(lc, denominator(p.coeff()));
}
for (const auto& p : m_row) {
dump_coeff_val(out << " (* ", p.coeff()*lc) << " " << var_name(p.var()) << ")";
}
return out;
}
void dump_the_row(std::ostream& out) const {
out << "; the row, excluding fixed vars\n";
out << "(assert ( = ( +";
dump_row_coefficients(out) << ") 0))\n";
}
void dump_declarations(std::ostream& out) const {
// for a column j the var name is vj
for (const auto & p : m_row) {
out << "(declare-const " << var_name(p.var())
<< (is_int(p.var())? " Int" : " Real") << ")\n";
}
}
void dump_lower_bound_expl(std::ostream & out, unsigned j) const {
out << "(assert (>= " << var_name(j) << " " << lower_bound(j).x << "))\n";
}
void dump_upper_bound_expl(std::ostream & out, unsigned j) const {
out << "(assert (<= " << var_name(j) << " " << upper_bound(j).x << "))\n";
}
void dump_explanations(std::ostream& out) const {
for (const auto & p : m_row) {
unsigned j = p.var();
if (j == m_inf_col || (!is_real(j) && p.coeff().is_int())) {
continue;
}
else if (at_lower(j)) {
dump_lower_bound_expl(out, j);
} else {
lp_assert(at_upper(j));
dump_upper_bound_expl(out, j);
}
}
}
std::ostream& dump_term_coefficients(std::ostream & out) const {
for (const auto& p : m_t) {
dump_coeff(out, p);
}
return out;
}
std::ostream& dump_term_sum(std::ostream & out) const {
return dump_term_coefficients(out << "(+ ") << ")";
}
std::ostream& dump_term_le_k(std::ostream & out) const {
return dump_term_sum(out << "(<= ") << " " << m_k << ")";
}
void dump_the_cut_assert(std::ostream & out) const {
dump_term_le_k(out << "(assert (not ") << "))\n";
}
void dump_cut_and_constraints_as_smt_lemma(std::ostream& out) const {
dump_declarations(out);
dump_the_row(out);
dump_explanations(out);
dump_the_cut_assert(out);
out << "(check-sat)\n";
}
public:
lia_move create_cut() {
TRACE("gomory_cut",
tout << "applying cut at:\n"; m_int_solver.m_lar_solver->print_row(m_row, tout); tout << std::endl;
tout << "applying cut at:\n"; print_linear_combination_of_column_indices_only(m_row, tout); tout << std::endl;
for (auto & p : m_row) {
m_int_solver.m_lar_solver->m_mpq_lar_core_solver.m_r_solver.print_column_info(p.var(), tout);
}
@ -162,19 +264,18 @@ public:
// gomory will be t <= k and the current solution has a property t > k
m_k = 1;
m_t.clear();
mpq lcm_den(1);
bool some_int_columns = false;
mpq f0 = int_solver::fractional_part(get_value(m_inf_col));
mpq f0 = fractional_part(get_value(m_inf_col));
TRACE("gomory_cut_detail", tout << "f0: " << f0 << ", ";
tout << "1 - f0: " << 1 - f0 << ", get_value(m_inf_col).x - f0 = " << get_value(m_inf_col).x - f0;);
lp_assert(f0.is_pos() && (get_value(m_inf_col).x - f0).is_int());
mpq one_min_f0 = 1 - f0;
for (const auto & p : m_row) {
unsigned j = p.var();
#if 1
if (column_is_fixed(j)) {
m_ex.push_justification(column_lower_bound_constraint(j));
m_ex.push_justification(column_upper_bound_constraint(j));
continue;
}
#endif
if (j == m_inf_col) {
lp_assert(p.coeff() == one_of_type<mpq>());
TRACE("gomory_cut_detail", tout << "seeing basic var";);
@ -195,8 +296,10 @@ public:
if (some_int_columns)
adjust_term_and_k_for_some_ints_case_gomory(lcm_den);
lp_assert(m_int_solver.current_solution_is_inf_on_cut());
TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout););
m_int_solver.m_lar_solver->subs_term_columns(m_t, m_k);
TRACE("gomory_cut", tout<<"gomory cut:"; m_int_solver.m_lar_solver->print_term(m_t, tout) << " <= " << m_k << std::endl;);
// TBD: validate result of subs_term_columns
TRACE("gomory_cut", print_linear_combination_of_column_indices_only(m_t, tout << "gomory cut:"); tout << " <= " << m_k << std::endl;);
return lia_move::cut;
}
imp(lar_term & t, mpq & k, explanation& ex, unsigned basic_inf_int_j, const row_strip<mpq>& row, const int_solver& int_slv ) :

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

@ -189,7 +189,7 @@ struct check_return_helper {
m_lar_solver->set_track_pivoted_rows(m_track_pivoted_rows);
if (m_r == lia_move::cut || m_r == lia_move::branch) {
int_solver * s = m_lar_solver->get_int_solver();
m_lar_solver->adjust_cut_for_terms(*(s->m_t), *(s->m_k));
// m_lar_solver->adjust_cut_for_terms(*(s->m_t), *(s->m_k));
}
}
};

8
src/util/lp/int_solver.h
View file

@ -113,17 +113,9 @@ private:
bool has_low(unsigned j) const;
bool has_upper(unsigned j) const;
unsigned row_of_basic_column(unsigned j) const;
inline static bool is_rational(const impq & n) {
return is_zero(n.y);
}
public:
void display_column(std::ostream & out, unsigned j) const;
inline static
mpq fractional_part(const impq & n) {
lp_assert(is_rational(n));
return n.x - floor(n.x);
}
constraint_index column_upper_bound_constraint(unsigned j) const;
constraint_index column_lower_bound_constraint(unsigned j) const;
bool current_solution_is_inf_on_cut() const;

2
src/util/lp/lar_solver.cpp
View file

@ -1273,7 +1273,7 @@ std::ostream& lar_solver::print_term_as_indices(lar_term const& term, std::ostre
if (!numeric_traits<mpq>::is_zero(term.m_v)) {
out << term.m_v << " + ";
}
print_linear_combination_of_column_indices_only(term.coeffs_as_vector(), out);
print_linear_combination_of_column_indices_only(term, out);
return out;
}

8
src/util/lp/lp_settings.h
View file

@ -433,7 +433,15 @@ inline void ensure_increasing(vector<unsigned> & v) {
}
}
inline static bool is_rational(const impq & n) { return is_zero(n.y); }
inline static mpq fractional_part(const impq & n) {
lp_assert(is_rational(n));
return n.x - floor(n.x);
}
inline static mpq fractional_part(const mpq & n) {
return n - floor(n);
}
#if Z3DEBUG
bool D();

31
src/util/lp/lp_utils.h
View file

@ -50,11 +50,34 @@ bool contains(const std::unordered_map<A, B> & map, const A& key) {
namespace lp {
inline void throw_exception(std::string && str) {
throw default_exception(std::move(str));
template <typename T>
void print_linear_combination_of_column_indices_only(const T & coeffs, std::ostream & out) {
bool first = true;
for (const auto & it : coeffs) {
auto val = it.coeff();
if (first) {
first = false;
} else {
if (val.is_pos()) {
out << " + ";
} else {
out << " - ";
val = -val;
}
}
if (val == 1)
out << " ";
else
out << T_to_string(val);
out << "x" << it.var();
}
typedef z3_exception exception;
}
inline void throw_exception(std::string && str) {
throw default_exception(std::move(str));
}
typedef z3_exception exception;
#define lp_assert(_x_) { SASSERT(_x_); }
inline void lp_unreachable() { lp_assert(false); }