debug tangent lemmas

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/smt/theory_lra.cpp

@@ -383,6 +383,7 @@ class theory_lra::imp {
         lp().settings().simplex_strategy() = static_cast<lp::simplex_strategy_enum>(lpar.simplex_strategy());
         lp().settings().bound_propagation() = BP_NONE != propagation_mode();
         lp().settings().m_enable_hnf = lpar.enable_hnf();
+        lp().settings().m_print_external_var_name = lpar.print_ext_var_names();
         lp().set_track_pivoted_rows(lpar.bprop_on_pivoted_rows());
         lp().settings().report_frequency = lpar.rep_freq();
         lp().settings().print_statistics = lpar.print_stats();

src/util/lp/lp_core_solver_base.h

@@ -579,7 +579,11 @@ public:
             out << "[" << j << "] is not present\n";
             return out;
         }
-        out << "[" << j << "],\tname = "<< column_name(j) << "\t";
+        if (m_settings.m_print_external_var_name)
+            out << "[" << j << "],\tname = "<< column_name(j) << "\t";
+        else
+            out << "v" << j <<  "= \t";
+            
         switch (m_column_types[j]) {
         case column_type::fixed:
         case column_type::boxed:

src/util/lp/lp_params.pyg

@@ -13,3 +13,6 @@ def_module_params('lp',
 
 
     
+                   ('print_ext_var_names', BOOL, False, 'print external variable names')
+                          ))
+

src/util/lp/lp_settings.h

@@ -195,6 +195,7 @@ public:
     unsigned         limit_on_rows_for_hnf_cutter;
     unsigned         limit_on_columns_for_hnf_cutter;
     bool             m_enable_hnf;
+    bool             m_print_external_var_name;
 #ifdef Z3DEBUG
     unsigned         m_counter_for_debug;
 #endif
@@ -266,10 +267,10 @@ public:
                     limit_on_rows_for_hnf_cutter(75),
                     limit_on_columns_for_hnf_cutter(150),
                     m_enable_hnf(true)
-                    #ifdef Z3DEBUG
+                    m_print_external_var_name(false),
+#ifdef Z3DEBUG
                   , m_counter_for_debug(0)
-                    #endif
+#endif
-                    
     {}
 
     void set_resource_limit(lp_resource_limit& lim) { m_resource_limit = &lim; }

src/util/lp/nla_core.cpp

@@ -164,7 +164,11 @@ std::ostream& core::print_product(const T & m, std::ostream& out) const {
     bool first = true;
     for (lpvar v : m) {
         if (!first) out << "*"; else first = false;
-        out << "(" << m_lar_solver.get_variable_name(v) << "=" << val(v) << ")";
+        if (settings().m_print_external_var_name)
+            out << "(" << m_lar_solver.get_variable_name(v) << "=" << val(v) << ")";
+        else
+            out << "(v" << v << " =" << val(v) << ")";
+            
     }
     return out;
 }
@@ -194,7 +198,10 @@ std::ostream & core::print_factor_with_vars(const factor& f, std::ostream& out)
 }
 
 std::ostream& core::print_monomial(const monomial& m, std::ostream& out) const {
-    out << "( [" << m.var() << "] = " << m_lar_solver.get_variable_name(m.var()) << " = " << val(m.var()) << " = ";
+    if (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()) << " = ";
     print_product(m.vars(), out) << ")\n";
     return out;
 }
@@ -210,7 +217,11 @@ std::ostream& core::print_tangent_domain(const point &a, const point &b, std::os
 }
 
 std::ostream& core::print_bfc(const bfc& m, std::ostream& out) const {
-    return out << "( x = "; print_factor(m.m_x, out); out <<  ", y = "; print_factor(m.m_y, out); out <<  ")";
+    out << "( x = ";
+    print_factor(m.m_x, out);
+    out <<  ", y = ";
+    print_factor(m.m_y, out); out <<  ")";
+    return out;
 }
 
 std::ostream& core::print_monomial_with_vars(lpvar v, std::ostream& out) const {
@@ -734,7 +745,6 @@ std::ostream & core::print_ineq(const ineq & in, std::ostream & out) const {
 std::ostream & core::print_var(lpvar j, std::ostream & out) const {
     if (m_emons.is_monomial_var(j)) {
         print_monomial(m_emons[j], out);
-        out << " = " << val(j);;
     }
         
     m_lar_solver.print_column_info(j, out);
@@ -1193,6 +1203,9 @@ template bool core::mon_has_zero<unsigned_vector>(const unsigned_vector& product
 lp::lp_settings& core::settings() {
     return m_lar_solver.settings();
 }
+const lp::lp_settings& core::settings() const {
+    return m_lar_solver.settings();
+}
     
 unsigned core::random() { return settings().random_next(); }
     

src/util/lp/nla_core.h

@@ -268,6 +268,7 @@ public:
     template <typename T>
     bool mon_has_zero(const T& product) const;
     lp::lp_settings& settings();
+    const lp::lp_settings& settings() const;
     unsigned random();
     void map_monomial_vars_to_monomial_indices(unsigned i);