diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 78c00fd65..2c127be49 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -16,7 +16,6 @@ namespace lp { }; struct imp { - lar_solver &lra; var_register m_var_register; svector m_columns; @@ -1723,14 +1722,6 @@ namespace lp { 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 { lar_solver& s; undo_add_column(lar_solver& s) : s(s) {} diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index a40179174..91195d065 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -296,8 +296,6 @@ public: 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); inline core_solver_pretty_printer pp(std::ostream& out) const {