mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

change lar_terms to use column indices

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-06 11:51:06 -07:00
parent 3313590b95
commit c2e5cd78c8
13 changed files with 88 additions and 103 deletions

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

@ -109,7 +109,7 @@ public:
auto & row = m_data[adjust_row(i)];
lp_assert(row_is_initialized_correctly(row));
for (const auto & p : c) {
unsigned j = adjust_column(column_fix(p.var().index()));
unsigned j = adjust_column(column_fix(p.column().index()));
row[j] = sign * p.coeff();
}
}

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

@ -191,7 +191,8 @@ class create_cut {
void dump_coeff(std::ostream & out, const T& c) const {
out << "( * ";
dump_coeff_val(out, c.coeff());
out << " " << var_name(c.var().index()) << ")";
auto t = lia.lra.column2tv(c.column());
out << " " << var_name(t.id()) << ")";
}
std::ostream& dump_row_coefficients(std::ostream & out) const {
@ -221,9 +222,9 @@ class create_cut {
dump_declaration(out, p.var());
}
for (const auto& p : m_t) {
unsigned v = p.var().index();
if (lp::tv::is_term(v)) {
dump_declaration(out, v);
auto t = lia.lra.column2tv(p.column());
if (t.is_term()) {
dump_declaration(out, t.id());
}
}
}
@ -349,7 +350,6 @@ public:
// NSB code review: this is also used in nla_core.
// but it isn't consistent: when theory_lra accesses lar_solver::get_term, the term that is returned uses
// column indices, not terms.
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;
}

3
src/math/lp/hnf_cutter.cpp
View file

@ -50,7 +50,8 @@ namespace lp {
m_constraints_for_explanation.push_back(ci);
for (const auto &p : *t) {
m_var_register.add_var(p.var().index(), true); // hnf only deals with integral variables for now
auto tv = lia.lra.column2tv(p.column());
m_var_register.add_var(tv.id(), true); // hnf only deals with integral variables for now
mpq t = abs(ceil(p.coeff()));
if (t > m_abs_max)
m_abs_max = t;

4
src/math/lp/int_cube.cpp
View file

@ -86,7 +86,7 @@ namespace lp {
bool seen_minus = false;
bool seen_plus = false;
for(const auto & p : t) {
if (!lia.column_is_int(p.var().index()))
if (!lia.column_is_int(p.column()))
goto usual_delta;
const mpq & c = p.coeff();
if (c == one_of_type<mpq>()) {
@ -104,7 +104,7 @@ namespace lp {
usual_delta:
mpq delta = zero_of_type<mpq>();
for (const auto & p : t)
if (lia.column_is_int(p.var().index()))
if (lia.column_is_int(p.column()))
delta += abs(p.coeff());
delta *= mpq(1, 2);

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

@ -228,7 +228,7 @@ const lp_settings& int_solver::settings() const {
return lra.settings();
}
bool int_solver::column_is_int(unsigned j) const {
bool int_solver::column_is_int(column_index const& j) const {
return lra.column_is_int(j);
}

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

@ -82,7 +82,7 @@ public:
bool is_real(unsigned j) const;
const impq & lower_bound(unsigned j) const;
const impq & upper_bound(unsigned j) const;
bool column_is_int(unsigned j) const;
bool column_is_int(column_index const& j) const;
const impq & get_value(unsigned j) const;
bool at_lower(unsigned j) const;
bool at_upper(unsigned j) const;

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

@ -115,13 +115,13 @@ bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be,
} else {
lar_term const& t = get_term(be.m_j);
auto first_coeff = t.begin();
unsigned j = (*first_coeff).var().index();
unsigned j = (*first_coeff).column();
auto it = coeff_map.find(j);
if (it == coeff_map.end())
return false;
mpq ratio = it->second / (*first_coeff).coeff();
for (auto p : t) {
it = coeff_map.find(p.var().index());
it = coeff_map.find(p.column());
if (it == coeff_map.end())
return false;
if (p.coeff() * ratio != it->second)
@ -231,6 +231,7 @@ void lar_solver::explain_implied_bound(implied_bound & ib, lp_bound_propagator &
}
// lp_assert(implied_bound_is_correctly_explained(ib, explanation));
}
// here i is just the term index
bool lar_solver::term_is_used_as_row(unsigned i) const {
SASSERT(i < m_terms.size());
@ -246,7 +247,6 @@ void lar_solver::propagate_bounds_on_terms(lp_bound_propagator & bp) {
}
}
// goes over touched rows and tries to induce bounds
void lar_solver::propagate_bounds_for_touched_rows(lp_bound_propagator & bp) {
if (!use_tableau())
@ -423,7 +423,7 @@ void lar_solver::set_costs_to_zero(const lar_term& term) {
lp_assert(jset.is_empty());
for (const auto & p : term) {
unsigned j = p.var().index();
unsigned j = p.column();
rslv.m_costs[j] = zero_of_type<mpq>();
int i = rslv.m_basis_heading[j];
if (i < 0)
@ -454,7 +454,7 @@ void lar_solver::prepare_costs_for_r_solver(const lar_term & term) {
lp_assert(reduced_costs_are_zeroes_for_r_solver());
rslv.m_costs.resize(A_r().column_count(), zero_of_type<mpq>());
for (const auto & p : term) {
unsigned j = p.var().index();
unsigned j = p.column();
rslv.m_costs[j] = p.coeff();
if (rslv.m_basis_heading[j] < 0)
rslv.m_d[j] += p.coeff();
@ -681,7 +681,7 @@ void lar_solver::substitute_terms_in_linear_expression(const vector<std::pair<mp
const lar_term & term = * m_terms[tv::unmask_term(t.second)];
for (auto p : term){
register_monoid_in_map(coeffs, t.first * p.coeff() , p.var().index());
register_monoid_in_map(coeffs, t.first * p.coeff() , p.column());
}
}
}
@ -917,7 +917,7 @@ void lar_solver::fill_last_row_of_A_r(static_matrix<mpq, numeric_pair<mpq>> & A,
lp_assert(A.m_rows[last_row].size() == 0);
for (auto t : *ls) {
lp_assert(!is_zero(t.coeff()));
var_index j = t.var().index();
var_index j = t.column();
A.set(last_row, j, - t.coeff());
}
unsigned basis_j = A.column_count() - 1;
@ -1147,7 +1147,7 @@ bool lar_solver::has_value(var_index var, mpq& value) const {
lar_term const& t = get_term(var);
value = 0;
for (auto const& cv : t) {
impq const& r = get_column_value(cv.var().index());
impq const& r = get_column_value(cv.column());
if (!numeric_traits<mpq>::is_zero(r.y)) return false;
value += r.x * cv.coeff();
}
@ -1306,7 +1306,7 @@ std::ostream& lar_solver::print_term(lar_term const& term, std::ostream & out) c
out << " - ";
else if (val != numeric_traits<mpq>::one())
out << T_to_string(val);
out << this->get_variable_name(p.var().index());
out << this->get_variable_name(p.column());
}
return out;
}
@ -1530,7 +1530,7 @@ bool lar_solver::model_is_int_feasible() const {
bool lar_solver::term_is_int(const lar_term * t) const {
for (auto const p : *t)
if (! (column_is_int(p.var().index()) && p.coeff().is_int()))
if (! (column_is_int(p.column()) && p.coeff().is_int()))
return false;
return true;
}
@ -1691,19 +1691,9 @@ bool lar_solver::term_coeffs_are_ok(const vector<std::pair<mpq, var_index>> & co
}
#endif
void lar_solver::push_term(lar_term* t) {
// SASSERT(well_formed(*t));
m_terms.push_back(t);
}
bool lar_solver::well_formed(lar_term const& t) const {
for (auto const& ti : t) {
if (!ti.var().is_term() &&
column_corresponds_to_term(ti.var().index())) {
return false;
}
}
return true;
}
// terms
@ -1956,7 +1946,7 @@ void lar_solver::fill_last_row_of_A_d(static_matrix<double, double> & A, const l
for (auto t : *ls) {
lp_assert(!is_zero(t.coeff()));
var_index j = t.var().index();
var_index j = t.column();
A.set(last_row, j, -t.coeff().get_double());
}
@ -2257,7 +2247,7 @@ void lar_solver::fix_terms_with_rounded_columns() {
bool need_to_fix = false;
const lar_term & t = *m_terms[i];
for (const auto & p : t) {
if (m_incorrect_columns.contains(p.var().index())) {
if (m_incorrect_columns.contains(p.column())) {
need_to_fix = true;
break;
}
@ -2274,7 +2264,7 @@ void lar_solver::fix_terms_with_rounded_columns() {
bool lar_solver::sum_first_coords(const lar_term& t, mpq & val) const {
val = zero_of_type<mpq>();
for (const auto & c : t) {
const auto & x = m_mpq_lar_core_solver.m_r_x[c.var().index()];
const auto & x = m_mpq_lar_core_solver.m_r_x[c.column()];
if (!is_zero(x.y))
return false;
val += x.x * c.coeff();

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

@ -60,7 +60,7 @@ class lar_solver : public column_namer {
size_t seed = 0;
int i = 0;
for (const auto p : t) {
hash_combine(seed, p.var().index());
hash_combine(seed, (unsigned)p.column());
hash_combine(seed, p.coeff());
if (i++ > 10)
break;
@ -125,15 +125,11 @@ public:
static bool valid_index(unsigned j){ return static_cast<int>(j) >= 0;}
bool column_is_int(unsigned j) const;
bool column_value_is_int(unsigned j) const {
return m_mpq_lar_core_solver.m_r_x[j].is_int();
}
bool column_is_int(column_index const& j) const { return column_is_int((unsigned)j); }
const impq& get_column_value(unsigned j) const {
return m_mpq_lar_core_solver.m_r_x[j];
}
bool column_is_int(unsigned j) const;
bool column_value_is_int(unsigned j) const { return m_mpq_lar_core_solver.m_r_x[j].is_int(); }
const impq& get_column_value(unsigned j) const { return m_mpq_lar_core_solver.m_r_x[j]; }
void set_column_value(unsigned j, const impq& v) {
m_mpq_lar_core_solver.m_r_x[j] = v;
@ -583,23 +579,9 @@ public:
return m_columns_to_ul_pairs()[j].lower_bound_witness();
}
// NSB code review - seems superfluous to translate back and forth because
// get_term(..) that is exposed over API does not ensure that columns that
// are based on terms are translated back to term indices.
// would be better to have consistent typing, either lar_term uses cv (and not tv)
// or they are created to use tv consistently.
void subs_term_columns(lar_term& t) {
svector<std::pair<unsigned,unsigned>> columns_to_subs;
for (const auto & m : t) {
unsigned tj = adjust_column_index_to_term_index(m.var().index());
if (tj == m.var().index()) continue;
columns_to_subs.push_back(std::make_pair(m.var().index(), tj));
}
for (const auto & p : columns_to_subs) {
t.subst_index(p.first, p.second);
}
tv column2tv(column_index const& c) const {
return tv::raw(adjust_column_index_to_term_index(c));
}
std::ostream& print_column_info(unsigned j, std::ostream& out) const {
m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out);

9
src/math/lp/lar_term.h
View file

@ -123,8 +123,7 @@ public:
const mpq & m_coeff;
public:
ival(unsigned var, const mpq & val) : m_var(var), m_coeff(val) { }
unsigned raw() const { return m_var; }
tv var() const { return tv::raw(m_var); }
column_index column() const { return column_index(m_var); }
const mpq & coeff() const { return m_coeff; }
};
@ -143,13 +142,13 @@ public:
lpvar min_var = -1;
mpq c;
for (const auto & p : *this) {
if (p.var().index() < min_var) {
min_var = p.var().index();
if (p.column() < min_var) {
min_var = p.column();
}
}
lar_term r;
for (const auto & p : *this) {
if (p.var().index() == min_var) {
if (p.column() == min_var) {
return p.coeff().is_one();
}
}

20
src/math/lp/lp_types.h
View file

@ -21,6 +21,11 @@ Revision History:
#include <sstream>
namespace nla {
class core;
}
namespace lp {
typedef unsigned var_index;
typedef unsigned constraint_index;
@ -62,8 +67,23 @@ public:
}
};
class column_index {
unsigned m_index;
friend class lar_solver;
friend class lar_term;
friend nla::core;
operator unsigned() const { return m_index; }
public:
column_index(unsigned j): m_index(j) {}
unsigned index() const { return m_index; }
};
}
inline std::ostream& operator<<(std::ostream& out, lp::tv const& t) {
return out << (t.is_term() ? "t":"j") << t.id() << "\n";
}

30
src/math/lp/nla_core.cpp
View file

@ -50,7 +50,7 @@ bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const
rational core::value(const lp::lar_term& r) const {
rational ret(0);
for (const auto & t : r) {
ret += t.coeff() * val(t.var().index());
ret += t.coeff() * val(t.column());
}
return ret;
}
@ -58,7 +58,7 @@ rational core::value(const lp::lar_term& r) const {
lp::lar_term core::subs_terms_to_columns(const lp::lar_term& t) const {
lp::lar_term r;
for (const auto& p : t) {
lpvar j = p.var().index();
lpvar j = p.column();
if (lp::tv::is_term(j))
j = m_lar_solver.map_term_index_to_column_index(j);
r.add_monomial(p.coeff(), j);
@ -323,25 +323,25 @@ bool core:: explain_coeff_lower_bound(const lp::lar_term::ival& p, rational& bou
SASSERT(!a.is_zero());
unsigned c; // the index for the lower or the upper bound
if (a.is_pos()) {
unsigned c = m_lar_solver.get_column_lower_bound_witness(p.var().index());
unsigned c = m_lar_solver.get_column_lower_bound_witness(p.column());
if (c + 1 == 0)
return false;
bound = a * m_lar_solver.get_lower_bound(p.var().index()).x;
bound = a * m_lar_solver.get_lower_bound(p.column()).x;
e.add(c);
return true;
}
// a.is_neg()
c = m_lar_solver.get_column_upper_bound_witness(p.var().index());
c = m_lar_solver.get_column_upper_bound_witness(p.column());
if (c + 1 == 0)
return false;
bound = a * m_lar_solver.get_upper_bound(p.var().index()).x;
bound = a * m_lar_solver.get_upper_bound(p.column()).x;
e.add(c);
return true;
}
bool core::explain_coeff_upper_bound(const lp::lar_term::ival& p, rational& bound, lp::explanation& e) const {
const rational& a = p.coeff();
lpvar j = p.var().is_term()? m_lar_solver.map_term_index_to_column_index(p.var().index()) : p.var().index();
lpvar j = p.column();
SASSERT(!a.is_zero());
unsigned c; // the index for the lower or the upper bound
if (a.is_neg()) {
@ -426,7 +426,6 @@ bool core:: explain_by_equiv(const lp::lar_term& t, lp::explanation& e) const {
void core::mk_ineq(lp::lar_term& t, llc cmp, const rational& rs) {
TRACE("nla_solver_details", m_lar_solver.print_term_as_indices(t, tout << "t = "););
if (!explain_ineq(t, cmp, rs)) {
m_lar_solver.subs_term_columns(t);
current_lemma().push_back(ineq(cmp, t, rs));
CTRACE("nla_solver", ineq_holds(ineq(cmp, t, rs)), print_ineq(ineq(cmp, t, rs), tout) << "\n";);
SASSERT(!ineq_holds(ineq(cmp, t, rs)));
@ -435,7 +434,6 @@ void core::mk_ineq(lp::lar_term& t, llc cmp, const rational& rs) {
void core::mk_ineq_no_expl_check(lp::lar_term& t, llc cmp, const rational& rs) {
TRACE("nla_solver_details", m_lar_solver.print_term_as_indices(t, tout << "t = "););
m_lar_solver.subs_term_columns(t);
current_lemma().push_back(ineq(cmp, t, rs));
CTRACE("nla_solver", ineq_holds(ineq(cmp, t, rs)), print_ineq(ineq(cmp, t, rs), tout) << "\n";);
SASSERT(!ineq_holds(ineq(cmp, t, rs)));
@ -681,7 +679,7 @@ std::ostream & core::print_ineqs(const lemma& l, std::ostream & out) const {
print_ineq(in, out);
if (i + 1 < l.ineqs().size()) out << " or ";
for (const auto & p: in.m_term)
vars.insert(p.var().index());
vars.insert(p.column());
}
out << std::endl;
for (lpvar j : vars) {
@ -864,9 +862,9 @@ bool core:: is_octagon_term(const lp::lar_term& t, bool & sign, lpvar& i, lpvar
return false;
}
if (i == static_cast<lpvar>(-1))
i = p.var().index();
i = p.column();
else
j = p.var().index();
j = p.column();
}
SASSERT(j != static_cast<unsigned>(-1));
sign = (seen_minus && seen_plus)? false : true;
@ -987,7 +985,7 @@ std::unordered_set<lpvar> core::collect_vars(const lemma& l) const {
for (const auto& i : current_lemma().ineqs()) {
for (const auto& p : i.term()) {
insert_j(p.var().index());
insert_j(p.column());
}
}
for (const auto& p : current_expl()) {
@ -1754,9 +1752,9 @@ std::unordered_set<lpvar> core::get_vars_of_expr_with_opening_terms(const nex *e
if (ls.column_corresponds_to_term(j)) {
const auto& t = m_lar_solver.get_term(lp::tv::raw(ls.local_to_external(j)));
for (auto p : t) {
if (ret.find(p.var().index()) == ret.end()) {
added.push_back(p.var().index());
ret.insert(p.var().index());
if (ret.find(p.column()) == ret.end()) {
added.push_back(p.column());
ret.insert(p.column());
}
}
}

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

@ -357,14 +357,14 @@ public:
// we use the form -it + 1 = 0
m_work_vector.set_value(one_of_type<T>(), bj);
for (auto p : row) {
m_work_vector.set_value(-p.coeff(), p.var().index());
m_work_vector.set_value(-p.coeff(), p.column().index());
// but take care of the basis 1 later
}
// now iterate with pivoting
fill_last_row_with_pivoting_loop_block(bj, basis_heading);
for (auto p : row) {
fill_last_row_with_pivoting_loop_block(p.var().index(), basis_heading);
fill_last_row_with_pivoting_loop_block(p.column().index(), basis_heading);
}
lp_assert(m_work_vector.is_OK());
unsigned last_row = row_count() - 1;

37
src/smt/theory_lra.cpp
View file

@ -1523,7 +1523,7 @@ public:
if (t.is_term()) {
const lp::lar_term& term = lp().get_term(t);
for (const auto & i: term) {
m_todo_terms.push_back(std::make_pair(i.var(), coeff * i.coeff()));
m_todo_terms.push_back(std::make_pair(lp().column2tv(i.column()), coeff * i.coeff()));
}
}
else {
@ -1555,11 +1555,12 @@ public:
if (t2.is_term()) {
const lp::lar_term& term = lp().get_term(t2);
for (const auto & i : term) {
if (m_variable_values.count(i.var().index()) > 0) {
result += m_variable_values[i.var().index()] * coeff * i.coeff();
auto tv = lp().column2tv(i.column());
if (m_variable_values.count(tv.index()) > 0) {
result += m_variable_values[tv.index()] * coeff * i.coeff();
}
else {
m_todo_terms.push_back(std::make_pair(i.var(), coeff * i.coeff()));
m_todo_terms.push_back(std::make_pair(tv, coeff * i.coeff()));
}
}
}
@ -1955,7 +1956,7 @@ public:
expr_ref t(m);
expr_ref_vector ts(m);
for (auto const& p : term) {
auto ti = p.var();
auto ti = lp().column2tv(p.column());
if (ti.is_term()) {
ts.push_back(multerm(p.coeff(), term2expr(lp().get_term(ti))));
}
@ -1997,7 +1998,7 @@ public:
lp().print_term(term, out << "bound: ");
out << (upper?" <= ":" >= ") << k << "\n";
for (auto const& p : term) {
auto ti = p.var();
auto ti = lp().column2tv(p.column());
out << p.coeff() << " * ";
if (ti.is_term()) {
lp().print_term(lp().get_term(ti), out) << "\n";
@ -2798,7 +2799,7 @@ public:
m_todo_vars.pop_back();
lp::lar_term const& term = lp().get_term(ti);
for (auto const& p : term) {
lp::tv wi = p.var();
lp::tv wi = lp().column2tv(p.column());
if (wi.is_term()) {
m_todo_vars.push_back(wi);
}
@ -2824,7 +2825,7 @@ public:
m_todo_vars.pop_back();
lp::lar_term const& term = lp().get_term(ti);
for (auto const& coeff : term) {
auto wi = coeff.var();
auto wi = lp().column2tv(coeff.column());
if (wi.is_term()) {
m_todo_vars.push_back(wi);
}
@ -2914,7 +2915,7 @@ public:
SASSERT(ti.is_term());
lp::lar_term const& term = m_solver->get_term(ti);
for (auto const mono : term) {
auto wi = mono.var();
auto wi = lp().column2tv(mono.column());
lp::constraint_index ci;
rational value;
bool is_strict;
@ -3377,7 +3378,7 @@ public:
m_nra->am().set(r1, c1.to_mpq());
m_nra->am().add(r, r1, r);
for (auto const & arg : term) {
auto wi = arg.var();
auto wi = lp().column2tv(arg.column());
c1 = arg.coeff() * wcoeff;
if (wi.is_term()) {
m_todo_terms.push_back(std::make_pair(wi, c1));
@ -3658,23 +3659,17 @@ public:
TRACE("arith", lp().print_term(term, tout) << "\n";);
for (const auto & ti : term) {
theory_var w;
if (ti.var().is_term()) {
lp::lar_term const& term1 = lp().get_term(ti.var());
auto tv = lp().column2tv(ti.column());
if (tv.is_term()) {
lp::lar_term const& term1 = lp().get_term(tv);
rational coeff2 = coeff * ti.coeff();
term2coeffs(term1, coeffs, coeff2);
continue;
}
else if (lp().column_corresponds_to_term(ti.var().index())) {
lp::tv t = lp::tv::term(ti.var().index());
lp::lar_term const& term1 = lp().get_term(t);
rational coeff2 = coeff * ti.coeff();
term2coeffs(term1, coeffs, coeff2);
continue;
}
else {
w = lp().local_to_external(ti.var().index());
w = lp().local_to_external(tv.id());
SASSERT(w >= 0);
TRACE("arith", tout << (ti.var().index()) << ": " << w << "\n";);
TRACE("arith", tout << (tv.id()) << ": " << w << "\n";);
}
rational c0(0);
coeffs.find(w, c0);