From 07354915572e6b99d9820e4a6a975714d99554cb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 4 Apr 2020 14:27:56 -0700
Subject: [PATCH] path fix #3747, this patches incoherent behavior of terms /
ival from lar_solver. The variables occurring in terms are mapped to columns
and not as original variables/terms. theory_lra has to interact with the
column_corresponds_to_term test instead of relying on the terms themselves
carrying the relevant information
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/math/lp/lar_solver.cpp | 24 +++++++++++++++++++-----
src/math/lp/lar_solver.h | 2 ++
src/math/lp/lp_types.h | 4 ++++
src/smt/theory_lra.cpp | 12 ++++++++++--
4 files changed, 35 insertions(+), 7 deletions(-)
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 7e9795a06..f7a1c1a19 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -192,10 +192,12 @@ void lar_solver::calculate_implied_bounds_for_row(unsigned i, lp_bound_propagato
}
unsigned lar_solver::adjust_column_index_to_term_index(unsigned j) const {
- if (tv::is_term(j))
- return j;
- unsigned ext_var_or_term = m_var_register.local_to_external(j);
- return !tv::is_term(ext_var_or_term) ? j : ext_var_or_term;
+ if (!tv::is_term(j)) {
+ unsigned ext_var_or_term = m_var_register.local_to_external(j);
+ TRACE("arith", tout << j << " " << ext_var_or_term << "\n";);
+ j = !tv::is_term(ext_var_or_term) ? j : ext_var_or_term;
+ }
+ return j;
}
unsigned lar_solver::map_term_index_to_column_index(unsigned j) const {
@@ -1689,9 +1691,20 @@ 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
bool lar_solver::all_vars_are_registered(const vector<std::pair<mpq, var_index>> & coeffs) {
@@ -2374,10 +2387,11 @@ std::pair<constraint_index, constraint_index> lar_solver::add_equality(lpvar j,
if (tv::is_term(k))
k = map_term_index_to_column_index(k);
-
+
coeffs.push_back(std::make_pair(mpq(1),j));
coeffs.push_back(std::make_pair(mpq(-1),k));
unsigned term_index = add_term(coeffs, UINT_MAX); // UINT_MAX is the external null var
+
if (get_column_value(j) != get_column_value(k))
set_status(lp_status::UNKNOWN);
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 302c9df08..88c4cab81 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -147,6 +147,8 @@ public:
bool column_is_fixed(unsigned j) const;
bool column_is_free(unsigned j) const;
+
+ bool well_formed(lar_term const& t) const;
public:
// init region
diff --git a/src/math/lp/lp_types.h b/src/math/lp/lp_types.h
index 38286eb7b..b8fea2ded 100644
--- a/src/math/lp/lp_types.h
+++ b/src/math/lp/lp_types.h
@@ -54,3 +54,7 @@ public:
};
}
+
+inline std::ostream& operator<<(lp::tv const& t, std::ostream& out) {
+ return out << (t.is_term() ? "t":"j") << t.id() << "\n";
+}
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 20befd474..efcef6b2f 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3644,18 +3644,26 @@ public:
}
void term2coeffs(lp::lar_term const& term, u_map<rational>& coeffs, rational const& coeff) {
+ TRACE("arith", lp().print_term(term, tout) << "\n";);
for (const auto & ti : term) {
theory_var w;
if (ti.var().is_term()) {
- //w = m_term_index2theory_var.get(lp::tv::unmask_term(ti.m_key), null_theory_var);
- //if (w == null_theory_var) // if extracting expressions directly from nested term
lp::lar_term const& term1 = lp().get_term(ti.var().index());
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.index());
+ rational coeff2 = coeff * ti.coeff();
+ term2coeffs(term1, coeffs, coeff2);
+ continue;
+ }
else {
w = lp().local_to_external(ti.var().index());
+ SASSERT(w >= 0);
+ TRACE("arith", tout << (ti.var().index()) << ": " << w << "\n";);
}
rational c0(0);
coeffs.find(w, c0);