diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h
index 35e3bb6ed..5af864220 100644
--- a/src/math/lp/bound_analyzer_on_row.h
+++ b/src/math/lp/bound_analyzer_on_row.h
@@ -93,39 +93,17 @@ private:
}
bool bound_is_available(unsigned j, bool lower_bound) {
- return (lower_bound && lower_bound_is_available(j)) ||
- (!lower_bound && upper_bound_is_available(j));
- }
-
- bool upper_bound_is_available(unsigned j) const {
- switch (m_bp.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 (m_bp.get_column_type(j)) {
- case column_type::fixed:
- case column_type::boxed:
- case column_type::lower_bound:
- return true;
- default:
- return false;
- }
+ return (lower_bound && m_bp.lower_bound_is_available(j)) ||
+ (!lower_bound && m_bp.upper_bound_is_available(j));
}
const impq & ub(unsigned j) const {
- lp_assert(upper_bound_is_available(j));
+ lp_assert(m_bp.upper_bound_is_available(j));
return m_bp.get_upper_bound(j);
}
const impq & lb(unsigned j) const {
- lp_assert(lower_bound_is_available(j));
+ lp_assert(m_bp.lower_bound_is_available(j));
return m_bp.get_lower_bound(j);
}
@@ -305,9 +283,8 @@ private:
void limit_j(unsigned bound_j, const mpq& u, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict){
- lar_solver* lar = & this->m_bp.lp();
unsigned row_index = this->m_row_index;
- auto explain = [lar, bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index]() { return explain_bound_on_var_on_coeff(lar, bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index); };
+ auto explain = [bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index](lar_solver& s) { return explain_bound_on_var_on_coeff(s, bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index); };
m_bp.add_bound(u, bound_j, is_lower_bound, strict, explain );
}
@@ -341,22 +318,22 @@ private:
break;
}
}
- static u_dependency* explain_bound_on_var_on_coeff(lar_solver* lar, unsigned bound_j, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict, unsigned row_index) {
+ static u_dependency* explain_bound_on_var_on_coeff(lar_solver& lar, unsigned bound_j, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict, unsigned row_index) {
int bound_sign = (is_lower_bound ? 1 : -1);
int j_sign = (coeff_before_j_is_pos ? 1 : -1) * bound_sign;
if (tv::is_term(bound_j))
- bound_j = lar->map_term_index_to_column_index(bound_j);
+ bound_j = lar.map_term_index_to_column_index(bound_j);
u_dependency* ret = nullptr;
- for (auto const& r : lar->get_row(row_index)) {
+ for (auto const& r : lar.get_row(row_index)) {
unsigned j = r.var();
if (j == bound_j)
continue;
mpq const& a = r.coeff();
int a_sign = is_pos(a) ? 1 : -1;
int sign = j_sign * a_sign;
- u_dependency* witness = sign > 0 ? lar->get_column_upper_bound_witness(j) : lar->get_column_lower_bound_witness(j);
- ret = lar->join_deps(ret, witness);
+ u_dependency* witness = sign > 0 ? lar.get_column_upper_bound_witness(j) : lar.get_column_lower_bound_witness(j);
+ ret = lar.join_deps(ret, witness);
}
return ret;
}
diff --git a/src/math/lp/implied_bound.h b/src/math/lp/implied_bound.h
index 2e7fcbbcb..0df1f4f60 100644
--- a/src/math/lp/implied_bound.h
+++ b/src/math/lp/implied_bound.h
@@ -20,18 +20,24 @@ Revision History:
#pragma once
#include "math/lp/lp_settings.h"
#include "math/lp/lar_constraints.h"
+#include "math/lp/lar_solver.h"
namespace lp {
class implied_bound {
public:
mpq m_bound;
- unsigned m_j; // the column for which the bound has been found
+ // It is either the column for which the bound has been found, or,
+ // in the case the column was created as
+ // the slack variable to a term, it is the term index.
+ // It is the same index that was returned by lar_solver::add_var(), or
+ // by lar_solver::add_term()
+ unsigned m_j;
bool m_is_lower_bound;
bool m_strict;
private:
- std::function<u_dependency*(void)> m_explain_bound = nullptr;
+ std::function<u_dependency*(lar_solver&)> m_explain_bound = nullptr;
public:
- u_dependency* explain() const { return m_explain_bound(); }
- void set_explain(std::function<u_dependency*(void)> f) { m_explain_bound = f; }
+ u_dependency* explain(lar_solver& s) const { return m_explain_bound(s); }
+ void set_explain(std::function<u_dependency*(lar_solver&)> f) { m_explain_bound = f; }
lconstraint_kind kind() const {
lconstraint_kind k = m_is_lower_bound? GE : LE;
if (m_strict)
@@ -43,7 +49,7 @@ class implied_bound {
unsigned j,
bool is_lower_bound,
bool is_strict,
- std::function<u_dependency*(void)> get_dep):
+ std::function<u_dependency*(lar_solver&)> get_dep):
m_bound(a),
m_j(j),
m_is_lower_bound(is_lower_bound),
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 7d16c7b63..50e9de7a3 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -311,7 +311,7 @@ class lar_solver : public column_namer {
template <typename T>
void explain_implied_bound(const implied_bound& ib, lp_bound_propagator<T>& bp) {
- u_dependency* dep = ib.explain();
+ u_dependency* dep = ib.explain(*this);
for (auto ci : flatten(dep))
bp.consume(mpq(1), ci); // TODO: flatten should provid the coefficients
/*
diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index 7ee647200..c67e99651 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -39,8 +39,28 @@ class lp_bound_propagator {
}
return x != UINT_MAX;
}
-
-
+public:
+ 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;
+ }
+ }
+private:
void try_add_equation_with_internal_fixed_tables(unsigned r1) {
unsigned v1, v2;
if (!only_one_nfixed(r1, v1))
@@ -119,11 +139,11 @@ class lp_bound_propagator {
}
void add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var) {
- add_lower_bound_monic(monic_var, mpq(0), false, [&](){return lp().get_bound_constraint_witnesses_for_column(zero_var);});
- add_upper_bound_monic(monic_var, mpq(0), false, [&](){return lp().get_bound_constraint_witnesses_for_column(zero_var);});
+ add_lower_bound_monic(monic_var, mpq(0), false, [zero_var](lar_solver& s){return s.get_bound_constraint_witnesses_for_column(zero_var);});
+ add_upper_bound_monic(monic_var, mpq(0), false, [zero_var](lar_solver& s){return s.get_bound_constraint_witnesses_for_column(zero_var);});
}
- void add_lower_bound_monic(lpvar monic_var, const mpq& v, bool is_strict, std::function<u_dependency* ()> explain_dep) {
+ void add_lower_bound_monic(lpvar monic_var, const mpq& v, bool is_strict, std::function<u_dependency* (lar_solver&)> explain_dep) {
unsigned k;
if (!try_get_value(m_improved_lower_bounds, monic_var, k)) {
m_improved_lower_bounds[monic_var] = m_ibounds.size();
@@ -137,7 +157,7 @@ class lp_bound_propagator {
}
}
- void add_upper_bound_monic(lpvar monic_var, const mpq& bound_val, bool is_strict, std::function <u_dependency* ()> explain_bound) {
+ void add_upper_bound_monic(lpvar monic_var, const mpq& bound_val, bool is_strict, std::function <u_dependency* (lar_solver&)> explain_bound) {
unsigned k;
if (!try_get_value(m_improved_upper_bounds, monic_var, k)) {
m_improved_upper_bounds[monic_var] = m_ibounds.size();
@@ -160,47 +180,54 @@ class lp_bound_propagator {
if (zero_var != null_lpvar) {
add_bounds_for_zero_var(monic_var, zero_var);
} else {
- if (non_fixed != null_lpvar && get_column_type(non_fixed) == column_type::free_column) return;
rational k = rational(1);
for (auto v : vars)
if (v != non_fixed) {
k *= lp().get_column_value(v).x;
if (k.is_big()) return;
}
- u_dependency* dep;
- lp::mpq bound_value;
+ lp::impq bound_value;
bool is_strict;
if (non_fixed != null_lpvar) {
- if (this->lp().has_lower_bound(non_fixed, dep, bound_value, is_strict)) {
+ if (lower_bound_is_available(non_fixed)) {
+ bound_value = lp().column_lower_bound(non_fixed);
+ is_strict = !bound_value.y.is_zero();
if (k.is_pos())
- add_lower_bound_monic(monic_var, k * bound_value, is_strict, [&]() { return dep; });
+ add_lower_bound_monic(monic_var, k * bound_value.x, is_strict , [non_fixed](lar_solver& s) { return s.get_column_lower_bound_witness(non_fixed); });
else
- add_upper_bound_monic(monic_var, k * bound_value, is_strict, [&]() {return dep;});
+ add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, [non_fixed](lar_solver& s) {return s.get_column_lower_bound_witness(non_fixed);});
}
- if (this->lp().has_upper_bound(non_fixed, dep, bound_value, is_strict)) {
+ if (upper_bound_is_available(non_fixed)) {
+ bound_value = lp().column_upper_bound(non_fixed);
+ is_strict = !bound_value.y.is_zero();
if (k.is_neg())
- add_lower_bound_monic(monic_var, k * bound_value, is_strict, [&]() {return dep;});
+ add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, [non_fixed](lar_solver& s) {return s.get_column_upper_bound_witness(non_fixed);});
else
- add_upper_bound_monic(monic_var, k * bound_value, is_strict, [&]() {return dep;});
+ add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, [non_fixed](lar_solver& s) {return s.get_column_upper_bound_witness(non_fixed);});
}
- if (this->lp().has_lower_bound(monic_var, dep, bound_value, is_strict)) {
+ if (lower_bound_is_available(monic_var)) {
+ bound_value = lp().column_lower_bound(monic_var);
+ is_strict = !bound_value.y.is_zero();
if (k.is_pos())
- add_lower_bound_monic(non_fixed, bound_value / k, is_strict, [&]() {return dep;});
+ add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, [monic_var](lar_solver& s) {return s.get_column_lower_bound_witness(monic_var);});
else
- add_upper_bound_monic(non_fixed, bound_value / k, is_strict, [&]() {return dep;});
+ add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, [monic_var](lar_solver & s) {return s.get_column_lower_bound_witness(monic_var);});
}
- if (this->lp().has_upper_bound(monic_var, dep, bound_value, is_strict)) {
+ if (upper_bound_is_available(monic_var)) {
+ bound_value = lp().column_upper_bound(monic_var);
+ is_strict = !bound_value.y.is_zero();
if (k.is_neg())
- add_lower_bound_monic(non_fixed, bound_value / k, is_strict, [&]() {return dep;});
+ add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, [monic_var](lar_solver& s) {return s.get_column_upper_bound_witness(monic_var);});
else
- add_upper_bound_monic(non_fixed, bound_value / k, is_strict, [&]() {return dep;});
+ add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, [monic_var](lar_solver & s) {return s.get_column_upper_bound_witness(monic_var);});
}
+
} else { // all variables are fixed
- add_lower_bound_monic(monic_var, k, false, [&](){return lp().get_bound_constraint_witnesses_for_columns(vars);});
- add_upper_bound_monic(monic_var, k, false, [&](){return lp().get_bound_constraint_witnesses_for_columns(vars);});
+ add_lower_bound_monic(monic_var, k, false, [vars](lar_solver& s){return s.get_bound_constraint_witnesses_for_columns(vars);});
+ add_upper_bound_monic(monic_var, k, false, [vars](lar_solver& s){return s.get_bound_constraint_witnesses_for_columns(vars);});
}
}
}
@@ -233,7 +260,7 @@ class lp_bound_propagator {
return (*m_column_types)[j] == column_type::fixed && get_lower_bound(j).y.is_zero();
}
- void add_bound(mpq const& v, unsigned j, bool is_low, bool strict, std::function<u_dependency* ()> explain_bound) {
+ void add_bound(mpq const& v, unsigned j, bool is_low, bool strict, std::function<u_dependency* (lar_solver&)> explain_bound) {
j = m_imp.lp().column_to_reported_index(j);
lconstraint_kind kind = is_low ? GE : LE;
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index e4bec83cc..346fbb7a9 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -253,7 +253,7 @@ namespace arith {
first = false;
reset_evidence();
m_explanation.clear();
- be.explain();
+ be.explain(lp());
}
CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";);
updt_unassigned_bounds(v, -1);