From 3e845010dd2f8af31a28a80136b94abd1e07ed81 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Mon, 30 Mar 2020 15:59:03 -0700
Subject: [PATCH] replace v by j in lp printouts

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/cross_nested.h  | 2 +-
 src/math/lp/lar_solver.cpp  | 4 ++--
 src/math/lp/lp_solver_def.h | 2 +-
 src/math/lp/lp_utils.h      | 2 +-
 src/math/lp/nex.h           | 2 +-
 src/math/lp/nex_creator.h   | 2 +-
 src/math/lp/nla_core.cpp    | 8 ++++----
 src/math/lp/nra_solver.cpp  | 6 +++---
 8 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h
index ddf23fb2d..a39ef5ef9 100644
--- a/src/math/lp/cross_nested.h
+++ b/src/math/lp/cross_nested.h
@@ -185,7 +185,7 @@ public:
     static std::ostream& dump_occurences(std::ostream& out, const T& occurences) {
         out << "{";
         for (const auto& p: occurences) {
-            out << "(v" << p.first << "->" << p.second << ")";
+            out << "(j" << p.first << "->" << p.second << ")";
         }
         out << "}" << std::endl;
         return out;
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 1f7fb0c2c..8d885a8d1 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -1267,10 +1267,10 @@ std::string lar_solver::get_variable_name(var_index j) const {
         return s;
     }
     if (m_settings.m_print_external_var_name) {
-        return std::string("v") + T_to_string(m_var_register.local_to_external(j));
+        return std::string("j") + T_to_string(m_var_register.local_to_external(j));
     }
     else {
-        std::string s = column_corresponds_to_term(j)? "t":"v";
+        std::string s = column_corresponds_to_term(j)? "t":"j";
         return s + T_to_string(j);
     }
 }
diff --git a/src/math/lp/lp_solver_def.h b/src/math/lp/lp_solver_def.h
index af1999559..94c4bd34b 100644
--- a/src/math/lp/lp_solver_def.h
+++ b/src/math/lp/lp_solver_def.h
@@ -30,7 +30,7 @@ template <typename T, typename X> column_info<T> * lp_solver<T, X>::get_or_creat
 template <typename T, typename X>
 std::string lp_solver<T, X>::get_variable_name(unsigned j) const { // j here is the core solver index
     if (!m_settings.m_print_external_var_name)
-        return std::string("v")+T_to_string(j);
+        return std::string("j")+T_to_string(j);
     auto it = this->m_core_solver_columns_to_external_columns.find(j);
     if (it == this->m_core_solver_columns_to_external_columns.end())
         return std::string("x")+T_to_string(j);
diff --git a/src/math/lp/lp_utils.h b/src/math/lp/lp_utils.h
index 387bc6cc5..40c5f0632 100644
--- a/src/math/lp/lp_utils.h
+++ b/src/math/lp/lp_utils.h
@@ -120,7 +120,7 @@ std::ostream& print_linear_combination_of_column_indices_only(const vector<std::
             if (tv::is_term(j)) {
                 ss << "t" << tv::unmask_term(j);
             } else {
-                ss << "v" << j;
+                ss << "j" << j;
             }
             return ss.str();},
         out); 
diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h
index 68d2fefdb..6b9bb6b2f 100644
--- a/src/math/lp/nex.h
+++ b/src/math/lp/nex.h
@@ -118,7 +118,7 @@ public:
     
     lpvar var() const {  return m_j; }
 
-    std::ostream & print(std::ostream& out) const override { return out << "v" << m_j; }    
+    std::ostream & print(std::ostream& out) const override { return out << "j" << m_j; }    
     expr_type type() const override { return expr_type::VAR; }
     unsigned number_of_child_powers() const override { return 1; }
     bool contains(lpvar j) const override { return j == m_j; }
diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h
index 20e5ac142..3a9477c94 100644
--- a/src/math/lp/nex_creator.h
+++ b/src/math/lp/nex_creator.h
@@ -48,7 +48,7 @@ class nex_creator {
 public:
     static std::string ch(unsigned j) {
         std::stringstream s;
-        s << "v" << j;
+        s << "j" << j;
         return s.str();
     }
 
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 7c32270cb..8b3384465 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -185,7 +185,7 @@ std::ostream& core::print_product(const T & m, std::ostream& out) const {
         if (lp_settings().m_print_external_var_name)
             out << "(" << m_lar_solver.get_variable_name(v) << "=" << val(v) << ")";
         else
-            out << "(v" << v << " =" << val(v) << ")";
+            out << "(j" << v << " =" << val(v) << ")";
             
     }
     return out;
@@ -199,7 +199,7 @@ std::string core::product_indices_str(const T & m) const {
             out << "*";
         else
             first = false;
-        out << "v" << v;;
+        out << "j" << v;;
     }
     return out.str();
 }
@@ -232,7 +232,7 @@ std::ostream& core::print_monic(const monic& m, std::ostream& out) const {
     if (lp_settings().m_print_external_var_name)
         out << "([" << m.var() << "] = " << m_lar_solver.get_variable_name(m.var()) << " = " << val(m.var()) << " = ";
     else 
-        out << "(v" << m.var() << " = " << val(m.var()) << " = ";
+        out << "(j" << m.var() << " = " << val(m.var()) << " = ";
     print_product(m.vars(), out) << ")\n";
     return out;
 }
@@ -1445,7 +1445,7 @@ std::ostream& core::print_terms(std::ostream& out) const {
 
 std::string core::var_str(lpvar j) const {
     return is_monic_var(j)?
-        (product_indices_str(m_emons[j].vars()) + (check_monic(m_emons[j])? "": "_")) : (std::string("v") + lp::T_to_string(j));        
+        (product_indices_str(m_emons[j].vars()) + (check_monic(m_emons[j])? "": "_")) : (std::string("j") + lp::T_to_string(j));        
 }
 
 std::ostream& core::print_term( const lp::lar_term& t, std::ostream& out) const {
diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index e79c9b643..7588231e6 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -208,7 +208,7 @@ typedef nla::variable_map_type variable_map_type;
             if (!m_lp2nl.find(v, r)) {
                 r = m_nlsat->mk_var(is_int(v));
                 m_lp2nl.insert(v, r);
-                TRACE("arith", tout << "v" << v << " := x" << r << "\n";);
+                TRACE("arith", tout << "j" << v << " := x" << r << "\n";);
             }
             return r;
         }
@@ -227,9 +227,9 @@ typedef nla::variable_map_type variable_map_type;
 
         std::ostream& display(std::ostream& out) const {
             for (auto m : m_monics) {
-                out << "v" << m.var() << " = ";
+                out << "j" << m.var() << " = ";
                 for (auto v : m.vars()) {
-                    out << "v" << v << " ";
+                    out << "j" << v << " ";
                 }
                 out << "\n";
             }