From e50082b48448bf303858824467584cfa76f2fbb2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 18 Mar 2020 16:48:37 -0700
Subject: [PATCH] add tv

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/gomory.cpp     |  2 +-
 src/math/lp/lar_solver.cpp | 72 +++++++++++++++++++-------------------
 src/math/lp/lar_solver.h   | 14 ++++----
 src/math/lp/lar_term.h     |  1 +
 src/math/lp/lp_types.h     | 37 ++++++++++++++++++++
 src/math/lp/nla_core.cpp   | 14 ++++----
 src/math/lp/var_register.h |  9 ++---
 src/smt/theory_lra.cpp     | 49 ++++++++++++++------------
 8 files changed, 117 insertions(+), 81 deletions(-)

diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
index 449dec271..fa506b277 100644
--- a/src/math/lp/gomory.cpp
+++ b/src/math/lp/gomory.cpp
@@ -222,7 +222,7 @@ class create_cut {
         }
         for (const auto& p : m_t) {
             unsigned v = p.var();
-            if (lp::is_term(v)) {
+            if (lp::tv::is_term(v)) {
                 dump_declaration(out, v);
             }
         }
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 16953ee4f..08d7b0502 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -59,9 +59,9 @@ bool lar_solver::sizes_are_correct() const {
 std::ostream& lar_solver::print_implied_bound(const implied_bound& be, std::ostream & out) const {
     out << "implied bound\n";
     unsigned v = be.m_j;
-    if (is_term(v)) {
+    if (tv::is_term(v)) {
         out << "it is a term number " << be.m_j << std::endl;
-        print_term(*m_terms[unmask_term(v)],  out);
+        print_term(*m_terms[tv::unmask_term(v)],  out);
     }
     else {
         out << get_variable_name(v);
@@ -102,7 +102,7 @@ bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be,
     if (strict)
         kind = static_cast<lconstraint_kind>((static_cast<int>(kind) / 2));
       
-    if (!is_term(be.m_j)) {
+    if (!tv::is_term(be.m_j)) {
         if (coeff_map.size() != 1)
             return false;
         auto it = coeff_map.find(be.m_j);
@@ -113,7 +113,7 @@ bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be,
         }
         rs_of_evidence /= ratio;
     } else {
-        lar_term & t = *m_terms[unmask_term(be.m_j)];
+        lar_term & t = *m_terms[tv::unmask_term(be.m_j)];
         auto first_coeff = t.begin();
         unsigned j = (*first_coeff).var();
         auto it = coeff_map.find(j);
@@ -192,14 +192,14 @@ 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 (is_term(j))
+    if (tv::is_term(j))
         return j;
     unsigned ext_var_or_term = m_var_register.local_to_external(j);
-    return !is_term(ext_var_or_term) ? j : ext_var_or_term;
+    return !tv::is_term(ext_var_or_term) ? j : ext_var_or_term;
 }
 
 unsigned lar_solver::map_term_index_to_column_index(unsigned j) const {
-    SASSERT(is_term(j));
+    SASSERT(tv::is_term(j));
     return m_var_register.external_to_local(j);
 }
     
@@ -213,7 +213,7 @@ void lar_solver::explain_implied_bound(implied_bound & ib, lp_bound_propagator &
     int bound_sign = ib.m_is_lower_bound? 1: -1;
     int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign;
     unsigned bound_j = ib.m_j;
-    if (is_term(bound_j)) {
+    if (tv::is_term(bound_j)) {
         bound_j = m_var_register.external_to_local(bound_j);
     }
     for (auto const& r : A_r().m_rows[i]) {
@@ -232,7 +232,7 @@ void lar_solver::explain_implied_bound(implied_bound & ib, lp_bound_propagator &
 // here i is just the term index
 bool lar_solver::term_is_used_as_row(unsigned i) const {
     SASSERT(i < m_terms.size());
-    return m_var_register.external_is_used(mask_term(i));
+    return m_var_register.external_is_used(tv::mask_term(i));
 }
     
 void lar_solver::propagate_bounds_on_terms(lp_bound_propagator & bp) {
@@ -560,7 +560,7 @@ bool lar_solver::remove_from_basis(unsigned j) {
 }
 
 lar_term lar_solver::get_term_to_maximize(unsigned j_or_term) const {
-    if (is_term(j_or_term)) {
+    if (tv::is_term(j_or_term)) {
         return get_term(j_or_term);
     }
     if (j_or_term < m_mpq_lar_core_solver.m_r_x.size()) {
@@ -633,8 +633,8 @@ lp_status lar_solver::maximize_term(unsigned j_or_term,
 
     
 const lar_term &  lar_solver::get_term(unsigned j) const {
-    lp_assert(is_term(j));
-    return *m_terms[unmask_term(j)];
+    lp_assert(tv::is_term(j));
+    return *m_terms[tv::unmask_term(j)];
 }
 
 void lar_solver::pop_core_solver_params() {
@@ -674,10 +674,10 @@ void lar_solver::substitute_terms_in_linear_expression(const vector<std::pair<mp
     std::unordered_map<var_index, mpq> coeffs;
     for (auto & t : left_side_with_terms) {
         unsigned j = t.second;
-        if (!is_term(j)) {
+        if (!tv::is_term(j)) {
             register_monoid_in_map(coeffs, t.first, j);
         } else {
-            const lar_term & term = * m_terms[unmask_term(t.second)];
+            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());
@@ -903,8 +903,8 @@ bool lar_solver::x_is_correct() const {
 }
 
 bool lar_solver::var_is_registered(var_index vj) const {
-    if (is_term(vj)) {
-        return unmask_term(vj) < m_terms.size();
+    if (tv::is_term(vj)) {
+        return tv::unmask_term(vj) < m_terms.size();
     }
     return vj < A_r().column_count();
 }
@@ -1143,7 +1143,7 @@ bool lar_solver::has_upper_bound(var_index var, constraint_index& ci, mpq& value
 }
 
 bool lar_solver::has_value(var_index var, mpq& value) const {
-    if (is_term(var)) {
+    if (tv::is_term(var)) {
         lar_term const& t = get_term(var);
         value = 0;
         for (auto const& cv : t) {
@@ -1258,7 +1258,7 @@ void lar_solver::set_variable_name(var_index vi, std::string name) {
 }
 
 std::string lar_solver::get_variable_name(var_index j) const {
-    if (is_term(j)) 
+    if (tv::is_term(j)) 
         return std::string("_t") + T_to_string(j);
     if (j >= m_var_register.size())
         return std::string("_s") + T_to_string(j);
@@ -1330,8 +1330,8 @@ mpq lar_solver::get_left_side_val(const lar_base_constraint &  cns, const std::u
 void lar_solver::fill_var_set_for_random_update(unsigned sz, var_index const * vars, vector<unsigned>& column_list) {
     for (unsigned i = 0; i < sz; i++) {        
         var_index var = vars[i];
-        if (is_term(var)) { // handle the term
-            for (auto it : *m_terms[unmask_term(var)]) {
+        if (tv::is_term(var)) { // handle the term
+            for (auto it : *m_terms[tv::unmask_term(var)]) {
                 column_list.push_back(it.var());
             }
         } else {
@@ -1541,7 +1541,7 @@ bool lar_solver::term_is_int(const vector<std::pair<mpq, unsigned int>>& coeffs)
 }
 
 bool lar_solver::var_is_int(var_index v) const {
-    if (is_term(v)) {
+    if (tv::is_term(v)) {
         lar_term const& t = get_term(v);
         return term_is_int(&t);
     }
@@ -1576,7 +1576,7 @@ var_index lar_solver::add_named_var(unsigned ext_j, bool is_int, const std::stri
 var_index lar_solver::add_var(unsigned ext_j, bool is_int) {
     TRACE("add_var", tout << "adding var " << ext_j << (is_int? " int" : " nonint") << std::endl;);
     var_index local_j;
-    lp_assert(!is_term(ext_j));
+    lp_assert(!tv::is_term(ext_j));
     if (m_var_register.external_is_used(ext_j, local_j))
         return local_j;
     lp_assert(m_columns_to_ul_pairs.size() == A_r().column_count());
@@ -1654,7 +1654,7 @@ void lar_solver::add_new_var_to_core_fields_for_mpq(bool register_in_basis) {
 
 var_index lar_solver::add_term_undecided(const vector<std::pair<mpq, var_index>> & coeffs) {
     push_term(new lar_term(coeffs));
-    return mask_term(m_terms.size() - 1);
+    return tv::mask_term(m_terms.size() - 1);
 }
 
 #if Z3DEBUG_CHECK_UNIQUE_TERMS
@@ -1710,7 +1710,7 @@ var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs,
     push_term(t);
     SASSERT(m_terms.size() == m_term_register.size());
     unsigned adjusted_term_index = m_terms.size() - 1;
-    var_index ret = mask_term(adjusted_term_index);
+    var_index ret = tv::mask_term(adjusted_term_index);
     if (use_tableau() && !coeffs.empty()) {
         add_row_from_term_no_constraint(m_terms.back(), ret);
         if (m_settings.bound_propagation())
@@ -1802,7 +1802,7 @@ mpq lar_solver::adjust_bound_for_int(lpvar j, lconstraint_kind& k, const mpq& bo
 constraint_index lar_solver::mk_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) {
     TRACE("lar_solver", tout << "j = " << j << " " << lconstraint_kind_string(kind) << " " << right_side<< std::endl;);
     constraint_index ci;
-    if (!is_term(j)) { // j is a var
+    if (!tv::is_term(j)) { // j is a var
         mpq rs = adjust_bound_for_int(j, kind, right_side);
         lp_assert(bound_is_integer_for_integer_column(j, rs));
         ci = m_constraints.add_var_constraint(j, kind, rs);
@@ -1815,7 +1815,7 @@ constraint_index lar_solver::mk_var_bound(var_index j, lconstraint_kind kind, co
 }
 
 bool lar_solver::compare_values(var_index j, lconstraint_kind k, const mpq & rhs) {
-    if (is_term(j))
+    if (tv::is_term(j))
         j = to_column(j);
     return compare_values(get_column_value(j), k, rhs);
 }
@@ -1843,8 +1843,8 @@ void lar_solver::update_column_type_and_bound(var_index j, lconstraint_kind kind
 }
 
 constraint_index lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side) {
-    lp_assert(is_term(j));
-    unsigned adjusted_term_index = unmask_term(j);
+    lp_assert(tv::is_term(j));
+    unsigned adjusted_term_index = tv::unmask_term(j);
     //    lp_assert(!term_is_int(m_terms[adjusted_term_index]) || right_side.is_int());
     unsigned term_j;
     lar_term const* term = m_terms[adjusted_term_index];    
@@ -1924,9 +1924,9 @@ void lar_solver::adjust_initial_state_for_lu() {
 
 void lar_solver::adjust_initial_state_for_tableau_rows() {
     for (unsigned i = 0; i < m_terms.size(); i++) {
-        if (m_var_register.external_is_used(mask_term(i)))
+        if (m_var_register.external_is_used(tv::mask_term(i)))
             continue;
-        add_row_from_term_no_constraint(m_terms[i], mask_term(i));
+        add_row_from_term_no_constraint(m_terms[i], tv::mask_term(i));
     }
 }
 
@@ -2168,7 +2168,7 @@ void lar_solver::update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kin
 }
 
 bool lar_solver::column_corresponds_to_term(unsigned j) const {
-    return is_term(m_var_register.local_to_external(j));
+    return tv::is_term(m_var_register.local_to_external(j));
 }
 
 var_index lar_solver::to_column(unsigned ext_j) const {
@@ -2176,8 +2176,8 @@ var_index lar_solver::to_column(unsigned ext_j) const {
 }
 
 bool lar_solver::tighten_term_bounds_by_delta(unsigned term_index, const impq& delta) {
-    SASSERT(!is_term(term_index));
-    unsigned tj = mask_term(term_index);
+    SASSERT(!tv::is_term(term_index));
+    unsigned tj = tv::mask_term(term_index);
     unsigned j;
     if (m_var_register.external_is_used(tj, j) == false)
         return true; // the term is not a column so it has no bounds
@@ -2246,7 +2246,7 @@ void lar_solver::fix_terms_with_rounded_columns() {
             }
         }
         if (need_to_fix) {
-            lpvar j = m_var_register.external_to_local(mask_term(i));
+            lpvar j = m_var_register.external_to_local(tv::mask_term(i));
             impq v = t.apply(m_mpq_lar_core_solver.m_r_x);
             m_mpq_lar_core_solver.m_r_solver.update_x(j, v);
         }
@@ -2266,7 +2266,7 @@ bool lar_solver::sum_first_coords(const lar_term& t, mpq & val) const {
 }
 
 bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term_index, mpq & rs, constraint_index& ci, bool &upper_bound) const {
-    unsigned tj = mask_term(term_index);
+    unsigned tj = tv::mask_term(term_index);
     unsigned j;
     bool is_int;
     if (m_var_register.external_is_used(tj, j, is_int) == false)
@@ -2341,7 +2341,7 @@ void lar_solver::register_existing_terms() {
     if (!m_need_register_terms) {
         TRACE("nla_solver", tout << "registering " << m_terms.size() << " terms\n";);
         for (unsigned k = 0; k < m_terms.size(); k++) {
-            lpvar j = m_var_register.external_to_local(mask_term(k));
+            lpvar j = m_var_register.external_to_local(tv::mask_term(k));
             register_normalized_term(*m_terms[k], j);
         }
     }
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index b807df75b..5615808f0 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -136,7 +136,7 @@ public:
     }
     
     const mpq& get_column_value_rational(unsigned j) const {
-        if (is_term(j)) {
+        if (tv::is_term(j)) {
             j = m_var_register.external_to_local(j);
         }
         return m_mpq_lar_core_solver.m_r_x[j].x;
@@ -266,7 +266,7 @@ public:
 
     unsigned map_term_index_to_column_index(unsigned j) const;
     
-    var_index local_to_external(var_index idx) const { return is_term(idx)?
+    var_index local_to_external(var_index idx) const { return tv::is_term(idx)?
             m_term_register.local_to_external(idx) : m_var_register.local_to_external(idx); }
 
     unsigned number_of_vars() const { return m_var_register.size(); }
@@ -561,14 +561,14 @@ public:
     }
 
     constraint_index get_column_upper_bound_witness(unsigned j) const {
-        if (is_term(j)) {
+        if (tv::is_term(j)) {
             j = m_var_register.external_to_local(j);
         }
         return m_columns_to_ul_pairs()[j].upper_bound_witness();
     }
 
     constraint_index get_column_lower_bound_witness(unsigned j) const {
-        if (is_term(j)) {
+        if (tv::is_term(j)) {
             j = m_var_register.external_to_local(j);
         }
         return m_columns_to_ul_pairs()[j].lower_bound_witness();
@@ -588,12 +588,12 @@ public:
     
     std::ostream& print_column_info(unsigned j, std::ostream& out) const {
         m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out);
-        if (is_term(j)) {
-            const lar_term& t = * m_terms[unmask_term(j)];
+        if (tv::is_term(j)) {
+            const lar_term& t = * m_terms[tv::unmask_term(j)];
             print_term_as_indices(t, out) << "\n";
             
         } else if(column_corresponds_to_term(j)) { 
-            const lar_term& t = * m_terms[unmask_term(m_var_register.local_to_external(j))];
+            const lar_term& t = * m_terms[tv::unmask_term(m_var_register.local_to_external(j))];
             print_term_as_indices(t, out) << "\n";
         }
         return out;
diff --git a/src/math/lp/lar_term.h b/src/math/lp/lar_term.h
index 6bc8ba8b0..f5c58ce05 100644
--- a/src/math/lp/lar_term.h
+++ b/src/math/lp/lar_term.h
@@ -22,6 +22,7 @@
 #include "util/map.h"
 
 namespace lp {
+
 class lar_term {
     // the term evaluates to sum of m_coeffs 
     typedef unsigned lpvar;
diff --git a/src/math/lp/lp_types.h b/src/math/lp/lp_types.h
index 8b18cdee8..38da85ef3 100644
--- a/src/math/lp/lp_types.h
+++ b/src/math/lp/lp_types.h
@@ -23,4 +23,41 @@ typedef unsigned var_index;
 typedef unsigned constraint_index;
 typedef unsigned row_index;
 enum lconstraint_kind { LE = -2, LT = -1 , GE = 2, GT = 1, EQ = 0, NE = 3 };
+
+
+// index that comes from term or variable.
+class tv {
+    unsigned m_index;
+    static const unsigned EF = UINT_MAX >> 1;
+    tv(unsigned i): m_index(i) {}
+public:
+    // create a term index
+    struct is_term {};
+    tv(unsigned i, is_term):m_index(mask_term(i)) { SASSERT(0 == (i & left_most_bit)); }
+
+    // create a variable index
+    struct is_var {};
+    tv(unsigned i, is_var):m_index(i) { SASSERT(0 == (i & left_most_bit)); }
+
+    // create a tv from an index
+    static tv to_tv(unsigned i) { return tv(i); }
+
+    // retrieve the identifier associated with tv
+    unsigned id() const { return unmask_term(m_index); }
+
+    // retrieve the raw index.
+    unsigned index() const { return m_index; }
+
+    bool is_term() const { return m_index & left_most_bit; }
+    bool is_var() const { return !is_term(); }
+
+    // utilities useful where tv isn't already encapsulating id's.
+    static inline unsigned unmask_term(unsigned j) { return j & EF; }
+    static inline bool is_term(unsigned j) { return j & left_most_bit; }
+    static inline unsigned mask_term(unsigned j) { return j | left_most_bit; }
+
+    // used by var_register. could we encapsulate even this?
+    static const unsigned left_most_bit  = ~EF;
+
+};
 }
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index af1a79f92..31d00923c 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -59,7 +59,7 @@ 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();
-        if (lp::is_term(j))
+        if (lp::tv::is_term(j))
             j = m_lar_solver.map_term_index_to_column_index(j);
         r.add_monomial(p.coeff(), j);
     }
@@ -126,7 +126,7 @@ void core::add_monic(lpvar v, unsigned sz, lpvar const* vs) {
     m_add_buffer.resize(sz);
     for (unsigned i = 0; i < sz; i++) {
         lpvar j = vs[i];
-        if (lp::is_term(j))
+        if (lp::tv::is_term(j))
             j = m_lar_solver.map_term_index_to_column_index(j);
         m_add_buffer[i] = j;
     }
@@ -342,7 +342,7 @@ bool core:: explain_coeff_lower_bound(const lp::lar_term::ival& p, rational& bou
 
 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 = lp::is_term(p.var())? m_lar_solver.map_term_index_to_column_index(p.var()) : p.var();
+    lpvar j = lp::tv::is_term(p.var())? m_lar_solver.map_term_index_to_column_index(p.var()) : p.var();
     SASSERT(!a.is_zero());
     unsigned c; // the index for the lower or the upper bound
     if (a.is_neg()) {
@@ -837,7 +837,7 @@ void core::collect_equivs() {
     for (unsigned i = 0; i < s.terms().size(); i++) {
         if (!s.term_is_used_as_row(i))
             continue;
-        lpvar j = s.external_to_local(lp::mask_term(i));
+        lpvar j = s.external_to_local(lp::tv::mask_term(i));
         if (var_is_fixed_to_zero(j)) {
             TRACE("nla_solver_eq", tout << "term = "; s.print_term_as_indices(*s.terms()[i], tout););
             add_equivalence_maybe(s.terms()[i], s.get_column_upper_bound_witness(j), s.get_column_lower_bound_witness(j));
@@ -1363,7 +1363,7 @@ lbool core::test_check(
 
 std::ostream& core::print_terms(std::ostream& out) const {
     for (unsigned i = 0; i< m_lar_solver.m_terms.size(); i++) {
-        unsigned ext = lp::mask_term(i);
+        unsigned ext = lp::tv::mask_term(i);
         if (!m_lar_solver.var_is_registered(ext)) {
             out << "term is not registered\n";
             continue;
@@ -1714,8 +1714,8 @@ bool core::is_nl_var(lpvar j) const {
 
 
 bool core::influences_nl_var(lpvar j) const {
-    if (lp::is_term(j))
-        j = lp::unmask_term(j);
+    if (lp::tv::is_term(j))
+        j = lp::tv::unmask_term(j);
     if (is_nl_var(j))
         return true;
     for (const auto & c : m_lar_solver.A_r().m_columns[j]) {
diff --git a/src/math/lp/var_register.h b/src/math/lp/var_register.h
index 490c9db13..69f07204f 100644
--- a/src/math/lp/var_register.h
+++ b/src/math/lp/var_register.h
@@ -17,15 +17,10 @@ Revision History:
 
 --*/
 #pragma once
+#include "math/lp/lp_types.h"
 namespace lp  {
-const unsigned EF = UINT_MAX >> 1;
-const unsigned left_most_bit  = ~EF;
 
-inline unsigned unmask_term(unsigned j) { return j & EF; }
 
-inline bool is_term(unsigned j) { return j & left_most_bit; }
-
-inline unsigned mask_term(unsigned j) { return j | left_most_bit; }
 
 class ext_var_info {
     unsigned m_external_j;
@@ -49,7 +44,7 @@ class var_register {
     unsigned m_locals_mask;
     unsigned m_locals_mask_inverted;
 public:
-    var_register(bool mask_locals): m_locals_mask(mask_locals? left_most_bit: 0), m_locals_mask_inverted(~m_locals_mask) {}
+    var_register(bool mask_locals): m_locals_mask(mask_locals? tv::left_most_bit: 0), m_locals_mask_inverted(~m_locals_mask) {}
     
     void set_name(unsigned j, std::string name) {
         m_local_to_external[j].set_name(name);
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 505b975cf..288511e28 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -978,7 +978,7 @@ class theory_lra::imp {
                 }
                 SASSERT(!m_left_side.empty());
                 vi = lp().add_term(m_left_side, v);
-                SASSERT (lp::is_term(vi));
+                SASSERT (lp::tv::is_term(vi));
                 TRACE("arith_verbose", tout << "v" << v << " := " << mk_pp(term, m) << " slack: " << vi << " scopes: " << m_scopes.size() << "\n";
                       lp().print_term(lp().get_term(vi), tout) << "\n";);
             }
@@ -1493,7 +1493,7 @@ public:
     lp::impq get_ivalue(theory_var v) const {
         SASSERT(can_get_ivalue(v));
         lpvar vi = get_lpvar(v);
-        if (!lp::is_term(vi))
+        if (!lp::tv::is_term(vi))
             return lp().get_column_value(vi);
         m_todo_terms.push_back(std::make_pair(vi, rational::one()));
         lp::impq result(0);
@@ -1501,7 +1501,7 @@ public:
             vi = m_todo_terms.back().first;
             rational coeff = m_todo_terms.back().second;
             m_todo_terms.pop_back();
-            if (lp::is_term(vi)) {
+            if (lp::tv::is_term(vi)) {
                 const lp::lar_term& term = lp().get_term(vi);
                 for (const auto & i:  term) {
                     m_todo_terms.push_back(std::make_pair(i.var(), coeff * i.coeff()));
@@ -1523,7 +1523,7 @@ public:
         if (m_variable_values.count(vi) > 0)
             return m_variable_values[vi];
         
-        if (!lp::is_term(vi)) {
+        if (!lp::tv::is_term(vi)) {
             return rational::zero();
         }
         
@@ -1533,7 +1533,7 @@ public:
             lpvar wi = m_todo_terms.back().first;
             rational coeff = m_todo_terms.back().second;
             m_todo_terms.pop_back();
-            if (lp::is_term(wi)) {
+            if (lp::tv::is_term(wi)) {
                 const lp::lar_term& term = lp().get_term(wi);
                 for (const auto & i : term) {
                     if (m_variable_values.count(i.var()) > 0) {
@@ -1933,7 +1933,7 @@ public:
         expr_ref_vector ts(m);
         for (auto const& p : term) {
             lpvar wi = p.var();
-            if (lp::is_term(wi)) {
+            if (lp::tv::is_term(wi)) {
                 ts.push_back(multerm(p.coeff(), term2expr(lp().get_term(wi))));
             }
             else {
@@ -1976,7 +1976,7 @@ public:
         for (auto const& p : term) {
             lpvar wi = p.var();
             out << p.coeff() << " * ";
-            if (lp::is_term(wi)) {
+            if (lp::tv::is_term(wi)) {
                 lp().print_term(lp().get_term(wi), out) << "\n";
             }
             else {
@@ -2770,7 +2770,7 @@ public:
     void add_use_lists(lp_api::bound* b) {
         theory_var v = b->get_var();
         lpvar vi = register_theory_var_in_lar_solver(v);
-        if (!lp::is_term(vi)) {
+        if (!lp::tv::is_term(vi)) {
             return;
         }
         m_todo_vars.push_back(vi);
@@ -2780,7 +2780,7 @@ public:
             lp::lar_term const& term = lp().get_term(vi);
             for (auto const& p : term) {
                 lpvar wi = p.var();
-                if (lp::is_term(wi)) {
+                if (lp::tv::is_term(wi)) {
                     m_todo_vars.push_back(wi);
                 }
                 else {
@@ -2795,7 +2795,7 @@ public:
     void del_use_lists(lp_api::bound* b) {
         theory_var v = b->get_var();
         lpvar vi = get_lpvar(v);
-        if (!lp::is_term(vi)) {
+        if (!lp::tv::is_term(vi)) {
             return;
         }
         m_todo_vars.push_back(vi);
@@ -2805,7 +2805,7 @@ public:
             lp::lar_term const& term = lp().get_term(vi);
             for (auto const& coeff : term) {
                 lpvar wi = coeff.var();
-                if (lp::is_term(wi)) {
+                if (lp::tv::is_term(wi)) {
                     m_todo_vars.push_back(wi);
                 }
                 else {
@@ -2892,14 +2892,14 @@ public:
         r.reset();
         theory_var v = b.get_var();
         lpvar vi = get_lpvar(v);
-        SASSERT(lp::is_term(vi));
+        SASSERT(lp::tv::is_term(vi));
         lp::lar_term const& term = m_solver->get_term(vi);
         for (auto const mono : term) {
             lp::var_index wi = mono.var();
             lp::constraint_index ci;
             rational value;
             bool is_strict;
-            if (lp::is_term(wi)) {
+            if (lp::tv::is_term(wi)) {
                 return false;
             }
             if (mono.coeff().is_neg() == is_lub) {
@@ -3048,8 +3048,8 @@ public:
 
     bool set_bound(lpvar vi, lp::constraint_index ci, rational const& v, bool is_lower) {
 
-        if (lp::is_term(vi)) {
-            lpvar ti = lp::unmask_term(vi);
+        if (lp::tv::is_term(vi)) {
+            lpvar ti = lp::tv::unmask_term(vi);
             auto& vec = is_lower ? m_lower_terms : m_upper_terms;
             if (vec.size() <= ti) {
                 vec.resize(ti + 1, constraint_bound(UINT_MAX, rational()));
@@ -3096,7 +3096,7 @@ public:
     bool has_lower_bound(lpvar vi, lp::constraint_index& ci, rational const& bound) { return has_bound(vi, ci, bound, true); }
        
     bool has_bound(lpvar vi, lp::constraint_index& ci, rational const& bound, bool is_lower) {
-        if (lp::is_term(vi)) {
+        if (lp::tv::is_term(vi)) {
             theory_var v = lp().local_to_external(vi);
             rational val;
             TRACE("arith", tout << vi << " " << v << "\n";);
@@ -3106,7 +3106,7 @@ public:
             }
 
             auto& vec = is_lower ? m_lower_terms : m_upper_terms;
-            lpvar ti = lp::unmask_term(vi);
+            lpvar ti = lp::tv::unmask_term(vi);
             if (vec.size() > ti) {
                 constraint_bound& b = vec[ti];
                 ci = b.first;
@@ -3218,6 +3218,7 @@ public:
     // lp::constraint_index const null_constraint_index = UINT_MAX; // not sure what a correct fix is
 
     void set_evidence(lp::constraint_index idx) {
+        std::cout << idx << "\n";
         if (idx == UINT_MAX) {
             return;
         }
@@ -3235,6 +3236,7 @@ public:
             break;
         }
         case definition_source: {
+            std::cout << "def\n";
             // skip definitions (these are treated as hard constraints)
             break;
         }
@@ -3266,12 +3268,13 @@ public:
         ++m_num_conflicts;
         ++m_stats.m_conflicts;
         TRACE("arith", tout << "scope: " << ctx().get_scope_level() << "\n"; display_evidence(tout, m_explanation); );
-        TRACE("arith", display(tout););
+        TRACE("arith", display(tout << "is-conflict: " << is_conflict << "\n"););
         for (auto const& ev : m_explanation) {
             if (!ev.first.is_zero()) { 
                 set_evidence(ev.second);
             }
         }
+        std::cout << m_core << "\n";
         // SASSERT(validate_conflict());
         dump_conflict();
         if (is_conflict) {
@@ -3336,7 +3339,7 @@ public:
         SASSERT(m_nra);
         SASSERT(m_use_nra_model);
         lpvar vi = get_lpvar(v);
-        if (lp::is_term(vi)) {
+        if (lp::tv::is_term(vi)) {
 
             m_todo_terms.push_back(std::make_pair(vi, rational::one()));
 
@@ -3357,7 +3360,7 @@ public:
                 for (auto const & arg : term) {
                     lpvar wi = arg.var();
                     c1 = arg.coeff() * wcoeff;
-                    if (lp::is_term(wi)) {
+                    if (lp::tv::is_term(wi)) {
                         m_todo_terms.push_back(std::make_pair(wi, c1));
                     }
                     else {
@@ -3628,8 +3631,8 @@ public:
     void term2coeffs(lp::lar_term const& term, u_map<rational>& coeffs, rational const& coeff) {
         for (const auto & ti : term) {
             theory_var w;
-            if (lp::is_term(ti.var())) {
-                //w = m_term_index2theory_var.get(lp::unmask_term(ti.m_key), null_theory_var);
+            if (lp::tv::is_term(ti.var())) {
+                //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());
                 rational coeff2 = coeff * ti.coeff();
@@ -3697,7 +3700,7 @@ public:
     app_ref mk_obj(theory_var v) {
         lpvar vi = get_lpvar(v);
         bool is_int = a.is_int(get_enode(v)->get_owner());
-        if (lp::is_term(vi)) {           
+        if (lp::tv::is_term(vi)) {           
             return mk_term(lp().get_term(vi), is_int);
         }
         else {