mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

replace v by j in lp printouts

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-03-30 15:59:03 -07:00
parent a6e7ed039c
commit 3e845010dd
8 changed files with 14 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/cross_nested.h
View file

@ -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;

4
src/math/lp/lar_solver.cpp
View file

@ -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);
}
}

2
src/math/lp/lp_solver_def.h
View file

@ -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);

2
src/math/lp/lp_utils.h
View file

@ -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);

2
src/math/lp/nex.h
View file

@ -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; }

2
src/math/lp/nex_creator.h
View file

@ -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();
}

8
src/math/lp/nla_core.cpp
View file

@ -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 {

6
src/math/lp/nra_solver.cpp
View file

@ -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";
}