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

improved dio handler

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-03-10 07:06:36 -10:00 committed by Lev Nachmanson
parent 30021dd74f
commit 6f7b749ff9
11 changed files with 885 additions and 544 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

63
src/math/lp/bound_analyzer_on_row.h
View file

@ -92,13 +92,13 @@ private:
}
const impq & ub(unsigned j) const {
lp_assert(m_bp.upper_bound_is_available(j));
return m_bp.get_upper_bound(j);
lp_assert(upper_bound_is_available(j));
return get_upper_bound(j);
}
const impq & lb(unsigned j) const {
lp_assert(m_bp.lower_bound_is_available(j));
return m_bp.get_lower_bound(j);
lp_assert(lower_bound_is_available(j));
return get_lower_bound(j);
}
const mpq & monoid_max_no_mult(bool a_is_pos, unsigned j, bool & strict) const {
@ -148,8 +148,7 @@ private:
mpq m_total, m_bound;
void limit_all_monoids_from_above() {
int strict = 0;
m_total.reset();
lp_assert(is_zero(m_total));
m_total = m_rs.x;
for (const auto& p : m_row) {
bool str;
m_total -= monoid_min(p.coeff(), p.var(), str);
@ -174,8 +173,7 @@ private:
void limit_all_monoids_from_below() {
int strict = 0;
m_total.reset();
lp_assert(is_zero(m_total));
m_total = m_rs.x;
for (const auto &p : m_row) {
bool str;
m_total -= monoid_max(p.coeff(), p.var(), str);
@ -205,7 +203,7 @@ private:
// every other monoid is impossible to limit from below
mpq u_coeff;
unsigned j;
m_bound = -m_rs.x;
m_bound = m_rs.x;
bool strict = false;
for (const auto& p : m_row) {
j = p.var();
@ -234,7 +232,7 @@ private:
// every other monoid is impossible to limit from above
mpq l_coeff;
unsigned j;
m_bound = -m_rs.x;
m_bound = m_rs.x;
bool strict = false;
for (const auto &p : m_row) {
j = p.var();
@ -275,8 +273,7 @@ private:
// */
// }
void limit_j(unsigned bound_j, const mpq& u, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict)
{
void limit_j(unsigned bound_j, const mpq& u, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict) {
auto* lar = &m_bp.lp();
const auto& row = this->m_row;
auto explain = [row, bound_j, coeff_before_j_is_pos, is_lower_bound, strict, lar]() {
@ -310,7 +307,7 @@ private:
}
void analyze_bound_on_var_on_coeff(int j, const mpq &a) {
switch (m_bp.get_column_type(j)) {
switch (get_column_type(j)) {
case column_type::lower_bound:
if (numeric_traits<mpq>::is_pos(a))
advance_u(j);
@ -332,8 +329,42 @@ private:
}
}
};
const impq& get_upper_bound(unsigned j) const {
return lp().get_upper_bound(j);
}
const impq& get_lower_bound(unsigned j) const {
return lp().get_lower_bound(j);
}
column_type get_column_type(unsigned j) const {
return (lp().get_column_types())[j];
}
const auto& lp() const { return m_bp.lp(); }
auto& lp() { return m_bp.lp(); }
bool upper_bound_is_available(unsigned j) const {
switch (get_column_type(j)) {
case column_type::fixed:
case column_type::boxed:
case column_type::upper_bound:
return true;
default:
return false;
}
}
bool lower_bound_is_available(unsigned j) const {
switch (get_column_type(j)) {
case column_type::fixed:
case column_type::boxed:
case column_type::lower_bound:
return true;
default:
return false;
}
}
};
}

496
src/math/lp/dioph_eq.cpp
View file

@ -232,6 +232,11 @@ namespace lp {
t += mpq(-1) * b;
return t.c() == mpq(0) && t.size() == 0;
}
friend bool operator!=(const term_o& a, const term_o& b) {
return ! (a == b);
}
#endif
term_o& operator+=(const term_o& t) {
for (const auto& p : t) {
@ -244,23 +249,16 @@ namespace lp {
std::ostream& print_S(std::ostream& out) {
out << "S:\n";
for (const auto& p : m_k2s.m_map) {
print_entry(p.second, out, false, false);
for (unsigned ei = 0 ; ei < m_e_matrix.row_count(); ei++) {
print_entry(ei, out, false, false, true);
}
return out;
}
std::ostream& print_bounds(std::ostream& out) {
out << "bounds:\n";
for (unsigned v = 0; v < m_var_register.size(); ++v) {
unsigned j = m_var_register.local_to_external(v);
out << "j" << j << ":= " << lra.get_column_value(j) << ": ";
if (lra.column_has_lower_bound(j))
out << lra.column_lower_bound(j).x << " <= ";
out << "x" << v;
if (lra.column_has_upper_bound(j))
out << " <= " << lra.column_upper_bound(j).x;
out << "\n";
for (unsigned v = 0; v < lra.column_count(); ++v) {
lra.print_column_info(v, out);
}
return out;
}
@ -467,6 +465,9 @@ namespace lp {
m_data.clear();
SASSERT(invariant());
}
auto begin() const { return m_data.begin();}
auto end() const { return m_data.end(); }
};
// m_lspace is for operations on l_terms - m_e_matrix rows
@ -483,7 +484,7 @@ namespace lp {
std::unordered_map<unsigned, std_vector<unsigned>> m_row2fresh_defs;
indexed_uint_set m_changed_rows;
indexed_uint_set m_changed_columns;
indexed_uint_set m_new_fixed_columns;
indexed_uint_set m_changed_terms; // a term is defined by its column j, as in lar_solver.get_term(j)
indexed_uint_set m_tightened_columns; // the column that got tightened by the tigthening phase,
// m_column_to_terms[j] is the set of all k such lra.get_term(k) depends on j
@ -711,8 +712,8 @@ namespace lp {
}
void add_changed_column(unsigned j) {
TRACE("dioph_eq", lra.print_column_info(j, tout););
m_changed_columns.insert(j);
TRACE("dio", lra.print_column_info(j, tout););
m_new_fixed_columns.insert(j);
}
std_vector<const lar_term*> m_added_terms;
std::unordered_set<const lar_term*> m_active_terms;
@ -742,7 +743,7 @@ namespace lp {
void update_column_bound_callback(unsigned j) {
if (!lra.column_is_int(j) || !lra.column_is_fixed(j))
return;
m_changed_columns.insert(j);
m_new_fixed_columns.insert(j);
auto undo = undo_fixed_column(*this, j);
lra.trail().push(undo);
}
@ -908,7 +909,7 @@ namespace lp {
TRACE("dioph_eq", print_entry(ei, tout) << std::endl;);
mpq& c = m_sum_of_fixed[ei];
c = mpq(0);
open_l_term_to_work_vector(ei, c);
open_l_term_to_espace(ei, c);
clear_e_row(ei);
mpq denom(1);
for (const auto& p : m_espace.m_data) {
@ -931,7 +932,7 @@ namespace lp {
}
void find_changed_terms_and_more_changed_rows() {
for (unsigned j : m_changed_columns) {
for (unsigned j : m_new_fixed_columns) {
const auto it = m_columns_to_terms.find(j);
if (it != m_columns_to_terms.end())
for (unsigned k : it->second) {
@ -979,7 +980,7 @@ namespace lp {
}
}
void process_changed_columns() {
void process_changed_columns(std_vector<unsigned> &f_vector) {
find_changed_terms_and_more_changed_rows();
for (unsigned j : m_changed_terms) {
if (j >= m_l_matrix.column_count()) continue;
@ -1008,7 +1009,10 @@ namespace lp {
for (unsigned ei : m_changed_rows) {
if (ei >= m_e_matrix.row_count())
continue;
if (belongs_to_s(ei))
f_vector.push_back(ei);
recalculate_entry(ei);
if (m_e_matrix.m_columns.back().size() == 0) {
m_e_matrix.m_columns.pop_back();
m_var_register.shrink(m_e_matrix.column_count());
@ -1021,8 +1025,8 @@ namespace lp {
remove_irrelevant_fresh_defs();
eliminate_substituted_in_changed_rows();
m_changed_columns.reset();
SASSERT(m_changed_columns.size() == 0);
m_new_fixed_columns.reset();
SASSERT(m_new_fixed_columns.size() == 0);
m_changed_rows.reset();
SASSERT(entries_are_ok());
}
@ -1046,37 +1050,16 @@ namespace lp {
subs_entry(ei);
}
void transpose_entries(unsigned i, unsigned k) {
SASSERT(i != k);
m_l_matrix.transpose_rows(i, k);
m_e_matrix.transpose_rows(i, k);
std::swap(m_sum_of_fixed[i], m_sum_of_fixed[k]);
m_k2s.transpose_val(i, k);
NOT_IMPLEMENTED_YET();
/*
// transpose fresh definitions
for (auto & fd: m_fresh_definitions) {
if (fd.m_ei == i)
fd.m_ei = k;
else if (fd.m_ei == k)
fd.m_ei = i;
if (fd.m_origin == i)
fd.m_origin = k;
}*/
}
// returns true if a variable j is substituted
bool can_substitute(unsigned j) const {
return m_k2s.has_key(j) || m_fresh_k2xt_terms.has_key(j);
}
bool entries_are_ok() {
if (lra.settings().get_cancel_flag()) return true;
for (unsigned ei = 0; ei < m_e_matrix.row_count(); ei++) {
if (entry_invariant(ei) == false) {
TRACE("dioph_deb_eq", tout << "bad entry:"; print_entry(ei, tout););
TRACE("dio", tout << "bad entry:"; print_entry(ei, tout););
return false;
}
if (belongs_to_f(ei)) {
@ -1084,19 +1067,18 @@ namespace lp {
const auto& row = m_e_matrix.m_rows[ei];
for (const auto& p : row) {
if (m_k2s.has_key(p.var())) {
/*
std::cout << "entry:" << ei << " belongs to f but depends on column " << p.var() << std::endl;
std::cout << "m_var_register.local_to_external(p.var()):" << m_var_register.local_to_external(p.var()) << std::endl;
print_entry(ei, std::cout);
std::cout << "column " << p.var() << " of m_e_matrix:";
TRACE("dio",
tout << "entry:" << ei << " belongs to f but depends on column " << p.var() << std::endl;
tout << "m_var_register.local_to_external(p.var()):" << m_var_register.local_to_external(p.var()) << std::endl;
print_entry(ei, tout);
tout << "column " << p.var() << " of m_e_matrix:";
for (const auto & c : m_e_matrix.m_columns[p.var()]) {
std::cout << "row:" << c.var() << ", ";
tout << "row:" << c.var() << ", ";
}
std::cout << std::endl;
std::cout << "column " << p.var() << " is subst by entry:";
print_entry(m_k2s[p.var()],std::cout) << std::endl;
*/
tout << std::endl;
tout << "column " << p.var() << " is subst by entry:";
print_entry(m_k2s[p.var()],tout) << std::endl;);
return false;
}
}
@ -1105,7 +1087,7 @@ namespace lp {
return true;
}
void init() {
void init(std_vector<unsigned> & f_vector) {
m_report_branch = false;
m_conflict_index = -1;
m_infeas_explanation.clear();
@ -1114,9 +1096,10 @@ namespace lp {
m_branch_stack.clear();
m_lra_level = 0;
process_changed_columns();
process_changed_columns(f_vector);
for (const lar_term* t : m_added_terms) {
m_active_terms.insert(t);
f_vector.push_back(m_e_matrix.row_count()); // going to add a row in fill_entry
fill_entry(*t);
register_columns_to_term(*t);
}
@ -1146,18 +1129,28 @@ namespace lp {
return g;
}
std::ostream& print_deps(std::ostream& out, u_dependency* dep) {
std::ostream& print_deps(std::ostream& out, u_dependency* dep) const {
explanation ex(lra.flatten(dep));
return lra.print_expl(out, ex);
}
bool has_fresh_var(unsigned row_index) const {
for (const auto& p : m_e_matrix.m_rows[row_index]) {
bool var_is_fresh(unsigned j) const {
bool ret = m_fresh_k2xt_terms.has_second_key(j);
SASSERT(!ret || m_var_register.local_to_external(j) == UINT_MAX);
return ret;
}
template <typename T>
bool has_fresh_var(const T& t) const {
for (const auto& p : t) {
if (var_is_fresh(p.var()))
return true;
}
return false;
}
bool has_fresh_var(unsigned row_index) const {
return has_fresh_var(m_e_matrix[row_index]);
}
// A conflict is reported when the gcd of the monomial coefficients does not divide the free coefficent.
// If there is no conflict the entry is divided, normalized, by gcd.
@ -1202,7 +1195,7 @@ namespace lp {
void subs_qfront_by_fresh(unsigned k, protected_queue& q) {
const lar_term& e = m_fresh_k2xt_terms.get_by_key(k).first;
TRACE("dioph_eq", tout << "k:" << k << ", in ";
print_term_o(create_term_from_subst_space(), tout) << std::endl;
print_term_o(create_term_from_espace(), tout) << std::endl;
tout << "subs with e:";
print_lar_term_L(e, tout) << std::endl;);
mpq coeff = -m_espace[k]; // need to copy since it will be zeroed
@ -1221,8 +1214,8 @@ namespace lp {
}
// there is no change in m_l_matrix
TRACE("dioph_eq", tout << "after subs k:" << k << "\n";
print_term_o(create_term_from_subst_space(), tout) << std::endl;
tout << "m_term_with_index:{"; print_lar_term_L(m_lspace.m_data, tout);
print_term_o(create_term_from_espace(), tout) << std::endl;
tout << "m_lspace:{"; print_lar_term_L(m_lspace.m_data, tout);
tout << "}, opened:"; print_ml(m_lspace.to_term(), tout) << std::endl;);
}
@ -1234,8 +1227,8 @@ namespace lp {
void subs_qfront_by_S(unsigned k, protected_queue& q) {
const mpq& e = m_sum_of_fixed[m_k2s[k]];
TRACE("dioph_eq", tout << "k:" << k << ", in ";
print_term_o(create_term_from_subst_space(), tout) << std::endl;
TRACE("dio", tout << "k:" << k << ", in ";
print_term_o(create_term_from_espace(), tout) << std::endl;
tout << "subs with e:";
print_entry(m_k2s[k], tout) << std::endl;);
mpq coeff = m_espace[k]; // need to copy since it will be zeroed
@ -1263,9 +1256,9 @@ namespace lp {
}
m_c += coeff * e;
add_l_row_to_term_with_index(coeff, sub_index(k));
TRACE("dioph_eq", tout << "after subs k:" << k << "\n";
print_term_o(create_term_from_subst_space(), tout) << std::endl;
tout << "m_term_with_index:{"; print_lar_term_L(m_lspace.to_term(), tout);
TRACE("dio", tout << "after subs k:" << k << "\n";
print_term_o(create_term_from_espace(), tout) << std::endl;
tout << "m_lspace:{"; print_lar_term_L(m_lspace.to_term(), tout);
tout << "}, opened:"; print_ml(m_lspace.to_term(), tout) << std::endl;);
}
@ -1314,8 +1307,7 @@ namespace lp {
return lra.column_is_fixed(j);
}
template <typename T>
term_o fix_vars(const T& t) const {
term_o fix_vars(const lar_term& t) const {
term_o ret;
for (const auto& p : t) {
if (is_fixed(p.var())) {
@ -1328,6 +1320,20 @@ namespace lp {
return ret;
}
term_o fix_vars(const term_o& t) const {
term_o ret;
ret.c() = t.c();
for (const auto& p : t) {
if (is_fixed(p.var())) {
ret.c() += p.coeff() * this->lra.get_lower_bound(p.var()).x;
}
else {
ret.add_monomial(p.coeff(), p.var());
}
}
return ret;
}
const unsigned sub_index(unsigned k) const {
return m_k2s[k];
}
@ -1339,6 +1345,22 @@ namespace lp {
return value;
}
bool subs_invariant(unsigned j) const {
term_o ls = fix_vars(term_to_lar_solver(remove_fresh_vars(create_term_from_espace())));
term_o t0 = m_lspace.to_term();
term_o t1 = open_ml(t0);
t1.add_monomial(mpq(1), j);
term_o rs = fix_vars(t1);
if (ls != rs) {
std::cout << "enabling trace dio\n";
enable_trace("dio");
TRACE("dio", tout << "ls:"; print_term_o(ls, tout) << "\n";
tout << "rs:"; print_term_o(rs, tout) << "\n";);
return false;
}
return true;
}
void subs_with_S_and_fresh(protected_queue& q) {
while (!q.empty())
subs_front_with_S_and_fresh(q);
@ -1364,8 +1386,7 @@ namespace lp {
std_vector<unsigned> cleanup;
m_tightened_columns.reset();
for (unsigned j : m_changed_terms) {
if (
j >= lra.column_count() ||
if (j >= lra.column_count() ||
!lra.column_has_term(j) ||
lra.column_is_free(j) ||
is_fixed(j) || !lia.column_is_int(j)) {
@ -1384,12 +1405,11 @@ namespace lp {
// Process sorted terms
TRACE("dio",
tout << "changed terms:"; for (auto j : sorted_changed_terms) tout << j << " "; tout << std::endl;
print_S(tout);
print_bounds(tout);
// print_S(tout);
// print_bounds(tout);
);
for (unsigned j : sorted_changed_terms) {
m_changed_terms.remove(j);
r = tighten_bounds_for_term_column(j);
if (r != lia_move::undef) {
break;
@ -1413,7 +1433,7 @@ namespace lp {
}
#endif
term_o create_term_from_subst_space() {
term_o create_term_from_espace() const {
term_o t;
for (const auto& p : m_espace.m_data) {
t.add_monomial(p.coeff(), p.var());
@ -1422,61 +1442,78 @@ namespace lp {
return t;
}
// We will have lar_t, and let j is lar_t.j(), the term column.
// In the m_espace we have lar_t. The result of open_ml((1*j)) is lar_t - (1, j).
// So we have "equality" m_espace = open(m_lspace) + (1*lar_t.j.
void init_substitutions(const lar_term& lar_t, protected_queue& q) {
m_espace.clear();
m_c = mpq(0);
m_lspace.clear();
m_lspace.add(mpq(1), lar_t.j());
SASSERT(get_extended_term_value(lar_t).is_zero());
TRACE("dioph_eq", tout << "t:";print_lar_term_L(lar_t, tout) << std::endl; tout << "value:" << get_extended_term_value(lar_t) << std::endl;);
for (const auto& p : lar_t) {
SASSERT(p.coeff().is_int());
if (is_fixed(p.j())) {
m_c += p.coeff() * lia.lower_bound(p.j()).x;
SASSERT(lia.lower_bound(p.j()).x == lra.get_column_value(p.j()).x);
}
else {
unsigned lj = lar_solver_to_local(p.j());
m_espace.add(p.coeff(), lj);;
if (!lra.column_is_fixed(p.j()) && can_substitute(lj))
q.push(lar_solver_to_local(p.j()));
if (can_substitute(lj))
q.push(lj);
}
}
TRACE("dioph_eq", tout << "m_espace:"; print_term_o(create_term_from_subst_space(), tout) << std::endl;
tout << "m_c:" << m_c << std::endl;
tout << "get_value_of_subs_space:" << get_value_of_espace() << std::endl;);
SASSERT(subs_invariant(lar_t.j()));
}
unsigned lar_solver_to_local(unsigned j) const {
return m_var_register.external_to_local(j);
}
// j is the index of the column representing a term
// return true if a conflict was found
void process_fixed_in_espace() {
std_vector<unsigned> fixed_vars;
for (const auto & p: m_espace) {
if (!var_is_fresh(p.var()) && is_fixed(local_to_lar_solver(p.var())))
fixed_vars.push_back(p.var());
}
for (unsigned j : fixed_vars) {
m_c += m_espace[j] * lra.get_lower_bound(local_to_lar_solver(j)).x;
m_espace.erase(j);
}
}
/* j is the index of the column representing a term
Return lia_move::conflict if a conflict was found, lia_move::continue_with_check if j became a fixed variable, and undef
otherwise
Let us say we have a constraint x + y <= 8, and after the substitutions with S and fresh variables
we have x+y = 7t - 1 <= 8, where t is a term. Then we have 7t <= 9, or t <= 9/7, or we can enforce t <= floor(9/7) = 1.
Then x + y = 7*1 - 1 <= 6: the bound is strenthgened. The constraint in this example comes from the upper bound on j, where
j is the slack variable in x+y + j = 0.
*/
lia_move tighten_bounds_for_term_column(unsigned j) {
term_o term_to_tighten = lra.get_term(j); // copy the term aside
SASSERT(get_extended_term_value(term_to_tighten).is_zero());
if (!all_vars_are_int(term_to_tighten))
return lia_move::undef;
// q is the queue of variables that can be substituted in term_to_tighten
protected_queue q;
TRACE("dioph_eq", tout << "j:" << j << ", t: "; print_lar_term_L(term_to_tighten, tout) << std::endl;);
TRACE("dio", tout << "j:" << j << " , intitial term t: "; print_lar_term_L(term_to_tighten, tout) << std::endl;
for( const auto& p : term_to_tighten) {
lra.print_column_info(p.var(), tout);
}
);
init_substitutions(term_to_tighten, q);
if (q.empty())
if (q.empty()) // todo: maybe still go ahead and process it?
return lia_move::undef;
TRACE("dioph_eq", tout << "t:"; print_lar_term_L(term_to_tighten, tout) << std::endl;
tout << "subs_space:"; print_term_o(create_term_from_subst_space(), tout) << std::endl;
TRACE("dio", tout << "t:";
tout << "m_espace:";
print_term_o(create_term_from_espace(), tout) << std::endl;
tout << "m_lspace:";
print_lar_term_L(m_lspace.to_term(), tout) << std::endl;);
subs_with_S_and_fresh(q);
TRACE("dioph_eq", tout << "after subs\n"; print_term_o(create_term_from_subst_space(), tout) << std::endl; tout << "m_l_term_space:"; print_lar_term_L(m_lspace.to_term(), tout) << std::endl; tout << "open_ml:"; print_lar_term_L(open_ml(m_lspace.to_term()), tout) << std::endl; tout << "term_to_tighten + open_ml:"; print_term_o(term_to_tighten + open_ml(m_lspace.to_term()), tout) << std::endl; term_o ls = fix_vars(term_to_tighten + open_ml(m_lspace.to_term())); tout << "ls:"; print_term_o(ls, tout) << std::endl; term_o rs = term_to_lar_solver(remove_fresh_vars(create_term_from_subst_space())); tout << "rs:"; print_term_o(rs, tout) << std::endl; term_o diff = ls - rs; if (!diff.is_empty()) {
tout << "diff:"; print_term_o(diff, tout ) << std::endl; });
SASSERT(
fix_vars(term_to_tighten + open_ml(m_lspace.to_term())) ==
term_to_lar_solver(remove_fresh_vars(create_term_from_subst_space())));
process_fixed_in_espace();
SASSERT(subs_invariant(j));
mpq g = gcd_of_coeffs(m_espace.m_data, true);
TRACE("dioph_eq", tout << "after process_q_with_S\nt:"; print_term_o(create_term_from_subst_space(), tout) << std::endl; tout << "g:" << g << std::endl;);
TRACE("dio", tout << "after process_q_with_S\nt:"; print_term_o(create_term_from_espace(), tout) << std::endl; tout << "g:" << g << std::endl;);
if (g.is_one())
return lia_move::undef;
@ -1498,6 +1535,9 @@ namespace lp {
if (tighten_bounds_for_non_trivial_gcd(g, j, false) != lia_move::undef) {
return lia_move::conflict;
}
if (m_new_fixed_columns.contains(j)) {
return lia_move::continue_with_check;
}
return lia_move::undef;
}
@ -1536,10 +1576,11 @@ namespace lp {
}
return ret;
}
impq get_term_value(const lar_term& t) const {
impq ret;
mpq get_term_value(const term_o& t) const {
mpq ret = t.c();
for (const auto& p : t) {
ret += p.coeff() * lra.get_column_value(p.j());
ret += p.coeff() * lra.get_column_value(p.var()).x;
}
return ret;
}
@ -1571,7 +1612,6 @@ namespace lp {
lia.offset() = floor(rs);
lia.is_upper() = true;
m_report_branch = true;
enable_trace("dioph_eq");
TRACE("dioph_eq", tout << "prepare branch, t:";
print_lar_term_L(t, tout)
<< " <= " << lia.offset()
@ -1622,9 +1662,7 @@ namespace lp {
}
}
lia_move propagate_bounds_on_tightened_columns() {
return lia_move::undef;
}
// m_espace contains the coefficients of the term
// m_c contains the fixed part of the term
// m_tmp_l is the linear combination of the equations that removes the
@ -1638,21 +1676,23 @@ namespace lp {
SASSERT(!g.is_zero());
if (lra.has_bound_of_type(j, b_dep, rs, is_strict, is_upper)) {
TRACE("dioph_eq", tout << "current upper bound for x" << j << ":"
TRACE("dio",
tout << "current " << (is_upper? "upper":"lower") << " bound for x" << j << ":"
<< rs << std::endl;);
rs = (rs - m_c) / g;
TRACE("dioph_eq", tout << "(rs - m_c) / g:" << rs << std::endl;);
TRACE("dio", tout << "((rs - m_c) / g):" << rs << std::endl;);
if (!rs.is_int()) {
if (tighten_bound_kind(g, j, rs, is_upper, b_dep))
if (tighten_bound_kind(g, j, rs, is_upper))
return lia_move::conflict;
} else {
TRACE("dio", tout << "no improvement in the bound\n";);
}
}
return lia_move::undef;
}
unsigned m_n_of_lemmas = 0;
// returns true only on a conflict
bool tighten_bound_kind(const mpq& g, unsigned j, const mpq& ub, bool upper,
u_dependency* prev_dep) {
bool tighten_bound_kind(const mpq& g, unsigned j, const mpq& ub, bool upper) {
// ub = (upper_bound(j) - m_c)/g.
// we have xj = t = g*t_+ m_c <= upper_bound(j), then
// t_ <= floor((upper_bound(j) - m_c)/g) = floor(ub)
@ -1661,27 +1701,31 @@ namespace lp {
// <= can be replaced with >= for lower bounds, with ceil instead of
// floor
mpq bound = g * (upper ? floor(ub) : ceil(ub)) + m_c;
TRACE("dioph_eq", tout << "is upper:" << upper << std::endl;
TRACE("dio", tout << "is upper:" << upper << std::endl;
tout << "new " << (upper ? "upper" : "lower")
<< " bound:" << bound << std::endl;);
SASSERT((upper && bound < lra.get_upper_bound(j).x) ||
(!upper && bound > lra.get_lower_bound(j).x));
lconstraint_kind kind =
upper ? lconstraint_kind::LE : lconstraint_kind::GE;
u_dependency* dep = prev_dep;
dep = lra.join_deps(dep, explain_fixed_in_meta_term(m_lspace.m_data));
u_dependency* j_bound_dep = upper
? lra.get_column_upper_bound_witness(j)
: lra.get_column_lower_bound_witness(j);
dep = lra.join_deps(dep, j_bound_dep);
dep = lra.join_deps(dep, explain_fixed(lra.get_term(j)));
dep =
lra.join_deps(dep, lra.get_bound_constraint_witnesses_for_column(j));
TRACE("dioph_eq", tout << "jterm:";
lconstraint_kind kind = upper ? lconstraint_kind::LE : lconstraint_kind::GE;
u_dependency* dep = upper ? lra.get_column_upper_bound_witness(j) : lra.get_column_lower_bound_witness(j);
auto rs = open_fixed_from_ml(m_lspace);
// the right side is off by 1*j from m_espace
if (is_fixed(j))
rs.add(mpq(1), j);
for (const auto& p: rs) {
SASSERT(is_fixed(p.var()));
dep = lra.join_deps(dep, lra.get_bound_constraint_witnesses_for_column(p.var()));
}
TRACE("dio", tout << "jterm:";
print_lar_term_L(lra.get_term(j), tout) << "\ndep:";
print_deps(tout, dep) << std::endl;);
lra.update_column_type_and_bound(j, kind, bound, dep);
if (lra.settings().dump_bound_lemmas()) {
std::string lemma_name = "lemma" + std::to_string(m_n_of_lemmas++);
lra.write_bound_lemma_to_file(j, !upper, lemma_name, std::string( __FILE__)+ ","+ std::to_string(__LINE__));
}
lp_status st = lra.find_feasible_solution();
if ((int)st >= (int)lp::lp_status::FEASIBLE) {
m_tightened_columns.insert(j);
@ -1693,16 +1737,16 @@ namespace lp {
}
template <typename T>
u_dependency* explain_fixed_in_meta_term(const T& t) {
return explain_fixed(open_ml(t));
u_dependency* explain_fixed_in_meta_term(const T& t) const {
return explain_fixed(open_fixed_from_ml(t));
}
u_dependency* explain_fixed(const lar_term& t) {
template <typename T>
u_dependency* explain_fixed(const T& t) const {
u_dependency* dep = nullptr;
for (const auto& p : t) {
if (is_fixed(p.j())) {
u_dependency* bound_dep =
lra.get_bound_constraint_witnesses_for_column(p.j());
if (is_fixed(p.var())) {
u_dependency* bound_dep = lra.get_bound_constraint_witnesses_for_column(p.var());
dep = lra.join_deps(dep, bound_dep);
}
}
@ -1725,33 +1769,42 @@ namespace lp {
}
}
lia_move process_f() {
std_vector<unsigned> f_vector;
fill_f_vector(f_vector);
lia_move process_f(std_vector<unsigned>& f_vector) {
if (m_conflict_index != UINT_MAX) {
lra.stats().m_dio_rewrite_conflicts++;
return lia_move::conflict;
}
lia_move r;
do {
r = rewrite_eqs(f_vector);
if (lra.settings().get_cancel_flag()) {
return lia_move::undef;
}
if (r == lia_move::conflict || r == lia_move::undef) {
break;
}
SASSERT(m_new_fixed_columns.size() == 0);
} while (f_vector.size());
while (rewrite_eqs(f_vector)) {}
if (r == lia_move::conflict) {
if (m_conflict_index != UINT_MAX) {
lra.stats().m_dio_rewrite_conflicts++;
}
return lia_move::conflict;
}
TRACE("dio", print_S(tout));
return lia_move::undef;
}
lia_move process_f_and_tighten_terms() {
lia_move ret = process_f();
lia_move process_f_and_tighten_terms(std_vector<unsigned>& f_vector) {
lia_move ret = process_f(f_vector);
if (ret != lia_move::undef)
return ret;
TRACE("dioph_eq", print_S(tout););
TRACE("dio", print_S(tout););
ret = tighten_terms_with_S();
if (ret == lia_move::conflict) {
if (ret == lia_move::conflict)
lra.stats().m_dio_tighten_conflicts++;
return lia_move::conflict;
}
return ret;
}
@ -2035,7 +2088,7 @@ namespace lp {
unsigned j = p.first;
const auto it = m_columns_to_terms.find(j);
if (it == m_columns_to_terms.end()) {
TRACE("dioph_eq", tout << "column j" << j << " is not registered" << std::endl; tout << "the column belongs to the the following terms:"; for (unsigned tj : p.second) { tout << " " << tj; } tout << std::endl;);
TRACE("dio", tout << "column j" << j << " is not registered" << std::endl; tout << "the column belongs to the the following terms:"; for (unsigned tj : p.second) { tout << " " << tj; } tout << std::endl;);
return false;
}
@ -2051,7 +2104,7 @@ namespace lp {
unsigned j = p.first;
const auto it = c2t.find(j);
if (it == c2t.end()) {
TRACE("dioph_eq", tout << "should not be registered j " << j << std::endl;
TRACE("dio", tout << "should not be registered j " << j << std::endl;
lra.print_terms(tout););
return false;
}
@ -2087,22 +2140,22 @@ namespace lp {
public:
lia_move check() {
lra.stats().m_dio_calls++;
TRACE("dioph_eq", tout << lra.stats().m_dio_calls << std::endl;);
init();
lia_move ret = process_f_and_tighten_terms();
if (ret == lia_move::branch || ret == lia_move::conflict)
TRACE("dio", tout << lra.stats().m_dio_calls << std::endl;);
std_vector<unsigned> f_vector;
lia_move ret;
do {
init(f_vector);
ret = process_f_and_tighten_terms(f_vector);
} while(ret == lia_move::continue_with_check);
if (ret != lia_move::undef) {
return ret;
SASSERT(ret == lia_move::undef);
}
if (lra.stats().m_dio_calls % lra.settings().dio_branching_period() == 0) {
ret = branching_on_undef();
}
if (ret == lia_move::sat || ret == lia_move::conflict) {
return ret;
}
SASSERT(ret == lia_move::undef);
m_max_of_branching_iterations = (unsigned)m_max_of_branching_iterations / 2;
return lia_move::undef;
return ret;
}
private:
@ -2122,7 +2175,7 @@ namespace lp {
std::tuple<mpq, unsigned, int, unsigned> find_minimal_abs_coeff(unsigned ei) {
bool first = true;
mpq ahk;
unsigned k;
unsigned k = -1;
int k_sign;
mpq t;
for (const auto& p : m_e_matrix.m_rows[ei]) {
@ -2149,7 +2202,7 @@ namespace lp {
t.add_monomial(-k_sign * p.coeff(), p.j());
}
t.c() = -k_sign * eh.c();
TRACE("dioph_eq", tout << "subst_term:";
TRACE("dio", tout << "subst_term:";
print_term_o(t, tout) << std::endl;);
return t;
}
@ -2170,7 +2223,7 @@ namespace lp {
SASSERT(belongs_to_s(ei));
const auto& e = m_sum_of_fixed[ei];
SASSERT(j_sign_is_correct(ei, j, j_sign));
TRACE("dioph_eq", tout << "eliminate var:" << j << " by using:";
TRACE("dio", tout << "eliminate var:" << j << " by using:";
print_entry(ei, tout) << std::endl;);
auto& column = m_e_matrix.m_columns[j];
auto it =
@ -2201,16 +2254,16 @@ namespace lp {
SASSERT(c.var() != ei && entry_invariant(c.var()));
mpq coeff = m_e_matrix.get_val(c);
unsigned i = c.var();
TRACE("dioph_eq", tout << "before pivot entry:";
TRACE("dio", tout << "before pivot entry:";
print_entry(i, tout) << std::endl;);
m_sum_of_fixed[i] -= j_sign * coeff * e;
m_e_matrix.pivot_row_to_row_given_cell_with_sign(ei, c, j, j_sign);
// m_sum_of_fixed[i].m_l -= j_sign * coeff * e.m_l;
m_l_matrix.add_rows(-j_sign * coeff, ei, i);
TRACE("dioph_eq", tout << "after pivoting c_row:";
TRACE("dio", tout << "after pivoting c_row:";
print_entry(i, tout););
CTRACE(
"dioph_eq", !entry_invariant(i), tout << "invariant delta:"; {
"dio", !entry_invariant(i), tout << "invariant delta:"; {
print_term_o(get_term_from_entry(ei) -
fix_vars(open_ml(m_l_matrix.m_rows[ei])),
tout)
@ -2226,7 +2279,7 @@ namespace lp {
// matrix m_l_matrix is not changed since it is a substitution of a fresh variable
void eliminate_var_in_f_with_term(const lar_term& t, unsigned j, int j_sign) {
SASSERT(abs(t.get_coeff(j)).is_one());
TRACE("dioph_eq", tout << "eliminate var:" << j << " by using:";
TRACE("dio", tout << "eliminate var:" << j << " by using:";
print_lar_term_L(t, tout) << std::endl;);
auto& column = m_e_matrix.m_columns[j];
@ -2239,9 +2292,9 @@ namespace lp {
}
mpq coeff = m_e_matrix.get_val(c);
TRACE("dioph_eq", tout << "before pivot entry :"; print_entry(c.var(), tout) << std::endl;);
TRACE("dio", tout << "before pivot entry :"; print_entry(c.var(), tout) << std::endl;);
m_e_matrix.pivot_term_to_row_given_cell(t, c, j, j_sign);
TRACE("dioph_eq", tout << "after pivoting c_row:";
TRACE("dio", tout << "after pivoting c_row:";
print_entry(c.var(), tout););
SASSERT(entry_invariant(c.var()));
cell_to_process--;
@ -2273,24 +2326,33 @@ namespace lp {
}
bool entry_invariant(unsigned ei) const {
if (belongs_to_s(ei)) {
auto it = m_k2s.m_rev_map.find(ei);
SASSERT(it != m_k2s.m_rev_map.end());
unsigned j = it->second;
get_sign_in_e_row(ei, j);
}
if (lra.settings().get_cancel_flag())
return true;
for (const auto& p : m_e_matrix.m_rows[ei]) {
if (!p.coeff().is_int()) {
return false;
}
if (var_is_fresh(p.var()))
continue;
unsigned j = local_to_lar_solver(p.var());
if (is_fixed(j)) {
enable_trace("dio");
TRACE("dio", tout << "x" << j << "(local: " << "x" << p.var() << ") should not be fixed\nbad entry:"; print_entry(ei, tout) << "\n";);
return false;
}
}
bool ret =
term_to_lar_solver(remove_fresh_vars(get_term_from_entry(ei))) ==
fix_vars(open_ml(m_l_matrix.m_rows[ei]));
CTRACE("dioph_deb_eq", !ret,
term_o ls = term_to_lar_solver(remove_fresh_vars(get_term_from_entry(ei)));
mpq ls_val = get_term_value(ls);
if (!ls_val.is_zero()) {
std::cout << "ls_val is not zero\n";
return false;
}
bool ret = ls == fix_vars(open_ml(m_l_matrix.m_rows[ei]));
if (!ret) {
enable_trace("dio");
CTRACE("dio", !ret,
{
tout << "get_term_from_entry(" << ei << "):";
print_term_o(get_term_from_entry(ei), tout) << std::endl;
@ -2304,7 +2366,7 @@ namespace lp {
tout << "rs:";
print_term_o(fix_vars(open_ml(m_l_matrix.m_rows[ei])), tout) << std::endl;
});
}
return ret;
}
@ -2319,7 +2381,7 @@ namespace lp {
while (!q.empty()) {
unsigned xt = q.pop_front(); // xt is a fresh var
const lar_term& fresh_t = m_fresh_k2xt_terms.get_by_val(xt).first;
TRACE("dioph_eq", print_lar_term_L(fresh_t, tout););
TRACE("dio_remove_fresh", print_lar_term_L(fresh_t, tout););
SASSERT(fresh_t.get_coeff(xt).is_minus_one());
if (!t.contains(xt))
continue;
@ -2335,11 +2397,25 @@ namespace lp {
return t;
}
std::ostream& print_ml(const lar_term& ml, std::ostream& out) {
std::ostream& print_ml(const lar_term& ml, std::ostream& out) const {
term_o opened_ml = open_ml(ml);
return print_lar_term_L(opened_ml, out);
}
// collect only fixed variables in a term
template <typename T>
term_with_index open_fixed_from_ml(const T& ml) const {
term_with_index r;
for (const auto& v : ml) {
for (const auto & p : lra.get_term(v.var()).ext_coeffs()) {
if (lra.column_is_fixed(p.var()))
r.add(v.coeff() * p.coeff(), p.var());
}
}
return r;
}
template <typename T>
term_o open_ml(const T& ml) const {
term_o r;
@ -2349,7 +2425,7 @@ namespace lp {
return r;
}
void open_l_term_to_work_vector(unsigned ei, mpq& c) {
void open_l_term_to_espace(unsigned ei, mpq& c) {
m_espace.clear();
for (const auto& p : m_l_matrix.m_rows[ei]) {
const lar_term& t = lra.get_term(p.var());
@ -2364,16 +2440,14 @@ namespace lp {
}
}
// it clears the row, and puts the term in the work vector
void move_row_espace(unsigned ei) {
void copy_row_to_espace(unsigned ei) {
m_espace.clear();
auto& row = m_e_matrix.m_rows[ei];
for (const auto& cell : row)
m_espace.add(cell.coeff(), cell.var());
clear_e_row(ei);
}
// The idea is to remove this fresh definition when the row h changes.
// The idea is to be able remove this fresh definition when the row h changes.
// The row can change if it depends on the term that is deleted, or on a variable that becomes fixed/unfixed
// fr_j is a fresh variable
void register_var_in_fresh_defs(unsigned h, unsigned fr_j) {
@ -2420,14 +2494,14 @@ namespace lp {
}
std::ostream& print_entry(unsigned i, std::ostream& out,
bool print_dep = false, bool print_in_S = true) {
bool print_dep = false, bool print_in_S = true, bool print_column_info = false) const {
unsigned j = m_k2s.has_val(i) ? m_k2s.get_key(i) : UINT_MAX;
out << "entry " << i << ": ";
if (j != UINT_MAX)
out << "x" << j << " ";
out << "{\n";
print_term_o(get_term_from_entry(i), out << "\t") << ",\n";
// out << "\tstatus:" << (int)e.m_entry_status;
if (print_dep) {
auto l_term = l_term_from_row(i);
out << "\tm_l:{";
@ -2441,13 +2515,26 @@ namespace lp {
out << "in F\n";
}
else {
if (local_to_lar_solver(j) == UINT_MAX) {
out << "FRESH\n";
}
else if (print_in_S) {
if (print_in_S) {
out << "in S\n";
}
}
if (print_column_info) {
bool has_fresh = false;
for (const auto& p : m_e_matrix[i] ) {
if (var_is_fresh(p.var())) {
has_fresh = true;
out << "has fresh var:" << p.var() << "\n";
break;
}
}
if (!has_fresh) {
for (const auto& p : get_term_from_entry(i)) {
out << "\tlocal(x" << p.var() << ")";
lra.print_column_info(local_to_lar_solver(p.var()), out);
}
}
}
out << "}\n";
return out;
}
@ -2467,10 +2554,11 @@ namespace lp {
}
// this is the step 6 or 7 of the algorithm
// returns true if an equlity was rewritten and false otherwise
bool rewrite_eqs(std_vector<unsigned>& f_vector) {
// returns lia_move::conflict if a conflict was found, continue_with_check if some progress has been achieved,
// otherwise returns lia_move::undef
lia_move rewrite_eqs(std_vector<unsigned>& f_vector) {
if (f_vector.size() == 0)
return false;
return lia_move::undef;
unsigned h = -1, kh = 0; // the initial value of kh does not matter, assign to remove the warning
unsigned n = 0; // number of choices for a fresh variable
mpq min_ahk;
@ -2486,7 +2574,7 @@ namespace lp {
}
else {
m_conflict_index = ei;
return false;
return lia_move::conflict;
}
}
@ -2494,7 +2582,7 @@ namespace lp {
mpq gcd;
if (!normalize_e_by_gcd(ei, gcd)) {
m_conflict_index = ei;
return false;
return lia_move::conflict;
}
if (!gcd.is_one())
ahk /= gcd;
@ -2519,7 +2607,10 @@ namespace lp {
if (min_ahk.is_one() && h_markovich_number == 0)
break;
}
if (h == UINT_MAX) return false;
if (h == UINT_MAX) {
TRACE("dio", tout << "done - cannot find an entry to rewrite\n");
return lia_move::undef;
}
SASSERT(h == f_vector[ih]);
if (min_ahk.is_one()) {
TRACE("dioph_eq", tout << "push to S:\n"; print_entry(h, tout););
@ -2530,9 +2621,11 @@ namespace lp {
}
f_vector.pop_back();
}
else
else {
fresh_var_step(h, kh, min_ahk * mpq(kh_sign));
return true;
}
return lia_move::continue_with_check;
}
public:
@ -2541,23 +2634,22 @@ namespace lp {
for (auto ci : m_infeas_explanation) {
ex.push_back(ci.ci());
}
TRACE("dioph_eq", lra.print_expl(tout, ex););
TRACE("dio", lra.print_expl(tout, ex););
return;
}
SASSERT(ex.empty());
TRACE("dioph_eq", tout << "conflict:";
TRACE("dio", tout << "conflict:";
print_entry(m_conflict_index, tout, true) << std::endl;);
for (auto ci : lra.flatten(explain_fixed_in_meta_term(m_l_matrix.m_rows[m_conflict_index]))) {
ex.push_back(ci);
}
TRACE("dioph_eq", lra.print_expl(tout, ex););
TRACE("dio", lra.print_expl(tout, ex););
}
bool var_is_fresh(unsigned j) const {
bool ret = m_fresh_k2xt_terms.has_second_key(j);
SASSERT(!ret || m_var_register.local_to_external(j) == UINT_MAX);
return ret;
}
// needed for the template bound_analyzer_on_row.h
const lar_solver& lp() const { return lra; }
lar_solver& lp() {return lra;}
};
// Constructor definition
dioph_eq::dioph_eq(int_solver& lia) {

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

@ -188,7 +188,7 @@ namespace lp {
}
bool should_gomory_cut() {
return (!settings().dio_eqs() || settings().dio_enable_gomory_cuts())
return (!all_columns_are_integral() ||(!settings().dio_eqs() || settings().dio_enable_gomory_cuts()))
&& m_number_of_calls % settings().m_int_gomory_cut_period == 0;
}

203
src/math/lp/lar_solver.cpp
View file

@ -2509,6 +2509,24 @@ namespace lp {
// Otherwise the new asserted lower bound is is greater than the existing upper bound.
// dep is the reason for the new bound
void lar_solver::write_bound_lemma_to_file(unsigned j, bool is_low, const std::string & file_name, const std::string& location) const {
std::ofstream file(file_name);
if (!file.is_open()) {
// Handle file open error
std::cerr << "Failed to open file: " << file_name << std::endl;
return;
}
write_bound_lemma(j, is_low, location, file);
file.close();
if (file.fail()) {
std::cerr << "Error occurred while writing to file: " << file_name << std::endl;
} else {
std::cout << "Bound lemma written to " << file_name << std::endl;
}
}
void lar_solver::set_crossed_bounds_column_and_deps(unsigned j, bool lower_bound, u_dependency* dep) {
if (m_crossed_bounds_column != null_lpvar) return; // already set
SASSERT(m_crossed_bounds_deps == nullptr);
@ -2518,7 +2536,7 @@ namespace lp {
u_dependency* bdep = lower_bound? ul.lower_bound_witness() : ul.upper_bound_witness();
SASSERT(bdep != nullptr);
m_crossed_bounds_deps = m_dependencies.mk_join(bdep, dep);
insert_to_columns_with_changed_bounds(j);
TRACE("dio", tout << "crossed_bound_deps:\n"; print_explanation(tout, flatten(m_crossed_bounds_deps)) << "\n";);
}
void lar_solver::collect_more_rows_for_lp_propagation(){
@ -2539,6 +2557,189 @@ namespace lp {
return out;
}
// Helper function to format constants in SMT2 format
std::string format_smt2_constant(const mpq& val) {
if (val.is_neg()) {
// Negative constant - use unary minus operator
return std::string("(- ") + abs(val).to_string() + ")";
} else {
// Positive or zero constant - write directly
return val.to_string();
}
}
void lar_solver::write_bound_lemma(unsigned j, bool is_low, const std::string& location, std::ostream & out) const {
// Get the bound value and dependency
mpq bound_val;
bool is_strict = false;
u_dependency* bound_dep = nullptr;
// Get the appropriate bound info
if (is_low) {
if (!has_lower_bound(j, bound_dep, bound_val, is_strict)) {
out << "; Error: Variable " << j << " has no lower bound\n";
return;
}
} else {
if (!has_upper_bound(j, bound_dep, bound_val, is_strict)) {
out << "; Error: Variable " << j << " has no upper bound\n";
return;
}
}
// Start SMT2 file
out << "(set-info : \"generated at " << location;
out << " for " << (is_low ? "lower" : "upper") << " bound of variable " << j << ",";
out << " bound value: " << bound_val << (is_strict ? (is_low ? " < " : " > ") : (is_low ? " <= " : " >= ")) << "x" << j << "\")\n";
// Collect all variables used in dependencies
std::unordered_set<unsigned> vars_used;
vars_used.insert(j);
bool is_int = column_is_int(j);
// Linearize the dependencies
svector<constraint_index> deps;
m_dependencies.linearize(bound_dep, deps);
// Collect variables from constraints
for (auto ci : deps) {
const auto& c = m_constraints[ci];
for (const auto& p : c.coeffs()) {
vars_used.insert(p.second);
if (!column_is_int(p.second))
is_int = false;
}
}
// Collect variables from terms
std::unordered_set<unsigned> term_variables;
for (unsigned var : vars_used) {
if (column_has_term(var)) {
const lar_term& term = get_term(var);
for (const auto& p : term) {
term_variables.insert(p.j());
if (!column_is_int(p.j()))
is_int = false;
}
}
}
// Add term variables to vars_used
vars_used.insert(term_variables.begin(), term_variables.end());
if (is_int) {
out << "(set-logic QF_LIA)\n\n";
}
// Declare variables
out << "; Variable declarations\n";
for (unsigned var : vars_used) {
out << "(declare-const x" << var << " " << (column_is_int(var) ? "Int" : "Real") << ")\n";
}
out << "\n";
// Define term relationships
out << "; Term definitions\n";
for (unsigned var : vars_used) {
if (column_has_term(var)) {
const lar_term& term = get_term(var);
out << "(assert (= x" << var << " ";
if (term.size() == 0) {
out << "0";
} else {
if (term.size() > 1) out << "(+ ";
bool first = true;
for (const auto& p : term) {
if (first) first = false;
else out << " ";
if (p.coeff().is_one()) {
out << "x" << p.j();
} else {
out << "(* " << format_smt2_constant(p.coeff()) << " x" << p.j() << ")";
}
}
if (term.size() > 1) out << ")";
}
out << "))\n";
}
}
out << "\n";
// Add assertions for the dependencies
out << "; Bound dependencies\n";
for (auto ci : deps) {
const auto& c = m_constraints[ci];
out << "(assert ";
// Handle the constraint type and expression
auto k = c.kind();
// Normal constraint with variables
switch (k) {
case LE: out << "(<= "; break;
case LT: out << "(< "; break;
case GE: out << "(>= "; break;
case GT: out << "(> "; break;
case EQ: out << "(= "; break;
default: out << "(unknown-constraint-type "; break;
}
// Left-hand side (variables)
if (c.coeffs().size() == 1) {
// Single variable
auto p = *c.coeffs().begin();
if (p.first.is_one()) {
out << "x" << p.second << " ";
} else {
out << "(* " << format_smt2_constant(p.first) << " x" << p.second << ") ";
}
} else {
// Multiple variables - create a sum
out << "(+ ";
for (auto const& p : c.coeffs()) {
if (p.first.is_one()) {
out << "x" << p.second << " ";
} else {
out << "(* " << format_smt2_constant(p.first) << " x" << p.second << ") ";
}
}
out << ") ";
}
// Right-hand side (constant)
out << format_smt2_constant(c.rhs());
out << "))\n";
}
out << "\n";
// Now add the assertion that contradicts the bound
out << "; Negation of the derived bound\n";
if (is_low) {
if (is_strict) {
out << "(assert (<= x" << j << " " << format_smt2_constant(bound_val) << "))\n";
} else {
out << "(assert (< x" << j << " " << format_smt2_constant(bound_val) << "))\n";
}
} else {
if (is_strict) {
out << "(assert (>= x" << j << " " << format_smt2_constant(bound_val) << "))\n";
} else {
out << "(assert (> x" << j << " " << format_smt2_constant(bound_val) << "))\n";
}
}
out << "\n";
// Check sat and get model if available
out << "(check-sat)\n";
out << "(exit)\n";
}
} // namespace lp

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

@ -617,10 +617,11 @@ public:
}
inline bool column_has_term(lpvar j) const { return m_columns[j].term() != nullptr; }
std::ostream& print_column_info(unsigned j, std::ostream& out) const {
std::ostream& print_column_info(unsigned j, std::ostream& out, bool print_expl = false) const {
m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out);
if (column_has_term(j))
print_term_as_indices(get_term(j), out) << "\n";
if (print_expl)
display_column_explanation(out, j);
return out;
}
@ -630,10 +631,18 @@ public:
svector<unsigned> vs1, vs2;
m_dependencies.linearize(ul.lower_bound_witness(), vs1);
m_dependencies.linearize(ul.upper_bound_witness(), vs2);
if (!vs1.empty())
out << "lo: " << vs1;
if (!vs2.empty())
out << "hi: " << vs2;
if (!vs1.empty()) {
out << " lo:\n";
for (unsigned ci : vs1) {
display_constraint(out, ci) << "\n";
}
}
if (!vs2.empty()) {
out << " hi:\n";
for (unsigned ci : vs2) {
display_constraint(out, ci) << "\n";
}
}
if (!vs1.empty() || !vs2.empty())
out << "\n";
return out;
@ -716,6 +725,11 @@ public:
return 0;
return m_usage_in_terms[j];
}
void write_bound_lemma_to_file(unsigned j, bool is_low, const std::string & file_name, const std::string & location) const;
void write_bound_lemma(unsigned j, bool is_low, const std::string & location, std::ostream & out) const;
std::function<void (const indexed_uint_set& columns_with_changed_bound)> m_find_monics_with_changed_bounds_func = nullptr;
friend int_solver;
friend int_branch;

4
src/math/lp/lp_core_solver_base.h
View file

@ -436,7 +436,7 @@ public:
return out;
}
std::ostream& print_column_info(unsigned j, std::ostream & out) const {
std::ostream& print_column_info(unsigned j, std::ostream & out, const std::string& var_prefix = "x") const {
if (j >= m_lower_bounds.size()) {
out << "[" << j << "] is not present\n";
return out;
@ -445,7 +445,7 @@ public:
std::stringstream strm;
strm << m_x[j];
std::string j_val = strm.str();
out << "[" << j << "] " << std::setw(6) << " := " << j_val;
out << var_prefix << j << " = " << std::setw(6) << j_val;
if (m_basis_heading[j] >= 0)
out << " base ";
else

1
src/math/lp/lp_settings.cpp
View file

@ -35,4 +35,5 @@ void lp::lp_settings::updt_params(params_ref const& _p) {
m_dio_eqs = p.arith_lp_dio_eqs();
m_dio_enable_gomory_cuts = p.arith_lp_dio_cuts_enable_gomory();
m_dio_branching_period = p.arith_lp_dio_branching_period();
m_dump_bound_lemmas = p.arith_dump_bound_lemmas();
}

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

@ -259,7 +259,7 @@ private:
bool m_dio_enable_hnf_cuts = true;
unsigned m_dio_branching_period = 100; // do branching rarely
unsigned m_dio_report_branch_with_term_tigthening_period = 10000000; // period of reporting the branch with term tigthening
bool m_dump_bound_lemmas = false;
public:
bool print_external_var_name() const { return m_print_external_var_name; }
bool propagate_eqs() const { return m_propagate_eqs;}
@ -277,6 +277,8 @@ public:
return m_bound_propagation;
}
bool dump_bound_lemmas() { return m_dump_bound_lemmas; }
bool& bound_propagation() { return m_bound_propagation; }
lp_settings() : m_default_resource_limit(*this),

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

@ -239,6 +239,8 @@ struct numeric_pair {
void neg() { x.neg(); y.neg(); }
std::string to_string() const {
if (y.is_zero())
return T_to_string(x);
return std::string("(") + T_to_string(x) + ", " + T_to_string(y) + ")";
}

15
src/math/lp/static_matrix.h
View file

@ -93,15 +93,8 @@ public:
operator T () const { return m_matrix.get_elem(m_row, m_col); }
};
class ref_row {
const static_matrix & m_matrix;
unsigned m_row;
public:
ref_row(const static_matrix & m, unsigned row): m_matrix(m), m_row(row) {}
T operator[](unsigned col) const { return m_matrix.get_elem(m_row, col); }
};
public:
const auto & operator[](unsigned i) const { return m_rows[i]; }
const T & get_val(const column_cell & c) const {
return m_rows[c.var()][c.offset()].coeff();
@ -146,6 +139,11 @@ public:
void remove_element(std_vector<row_cell<T>> & row, row_cell<T> & elem_to_remove);
void remove_element(unsigned ei, row_cell<T> & elem_to_remove) {
remove_element(m_rows[ei], elem_to_remove);
}
void multiply_column(unsigned column, T const & alpha) {
for (auto & t : m_columns[column]) {
auto & r = m_rows[t.var()][t.offset()];
@ -452,7 +450,6 @@ public:
return column_container(j, *this);
}
ref_row operator[](unsigned i) const { return ref_row(*this, i);}
typedef T coefftype;
typedef X argtype;
};

1
src/smt/params/smt_params_helper.pyg
View file

@ -94,6 +94,7 @@ def_module_params(module_name='smt',
('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),
('arith.ignore_int', BOOL, False, 'treat integer variables as real'),
('arith.dump_lemmas', BOOL, False, 'dump arithmetic theory lemmas to files'),
('arith.dump_bound_lemmas', BOOL, False, 'dump linear solver bounds to files in smt2 format'),
('arith.greatest_error_pivot', BOOL, False, 'Pivoting strategy'),
('arith.eager_eq_axioms', BOOL, True, 'eager equality axioms'),
('arith.auto_config_simplex', BOOL, False, 'force simplex solver in auto_config'),