From 13549aff6669bb9536bd3c1fe9f6aefbadf23abf Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 7 Mar 2023 17:11:26 -0800
Subject: [PATCH] rm dead code

---
 src/math/lp/CMakeLists.txt                    |  1 -
 src/math/lp/lp_primal_core_solver.h           |  2 --
 src/math/lp/lp_primal_core_solver_def.h       |  5 ----
 .../lp/lp_primal_core_solver_tableau_def.h    |  3 ++-
 src/math/lp/lp_utils.cpp                      | 26 -------------------
 5 files changed, 2 insertions(+), 35 deletions(-)
 delete mode 100644 src/math/lp/lp_utils.cpp

diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt
index 98241bf603e..4ca8cb1d2ae 100644
--- a/src/math/lp/CMakeLists.txt
+++ b/src/math/lp/CMakeLists.txt
@@ -20,7 +20,6 @@ z3_add_component(lp
     lp_core_solver_base.cpp
     lp_primal_core_solver.cpp
     lp_settings.cpp
-    lp_utils.cpp
     matrix.cpp
     mon_eq.cpp
     monomial_bounds.cpp
diff --git a/src/math/lp/lp_primal_core_solver.h b/src/math/lp/lp_primal_core_solver.h
index 17b1ea494d0..1719f9c556c 100644
--- a/src/math/lp/lp_primal_core_solver.h
+++ b/src/math/lp/lp_primal_core_solver.h
@@ -618,8 +618,6 @@ class lp_primal_core_solver:public lp_core_solver_base<T, X> {
     
     void print_bound_info_and_x(unsigned j, std::ostream & out);
     
-    unsigned solve_with_tableau();
-
     bool basis_column_is_set_correctly(unsigned j) const {
         return this->m_A.m_columns[j].size() == 1;
             
diff --git a/src/math/lp/lp_primal_core_solver_def.h b/src/math/lp/lp_primal_core_solver_def.h
index 1c48f11636c..cc8ad88b392 100644
--- a/src/math/lp/lp_primal_core_solver_def.h
+++ b/src/math/lp/lp_primal_core_solver_def.h
@@ -315,11 +315,6 @@ template <typename T, typename X>  unsigned lp_primal_core_solver<T, X>::get_num
 }
 
 
-// returns the number of iterations
-template <typename T, typename X> unsigned lp_primal_core_solver<T, X>::solve() {
-    TRACE("lar_solver", tout << "solve " << this->get_status() << "\n";);
-    return solve_with_tableau();
-}
 
 // calling it stage1 is too cryptic
 template <typename T, typename X>    void lp_primal_core_solver<T, X>::find_feasible_solution() {
diff --git a/src/math/lp/lp_primal_core_solver_tableau_def.h b/src/math/lp/lp_primal_core_solver_tableau_def.h
index de2f1c208af..c7b604b9553 100644
--- a/src/math/lp/lp_primal_core_solver_tableau_def.h
+++ b/src/math/lp/lp_primal_core_solver_tableau_def.h
@@ -87,7 +87,8 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::advance_on_e
 }
 
 template <typename T, typename X>
-unsigned lp_primal_core_solver<T, X>::solve_with_tableau() {
+unsigned lp_primal_core_solver<T, X>::solve() {
+    TRACE("lar_solver", tout << "solve " << this->get_status() << "\n";);
     init_run_tableau();
     if (this->current_x_is_feasible() && this->m_look_for_feasible_solution_only) {
         this->set_status(lp_status::FEASIBLE);
diff --git a/src/math/lp/lp_utils.cpp b/src/math/lp/lp_utils.cpp
deleted file mode 100644
index b909a0389d0..00000000000
--- a/src/math/lp/lp_utils.cpp
+++ /dev/null
@@ -1,26 +0,0 @@
-/*++
-Copyright (c) 2017 Microsoft Corporation
-
-Module Name:
-
-    <name>
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Lev Nachmanson (levnach)
-
-Revision History:
-
-
---*/
-#include "math/lp/lp_utils.h"
-#ifdef lp_for_z3
-namespace lp {
-
-}
-#endif
-