mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-12 10:14:42 +00:00
Code Activity

remove a function from lar_solver

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-05-07 13:33:46 -07:00
parent 67652dd8eb
commit 97c6074156
2 changed files with 0 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -16,7 +16,6 @@ namespace lp {
}; };
struct imp { struct imp {
lar_solver &lra; lar_solver &lra;
var_register m_var_register; var_register m_var_register;
svector<column> m_columns; svector<column> m_columns;
@ -1723,14 +1722,6 @@ namespace lp {
return m_mpq_lar_core_solver.column_is_free(j); return m_mpq_lar_core_solver.column_is_free(j);
} }
// below is the initialization functionality of lar_solver
lpvar lar_solver::add_named_var(unsigned ext_j, bool is_int, const std::string& name) {
lpvar j = add_var(ext_j, is_int);
m_imp->m_var_register.set_name(j, name);
return j;
}
struct lar_solver::undo_add_column : public trail { struct lar_solver::undo_add_column : public trail {
lar_solver& s; lar_solver& s;
undo_add_column(lar_solver& s) : s(s) {} undo_add_column(lar_solver& s) : s(s) {}

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

@ -296,8 +296,6 @@ public:
set_column_value(j, v); set_column_value(j, v);
} }
lpvar add_named_var(unsigned ext_j, bool is_integer, const std::string&);
lp_status maximize_term(unsigned j_or_term, impq& term_max); lp_status maximize_term(unsigned j_or_term, impq& term_max);
inline core_solver_pretty_printer<lp::mpq, lp::impq> pp(std::ostream& out) const { inline core_solver_pretty_printer<lp::mpq, lp::impq> pp(std::ostream& out) const {