From b102710b2f987f22cdf53ba5b420aa2d1f2b1f77 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 12 Feb 2019 12:12:38 -0800
Subject: [PATCH] map term indices to columns when test checking lemmas

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/util/lp/lar_solver.cpp |  5 +++++
 src/util/lp/lar_solver.h   |  2 ++
 src/util/lp/nla_solver.cpp | 14 +++++++++++++-
 3 files changed, 20 insertions(+), 1 deletion(-)

diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 3e42ecd08..e5bf3632a 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -210,6 +210,11 @@ unsigned lar_solver::adjust_column_index_to_term_index(unsigned j) const {
     unsigned ext_var_or_term = m_var_register.local_to_external(j);
     return ext_var_or_term < m_terms_start_index ? j : ext_var_or_term;
 }
+
+unsigned lar_solver::map_term_index_to_column_index(unsigned j) const {
+    SASSERT(is_term(j));
+    return m_var_register.external_to_local(j);
+}
     
 void lar_solver::propagate_bounds_on_a_term(const lar_term& t, bound_propagator & bp, unsigned term_offset) {
     lp_assert(false); // not implemented
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 9a8cae438..c6c2ca626 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -271,6 +271,8 @@ public:
 
     unsigned adjust_column_index_to_term_index(unsigned j) const;
 
+    unsigned map_term_index_to_column_index(unsigned j) const;
+    
     var_index local2external(var_index idx) const { return m_var_register.local_to_external(idx); }
 
     unsigned number_of_vars() const { return m_var_register.size(); }
diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index dd42ab286..285e9ce17 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -142,8 +142,20 @@ struct solver::imp {
         return ret;
     }
 
+    lp::lar_term subs_terms_to_columns(const lp::lar_term& t) const {
+        lp::lar_term r;
+        for (const auto& p : t) {
+            lpvar j = p.var();
+            if (m_lar_solver.is_term(j))
+                j = m_lar_solver.map_term_index_to_column_index(j);
+            r.add_coeff_var(p.coeff(), j);
+        }
+        return r;
+    } 
+    
     bool ineq_holds(const ineq& n) const {
-        return compare_holds(value(n.term()), n.cmp(), n.rs());
+        lp::lar_term t = subs_terms_to_columns(n.term());
+        return compare_holds(value(t), n.cmp(), n.rs());
     }
 
     bool an_ineq_holds(const lemma& l) const {