From 024ca86386818e6dd46bbd0afd303ae3234d56c1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 7 Feb 2020 09:16:14 -0800 Subject: [PATCH] isolate constraints in a constraint_set Signed-off-by: Nikolaj Bjorner --- src/math/lp/lar_solver.cpp | 17 +---------------- src/math/lp/lar_solver.h | 11 ----------- 2 files changed, 1 insertion(+), 27 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 3ab51c9cc..f678d39b7 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -530,7 +530,7 @@ bool lar_solver::maximize_term_on_corrected_r_solver(lar_term & term, impq &term_max) { settings().backup_costs = false; bool ret = false; - TRACE("lar_solver", print_term(term, tout << "maximize: ") << "\n"; print_constraints(tout); tout << ", strategy = " << (int)settings().simplex_strategy() << "\n";); + TRACE("lar_solver", print_term(term, tout << "maximize: ") << "\n" << constraints() << ", strategy = " << (int)settings().simplex_strategy() << "\n";); switch (settings().simplex_strategy()) { case simplex_strategy_enum::tableau_rows: @@ -1286,21 +1286,6 @@ std::string lar_solver::get_variable_name(var_index j) const { } // ********** print region start -std::ostream& lar_solver::print_constraint(constraint_index ci, std::ostream & out) const { - return m_constraints.display(out, ci); -} - -std::ostream& lar_solver::print_constraint_indices_only(constraint_index ci, std::ostream & out) const { - return m_constraints.display_indices_only(out, ci); -} - -std::ostream& lar_solver::print_constraint_indices_only_customized(constraint_index ci, std::function var_str, std::ostream & out) const { - return m_constraints.display(out, var_str, ci); -} - -std::ostream& lar_solver::print_constraints(std::ostream& out) const { - return out << m_constraints; -} std::ostream& lar_solver::print_terms(std::ostream& out) const { for (auto it : m_terms) { diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index dd711b2c5..60efe1319 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -489,17 +489,6 @@ public: void set_variable_name(var_index vi, std::string); // ********** print region start - private: - std::ostream& print_constraint(constraint_index ci, std::ostream & out) const; - - std::ostream& print_constraints(std::ostream& out) const ; - - std::ostream& print_constraint_indices_only(constraint_index ci, std::ostream & out) const; - - std::ostream& print_constraint_indices_only_customized(constraint_index ci, std::function var_str, std::ostream & out) const; - - std::ostream& print_constraint_indices_only_customized(const lar_base_constraint * c, std::function var_str, std::ostream & out) const; - public: std::ostream& print_terms(std::ostream& out) const;