From 33cbd29ed0e0ef9224a79b035617404a1b604b5c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 3 Jun 2019 16:46:19 -0700 Subject: [PATCH] mv util/lp to math/lp Signed-off-by: Lev Nachmanson --- src/{util => math}/lp/CMakeLists.txt | 0 src/{util => math}/lp/active_set.h | 2 +- .../lp/binary_heap_priority_queue.cpp | 4 +- .../lp/binary_heap_priority_queue.h | 2 +- .../lp/binary_heap_priority_queue_def.h | 2 +- .../lp/binary_heap_upair_queue.cpp | 2 +- .../lp/binary_heap_upair_queue.h | 2 +- .../lp/binary_heap_upair_queue_def.h | 4 +- src/{util => math}/lp/bound_analyzer_on_row.h | 2 +- src/{util => math}/lp/bound_propagator.h | 2 +- src/{util => math}/lp/breakpoint.h | 0 src/{util => math}/lp/column_info.h | 2 +- src/{util => math}/lp/column_namer.h | 2 +- src/{util => math}/lp/constraint.h | 0 src/{util => math}/lp/conversion_helper.h | 0 .../lp/core_solver_pretty_printer.cpp | 4 +- .../lp/core_solver_pretty_printer.h | 4 +- .../lp/core_solver_pretty_printer_def.h | 8 +- src/{util => math}/lp/dense_matrix.cpp | 4 +- src/{util => math}/lp/dense_matrix.h | 2 +- src/{util => math}/lp/dense_matrix_def.h | 6 +- src/{util => math}/lp/emonomials.cpp | 6 +- src/{util => math}/lp/emonomials.h | 6 +- src/{util => math}/lp/eta_matrix.cpp | 4 +- src/{util => math}/lp/eta_matrix.h | 4 +- src/{util => math}/lp/eta_matrix_def.h | 2 +- src/{util => math}/lp/explanation.h | 2 +- src/{util => math}/lp/factorization.cpp | 2 +- src/{util => math}/lp/factorization.h | 4 +- .../lp/factorization_factory_imp.cpp | 4 +- .../lp/factorization_factory_imp.h | 2 +- src/{util => math}/lp/general_matrix.h | 0 src/{util => math}/lp/gomory.cpp | 8 +- src/{util => math}/lp/gomory.h | 8 +- src/{util => math}/lp/hnf.h | 2 +- src/{util => math}/lp/hnf_cutter.h | 12 +- src/{util => math}/lp/implied_bound.h | 4 +- src/{util => math}/lp/incremental_vector.h | 0 src/{util => math}/lp/indexed_value.h | 0 src/{util => math}/lp/indexed_vector.cpp | 2 +- src/{util => math}/lp/indexed_vector.h | 4 +- src/{util => math}/lp/indexed_vector_def.h | 4 +- .../lp/indexer_of_constraints.h | 2 +- src/{util => math}/lp/int_set.h | 2 +- src/{util => math}/lp/int_solver.cpp | 10 +- src/{util => math}/lp/int_solver.h | 16 +- src/{util => math}/lp/lar_constraints.h | 6 +- src/{util => math}/lp/lar_core_solver.cpp | 2 +- src/{util => math}/lp/lar_core_solver.h | 16 +- src/{util => math}/lp/lar_core_solver_def.h | 4 +- .../lp/lar_solution_signature.h | 2 +- src/{util => math}/lp/lar_solver.cpp | 2 +- src/{util => math}/lp/lar_solver.h | 28 +- src/{util => math}/lp/lar_term.h | 2 +- src/{util => math}/lp/lia_move.h | 0 src/{util => math}/lp/lp_bound_propagator.cpp | 2 +- src/{util => math}/lp/lp_core_solver_base.cpp | 2 +- src/{util => math}/lp/lp_core_solver_base.h | 14 +- .../lp/lp_core_solver_base_def.h | 4 +- src/{util => math}/lp/lp_dual_core_solver.cpp | 2 +- src/{util => math}/lp/lp_dual_core_solver.h | 4 +- .../lp/lp_dual_core_solver_def.h | 2 +- src/{util => math}/lp/lp_dual_simplex.cpp | 2 +- src/{util => math}/lp/lp_dual_simplex.h | 6 +- src/{util => math}/lp/lp_dual_simplex_def.h | 2 +- src/{util => math}/lp/lp_params.pyg | 0 .../lp/lp_primal_core_solver.cpp | 6 +- src/{util => math}/lp/lp_primal_core_solver.h | 16 +- .../lp/lp_primal_core_solver_def.h | 2 +- .../lp/lp_primal_core_solver_tableau_def.h | 2 +- src/{util => math}/lp/lp_primal_simplex.cpp | 2 +- src/{util => math}/lp/lp_primal_simplex.h | 8 +- src/{util => math}/lp/lp_primal_simplex_def.h | 2 +- src/{util => math}/lp/lp_settings.cpp | 2 +- src/{util => math}/lp/lp_settings.h | 4 +- src/{util => math}/lp/lp_settings_def.h | 2 +- src/{util => math}/lp/lp_solver.cpp | 2 +- src/{util => math}/lp/lp_solver.h | 12 +- src/{util => math}/lp/lp_solver_def.h | 2 +- src/{util => math}/lp/lp_types.h | 0 src/{util => math}/lp/lp_utils.cpp | 2 +- src/{util => math}/lp/lp_utils.h | 2 +- src/{util => math}/lp/lu.cpp | 2 +- src/{util => math}/lp/lu.h | 12 +- src/{util => math}/lp/lu_def.h | 2 +- src/{util => math}/lp/matrix.cpp | 6 +- src/{util => math}/lp/matrix.h | 4 +- src/{util => math}/lp/matrix_def.h | 2 +- src/{util => math}/lp/mon_eq.cpp | 4 +- src/{util => math}/lp/monomial.h | 6 +- src/{util => math}/lp/mps_reader.h | 10 +- src/{util => math}/lp/nla_basics_lemmas.cpp | 6 +- src/{util => math}/lp/nla_basics_lemmas.h | 6 +- src/{util => math}/lp/nla_common.cpp | 4 +- src/{util => math}/lp/nla_common.h | 10 +- src/{util => math}/lp/nla_core.cpp | 4 +- src/{util => math}/lp/nla_core.h | 17 +- src/{util => math}/lp/nla_defs.h | 6 +- src/{util => math}/lp/nla_monotone_lemmas.cpp | 6 +- src/{util => math}/lp/nla_monotone_lemmas.h | 0 src/{util => math}/lp/nla_order_lemmas.cpp | 8 +- src/{util => math}/lp/nla_order_lemmas.h | 4 +- src/{util => math}/lp/nla_params.pyg | 0 src/math/lp/nla_settings.h | 34 +++ src/{util => math}/lp/nla_solver.cpp | 12 +- src/{util => math}/lp/nla_solver.h | 8 +- src/{util => math}/lp/nla_tangent_lemmas.cpp | 4 +- src/{util => math}/lp/nla_tangent_lemmas.h | 4 +- src/{util => math}/lp/nra_solver.cpp | 6 +- src/{util => math}/lp/nra_solver.h | 2 +- src/{util => math}/lp/numeric_pair.h | 6 +- src/{util => math}/lp/permutation_matrix.cpp | 4 +- src/{util => math}/lp/permutation_matrix.h | 10 +- .../lp/permutation_matrix_def.h | 2 +- src/{util => math}/lp/polynomial.h | 0 src/{util => math}/lp/random_updater.cpp | 2 +- src/{util => math}/lp/random_updater.h | 2 +- src/{util => math}/lp/random_updater_def.h | 6 +- src/{util => math}/lp/row_eta_matrix.cpp | 4 +- src/{util => math}/lp/row_eta_matrix.h | 6 +- src/{util => math}/lp/row_eta_matrix_def.h | 2 +- src/{util => math}/lp/scaler.cpp | 2 +- src/{util => math}/lp/scaler.h | 4 +- src/{util => math}/lp/scaler_def.h | 4 +- .../lp/signature_bound_evidence.h | 4 +- src/{util => math}/lp/sparse_vector.h | 4 +- .../lp/square_dense_submatrix.cpp | 2 +- .../lp/square_dense_submatrix.h | 16 +- .../lp/square_dense_submatrix_def.h | 2 +- .../lp/square_sparse_matrix.cpp | 8 +- src/{util => math}/lp/square_sparse_matrix.h | 18 +- .../lp/square_sparse_matrix_def.h | 2 +- src/{util => math}/lp/stacked_value.h | 0 src/{util => math}/lp/stacked_vector.h | 0 src/{util => math}/lp/static_matrix.cpp | 14 +- src/{util => math}/lp/static_matrix.h | 6 +- src/{util => math}/lp/static_matrix_def.h | 2 +- src/{util => math}/lp/tail_matrix.h | 6 +- src/{util => math}/lp/test_bound_analyzer.h | 4 +- src/{util => math}/lp/ul_pair.h | 4 +- src/{util => math}/lp/var_eqs.h | 6 +- src/{util => math}/lp/var_register.h | 0 src/shell/lp_frontend.cpp | 6 +- src/smt/tactic/smt_tactic.cpp | 2 +- src/smt/theory_lra.cpp | 17 +- src/test/lp/gomory_test.h | 2 +- src/test/lp/lp.cpp | 276 +++++++++--------- src/test/lp/nla_solver_test.cpp | 11 +- src/test/lp/smt_reader.h | 12 +- src/test/lp/test_file_reader.h | 4 +- 150 files changed, 524 insertions(+), 479 deletions(-) rename src/{util => math}/lp/CMakeLists.txt (100%) rename src/{util => math}/lp/active_set.h (97%) rename src/{util => math}/lp/binary_heap_priority_queue.cpp (94%) rename src/{util => math}/lp/binary_heap_priority_queue.h (98%) rename src/{util => math}/lp/binary_heap_priority_queue_def.h (99%) rename src/{util => math}/lp/binary_heap_upair_queue.cpp (95%) rename src/{util => math}/lp/binary_heap_upair_queue.h (96%) rename src/{util => math}/lp/binary_heap_upair_queue_def.h (97%) rename src/{util => math}/lp/bound_analyzer_on_row.h (99%) rename src/{util => math}/lp/bound_propagator.h (97%) rename src/{util => math}/lp/breakpoint.h (100%) rename src/{util => math}/lp/column_info.h (99%) rename src/{util => math}/lp/column_namer.h (97%) rename src/{util => math}/lp/constraint.h (100%) rename src/{util => math}/lp/conversion_helper.h (100%) rename src/{util => math}/lp/core_solver_pretty_printer.cpp (93%) rename src/{util => math}/lp/core_solver_pretty_printer.h (97%) rename src/{util => math}/lp/core_solver_pretty_printer_def.h (98%) rename src/{util => math}/lp/dense_matrix.cpp (96%) rename src/{util => math}/lp/dense_matrix.h (99%) rename src/{util => math}/lp/dense_matrix_def.h (98%) rename src/{util => math}/lp/emonomials.cpp (99%) rename src/{util => math}/lp/emonomials.h (99%) rename src/{util => math}/lp/eta_matrix.cpp (96%) rename src/{util => math}/lp/eta_matrix.h (96%) rename src/{util => math}/lp/eta_matrix_def.h (99%) rename src/{util => math}/lp/explanation.h (97%) rename src/{util => math}/lp/factorization.cpp (99%) rename src/{util => math}/lp/factorization.h (98%) rename src/{util => math}/lp/factorization_factory_imp.cpp (91%) rename src/{util => math}/lp/factorization_factory_imp.h (95%) rename src/{util => math}/lp/general_matrix.h (100%) rename src/{util => math}/lp/gomory.cpp (99%) rename src/{util => math}/lp/gomory.h (79%) rename src/{util => math}/lp/hnf.h (99%) rename src/{util => math}/lp/hnf_cutter.h (97%) rename src/{util => math}/lp/implied_bound.h (95%) rename src/{util => math}/lp/incremental_vector.h (100%) rename src/{util => math}/lp/indexed_value.h (100%) rename src/{util => math}/lp/indexed_vector.cpp (98%) rename src/{util => math}/lp/indexed_vector.h (98%) rename src/{util => math}/lp/indexed_vector_def.h (97%) rename src/{util => math}/lp/indexer_of_constraints.h (94%) rename src/{util => math}/lp/int_set.h (97%) rename src/{util => math}/lp/int_solver.cpp (99%) rename src/{util => math}/lp/int_solver.h (95%) rename src/{util => math}/lp/lar_constraints.h (96%) rename src/{util => math}/lp/lar_core_solver.cpp (86%) rename src/{util => math}/lp/lar_core_solver.h (98%) rename src/{util => math}/lp/lar_core_solver_def.h (99%) rename src/{util => math}/lp/lar_solution_signature.h (91%) rename src/{util => math}/lp/lar_solver.cpp (99%) rename src/{util => math}/lp/lar_solver.h (97%) rename src/{util => math}/lp/lar_term.h (99%) rename src/{util => math}/lp/lia_move.h (100%) rename src/{util => math}/lp/lp_bound_propagator.cpp (98%) rename src/{util => math}/lp/lp_core_solver_base.cpp (99%) rename src/{util => math}/lp/lp_core_solver_base.h (98%) rename src/{util => math}/lp/lp_core_solver_base_def.h (99%) rename src/{util => math}/lp/lp_dual_core_solver.cpp (97%) rename src/{util => math}/lp/lp_dual_core_solver.h (98%) rename src/{util => math}/lp/lp_dual_core_solver_def.h (99%) rename src/{util => math}/lp/lp_dual_simplex.cpp (92%) rename src/{util => math}/lp/lp_dual_simplex.h (95%) rename src/{util => math}/lp/lp_dual_simplex_def.h (99%) rename src/{util => math}/lp/lp_params.pyg (100%) rename src/{util => math}/lp/lp_primal_core_solver.cpp (89%) rename src/{util => math}/lp/lp_primal_core_solver.h (99%) rename src/{util => math}/lp/lp_primal_core_solver_def.h (99%) rename src/{util => math}/lp/lp_primal_core_solver_tableau_def.h (99%) rename src/{util => math}/lp/lp_primal_simplex.cpp (96%) rename src/{util => math}/lp/lp_primal_simplex.h (94%) rename src/{util => math}/lp/lp_primal_simplex_def.h (99%) rename src/{util => math}/lp/lp_settings.cpp (91%) rename src/{util => math}/lp/lp_settings.h (99%) rename src/{util => math}/lp/lp_settings_def.h (99%) rename src/{util => math}/lp/lp_solver.cpp (98%) rename src/{util => math}/lp/lp_solver.h (97%) rename src/{util => math}/lp/lp_solver_def.h (99%) rename src/{util => math}/lp/lp_types.h (100%) rename src/{util => math}/lp/lp_utils.cpp (90%) rename src/{util => math}/lp/lp_utils.h (99%) rename src/{util => math}/lp/lu.cpp (99%) rename src/{util => math}/lp/lu.h (98%) rename src/{util => math}/lp/lu_def.h (99%) rename src/{util => math}/lp/matrix.cpp (89%) rename src/{util => math}/lp/matrix.h (96%) rename src/{util => math}/lp/matrix_def.h (99%) rename src/{util => math}/lp/mon_eq.cpp (94%) rename src/{util => math}/lp/monomial.h (96%) rename src/{util => math}/lp/mps_reader.h (99%) rename src/{util => math}/lp/nla_basics_lemmas.cpp (99%) rename src/{util => math}/lp/nla_basics_lemmas.h (97%) rename src/{util => math}/lp/nla_common.cpp (98%) rename src/{util => math}/lp/nla_common.h (94%) rename src/{util => math}/lp/nla_core.cpp (99%) rename src/{util => math}/lp/nla_core.h (97%) rename src/{util => math}/lp/nla_defs.h (96%) rename src/{util => math}/lp/nla_monotone_lemmas.cpp (96%) rename src/{util => math}/lp/nla_monotone_lemmas.h (100%) rename src/{util => math}/lp/nla_order_lemmas.cpp (98%) rename src/{util => math}/lp/nla_order_lemmas.h (97%) rename src/{util => math}/lp/nla_params.pyg (100%) create mode 100644 src/math/lp/nla_settings.h rename src/{util => math}/lp/nla_solver.cpp (81%) rename src/{util => math}/lp/nla_solver.h (85%) rename src/{util => math}/lp/nla_tangent_lemmas.cpp (98%) rename src/{util => math}/lp/nla_tangent_lemmas.h (97%) rename src/{util => math}/lp/nra_solver.cpp (98%) rename src/{util => math}/lp/nra_solver.h (97%) rename src/{util => math}/lp/numeric_pair.h (99%) rename src/{util => math}/lp/permutation_matrix.cpp (98%) rename src/{util => math}/lp/permutation_matrix.h (96%) rename src/{util => math}/lp/permutation_matrix_def.h (99%) rename src/{util => math}/lp/polynomial.h (100%) rename src/{util => math}/lp/random_updater.cpp (80%) rename src/{util => math}/lp/random_updater.h (97%) rename src/{util => math}/lp/random_updater_def.h (95%) rename src/{util => math}/lp/row_eta_matrix.cpp (97%) rename src/{util => math}/lp/row_eta_matrix.h (95%) rename src/{util => math}/lp/row_eta_matrix_def.h (99%) rename src/{util => math}/lp/scaler.cpp (89%) rename src/{util => math}/lp/scaler.h (96%) rename src/{util => math}/lp/scaler_def.h (99%) rename src/{util => math}/lp/signature_bound_evidence.h (89%) rename src/{util => math}/lp/sparse_vector.h (93%) rename src/{util => math}/lp/square_dense_submatrix.cpp (98%) rename src/{util => math}/lp/square_dense_submatrix.h (95%) rename src/{util => math}/lp/square_dense_submatrix_def.h (99%) rename src/{util => math}/lp/square_sparse_matrix.cpp (98%) rename src/{util => math}/lp/square_sparse_matrix.h (97%) rename src/{util => math}/lp/square_sparse_matrix_def.h (99%) rename src/{util => math}/lp/stacked_value.h (100%) rename src/{util => math}/lp/stacked_vector.h (100%) rename src/{util => math}/lp/static_matrix.cpp (94%) rename src/{util => math}/lp/static_matrix.h (99%) rename src/{util => math}/lp/static_matrix_def.h (99%) rename src/{util => math}/lp/tail_matrix.h (91%) rename src/{util => math}/lp/test_bound_analyzer.h (99%) rename src/{util => math}/lp/ul_pair.h (97%) rename src/{util => math}/lp/var_eqs.h (99%) rename src/{util => math}/lp/var_register.h (100%) diff --git a/src/util/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt similarity index 100% rename from src/util/lp/CMakeLists.txt rename to src/math/lp/CMakeLists.txt diff --git a/src/util/lp/active_set.h b/src/math/lp/active_set.h similarity index 97% rename from src/util/lp/active_set.h rename to src/math/lp/active_set.h index 587570559..3b2ead8c2 100644 --- a/src/util/lp/active_set.h +++ b/src/math/lp/active_set.h @@ -19,7 +19,7 @@ Revision History: --*/ #pragma once -#include "util/lp/binary_heap_priority_queue.h" +#include "math/lp/binary_heap_priority_queue.h" namespace lp { class active_set { std::unordered_set m_cs; diff --git a/src/util/lp/binary_heap_priority_queue.cpp b/src/math/lp/binary_heap_priority_queue.cpp similarity index 94% rename from src/util/lp/binary_heap_priority_queue.cpp rename to src/math/lp/binary_heap_priority_queue.cpp index 89b9dba6f..bbe735e58 100644 --- a/src/util/lp/binary_heap_priority_queue.cpp +++ b/src/math/lp/binary_heap_priority_queue.cpp @@ -17,8 +17,8 @@ Revision History: --*/ -#include "util/lp/numeric_pair.h" -#include "util/lp/binary_heap_priority_queue_def.h" +#include "math/lp/numeric_pair.h" +#include "math/lp/binary_heap_priority_queue_def.h" namespace lp { template binary_heap_priority_queue::binary_heap_priority_queue(unsigned int); template unsigned binary_heap_priority_queue::dequeue(); diff --git a/src/util/lp/binary_heap_priority_queue.h b/src/math/lp/binary_heap_priority_queue.h similarity index 98% rename from src/util/lp/binary_heap_priority_queue.h rename to src/math/lp/binary_heap_priority_queue.h index 018d154ab..1ea8363ef 100644 --- a/src/util/lp/binary_heap_priority_queue.h +++ b/src/math/lp/binary_heap_priority_queue.h @@ -21,7 +21,7 @@ Revision History: #pragma once #include "util/vector.h" #include "util/debug.h" -#include "util/lp/lp_utils.h" +#include "math/lp/lp_utils.h" namespace lp { // the elements with the smallest priority are dequeued first template diff --git a/src/util/lp/binary_heap_priority_queue_def.h b/src/math/lp/binary_heap_priority_queue_def.h similarity index 99% rename from src/util/lp/binary_heap_priority_queue_def.h rename to src/math/lp/binary_heap_priority_queue_def.h index d0a08c27d..c17d70fb2 100644 --- a/src/util/lp/binary_heap_priority_queue_def.h +++ b/src/math/lp/binary_heap_priority_queue_def.h @@ -18,7 +18,7 @@ Revision History: --*/ #include "util/vector.h" -#include "util/lp/binary_heap_priority_queue.h" +#include "math/lp/binary_heap_priority_queue.h" namespace lp { // "i" is the child's place in the heap template void binary_heap_priority_queue::swap_with_parent(unsigned i) { diff --git a/src/util/lp/binary_heap_upair_queue.cpp b/src/math/lp/binary_heap_upair_queue.cpp similarity index 95% rename from src/util/lp/binary_heap_upair_queue.cpp rename to src/math/lp/binary_heap_upair_queue.cpp index a521f7058..f1ff1d639 100644 --- a/src/util/lp/binary_heap_upair_queue.cpp +++ b/src/math/lp/binary_heap_upair_queue.cpp @@ -17,7 +17,7 @@ Revision History: --*/ -#include "util/lp/binary_heap_upair_queue_def.h" +#include "math/lp/binary_heap_upair_queue_def.h" namespace lp { template binary_heap_upair_queue::binary_heap_upair_queue(unsigned int); template binary_heap_upair_queue::binary_heap_upair_queue(unsigned int); diff --git a/src/util/lp/binary_heap_upair_queue.h b/src/math/lp/binary_heap_upair_queue.h similarity index 96% rename from src/util/lp/binary_heap_upair_queue.h rename to src/math/lp/binary_heap_upair_queue.h index 640c4bb81..ce4542803 100644 --- a/src/util/lp/binary_heap_upair_queue.h +++ b/src/math/lp/binary_heap_upair_queue.h @@ -25,7 +25,7 @@ Revision History: #include "util/vector.h" #include #include -#include "util/lp/binary_heap_priority_queue.h" +#include "math/lp/binary_heap_priority_queue.h" typedef std::pair upair; diff --git a/src/util/lp/binary_heap_upair_queue_def.h b/src/math/lp/binary_heap_upair_queue_def.h similarity index 97% rename from src/util/lp/binary_heap_upair_queue_def.h rename to src/math/lp/binary_heap_upair_queue_def.h index e9f3d424a..a74f9e46a 100644 --- a/src/util/lp/binary_heap_upair_queue_def.h +++ b/src/math/lp/binary_heap_upair_queue_def.h @@ -19,8 +19,8 @@ Revision History: --*/ #include -#include "util/lp/lp_utils.h" -#include "util/lp/binary_heap_upair_queue.h" +#include "math/lp/lp_utils.h" +#include "math/lp/binary_heap_upair_queue.h" namespace lp { template binary_heap_upair_queue::binary_heap_upair_queue(unsigned size) : m_q(size), m_pairs(size) { for (unsigned i = 0; i < size; i++) diff --git a/src/util/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h similarity index 99% rename from src/util/lp/bound_analyzer_on_row.h rename to src/math/lp/bound_analyzer_on_row.h index 0c6527dd5..22c40a753 100644 --- a/src/util/lp/bound_analyzer_on_row.h +++ b/src/math/lp/bound_analyzer_on_row.h @@ -21,7 +21,7 @@ Revision History: #include "util/vector.h" #include "implied_bound.h" #include "test_bound_analyzer.h" -#include "util/lp/bound_propagator.h" +#include "math/lp/bound_propagator.h" // We have an equality : sum by j of row[j]*x[j] = rs // We try to pin a var by pushing the total by using the variable bounds // In a loop we drive the partial sum down, denoting the variables of this process by _u. diff --git a/src/util/lp/bound_propagator.h b/src/math/lp/bound_propagator.h similarity index 97% rename from src/util/lp/bound_propagator.h rename to src/math/lp/bound_propagator.h index a1f0301aa..a75cabf6d 100644 --- a/src/util/lp/bound_propagator.h +++ b/src/math/lp/bound_propagator.h @@ -3,7 +3,7 @@ Author: Lev Nachmanson */ #pragma once -#include "util/lp/lp_settings.h" +#include "math/lp/lp_settings.h" namespace lp { class lar_solver; class bound_propagator { diff --git a/src/util/lp/breakpoint.h b/src/math/lp/breakpoint.h similarity index 100% rename from src/util/lp/breakpoint.h rename to src/math/lp/breakpoint.h diff --git a/src/util/lp/column_info.h b/src/math/lp/column_info.h similarity index 99% rename from src/util/lp/column_info.h rename to src/math/lp/column_info.h index 2a38900c1..1dc0c60c7 100644 --- a/src/util/lp/column_info.h +++ b/src/math/lp/column_info.h @@ -23,7 +23,7 @@ Revision History: #include #include #include -#include "util/lp/lp_settings.h" +#include "math/lp/lp_settings.h" namespace lp { inline bool is_valid(unsigned j) { return static_cast(j) >= 0;} diff --git a/src/util/lp/column_namer.h b/src/math/lp/column_namer.h similarity index 97% rename from src/util/lp/column_namer.h rename to src/math/lp/column_namer.h index 2ddc248fd..2352bd99a 100644 --- a/src/util/lp/column_namer.h +++ b/src/math/lp/column_namer.h @@ -19,7 +19,7 @@ Revision History: --*/ #include -#include "util/lp/static_matrix.h" +#include "math/lp/static_matrix.h" namespace lp { class column_namer { public: diff --git a/src/util/lp/constraint.h b/src/math/lp/constraint.h similarity index 100% rename from src/util/lp/constraint.h rename to src/math/lp/constraint.h diff --git a/src/util/lp/conversion_helper.h b/src/math/lp/conversion_helper.h similarity index 100% rename from src/util/lp/conversion_helper.h rename to src/math/lp/conversion_helper.h diff --git a/src/util/lp/core_solver_pretty_printer.cpp b/src/math/lp/core_solver_pretty_printer.cpp similarity index 93% rename from src/util/lp/core_solver_pretty_printer.cpp rename to src/math/lp/core_solver_pretty_printer.cpp index 3cba2240d..cd9c1a68b 100644 --- a/src/util/lp/core_solver_pretty_printer.cpp +++ b/src/math/lp/core_solver_pretty_printer.cpp @@ -17,8 +17,8 @@ Revision History: --*/ -#include "util/lp/numeric_pair.h" -#include "util/lp/core_solver_pretty_printer_def.h" +#include "math/lp/numeric_pair.h" +#include "math/lp/core_solver_pretty_printer_def.h" template lp::core_solver_pretty_printer::core_solver_pretty_printer(lp::lp_core_solver_base &, std::ostream & out); template void lp::core_solver_pretty_printer::print(); template lp::core_solver_pretty_printer::~core_solver_pretty_printer(); diff --git a/src/util/lp/core_solver_pretty_printer.h b/src/math/lp/core_solver_pretty_printer.h similarity index 97% rename from src/util/lp/core_solver_pretty_printer.h rename to src/math/lp/core_solver_pretty_printer.h index 2f2c61f7b..990fd94ed 100644 --- a/src/util/lp/core_solver_pretty_printer.h +++ b/src/math/lp/core_solver_pretty_printer.h @@ -23,8 +23,8 @@ Revision History: #include #include "util/vector.h" #include -#include "util/lp/lp_settings.h" -#include "util/lp/indexed_vector.h" +#include "math/lp/lp_settings.h" +#include "math/lp/indexed_vector.h" namespace lp { template class lp_core_solver_base; // forward definition diff --git a/src/util/lp/core_solver_pretty_printer_def.h b/src/math/lp/core_solver_pretty_printer_def.h similarity index 98% rename from src/util/lp/core_solver_pretty_printer_def.h rename to src/math/lp/core_solver_pretty_printer_def.h index 5453c6085..828e10cce 100644 --- a/src/util/lp/core_solver_pretty_printer_def.h +++ b/src/math/lp/core_solver_pretty_printer_def.h @@ -20,10 +20,10 @@ Revision History: #include #include #include -#include "util/lp/lp_utils.h" -#include "util/lp/lp_core_solver_base.h" -#include "util/lp/core_solver_pretty_printer.h" -#include "util/lp/numeric_pair.h" +#include "math/lp/lp_utils.h" +#include "math/lp/lp_core_solver_base.h" +#include "math/lp/core_solver_pretty_printer.h" +#include "math/lp/numeric_pair.h" namespace lp { diff --git a/src/util/lp/dense_matrix.cpp b/src/math/lp/dense_matrix.cpp similarity index 96% rename from src/util/lp/dense_matrix.cpp rename to src/math/lp/dense_matrix.cpp index 4ababc47a..f12e688d3 100644 --- a/src/util/lp/dense_matrix.cpp +++ b/src/math/lp/dense_matrix.cpp @@ -17,8 +17,8 @@ Revision History: --*/ -#include "util/lp/lp_settings.h" -#include "util/lp/dense_matrix_def.h" +#include "math/lp/lp_settings.h" +#include "math/lp/dense_matrix_def.h" #ifdef Z3DEBUG #include "util/vector.h" template lp::dense_matrix lp::operator*(lp::matrix&, lp::matrix&); diff --git a/src/util/lp/dense_matrix.h b/src/math/lp/dense_matrix.h similarity index 99% rename from src/util/lp/dense_matrix.h rename to src/math/lp/dense_matrix.h index e1f34ecd9..342fc7aeb 100644 --- a/src/util/lp/dense_matrix.h +++ b/src/math/lp/dense_matrix.h @@ -20,7 +20,7 @@ Revision History: #pragma once #ifdef Z3DEBUG #include "util/vector.h" -#include "util/lp/matrix.h" +#include "math/lp/matrix.h" namespace lp { // used for debugging purposes only template diff --git a/src/util/lp/dense_matrix_def.h b/src/math/lp/dense_matrix_def.h similarity index 98% rename from src/util/lp/dense_matrix_def.h rename to src/math/lp/dense_matrix_def.h index f615c412d..f781dbf8f 100644 --- a/src/util/lp/dense_matrix_def.h +++ b/src/math/lp/dense_matrix_def.h @@ -17,11 +17,11 @@ Revision History: --*/ -#include "util/lp/lp_settings.h" +#include "math/lp/lp_settings.h" #ifdef Z3DEBUG #include "util/vector.h" -#include "util/lp/numeric_pair.h" -#include "util/lp/dense_matrix.h" +#include "math/lp/numeric_pair.h" +#include "math/lp/dense_matrix.h" namespace lp { template dense_matrix::dense_matrix(unsigned m, unsigned n) : m_m(m), m_n(n), m_values(m * n, numeric_traits::zero()) { } diff --git a/src/util/lp/emonomials.cpp b/src/math/lp/emonomials.cpp similarity index 99% rename from src/util/lp/emonomials.cpp rename to src/math/lp/emonomials.cpp index 80ac9a54f..dd73cc171 100644 --- a/src/util/lp/emonomials.cpp +++ b/src/math/lp/emonomials.cpp @@ -19,9 +19,9 @@ --*/ -#include "util/lp/emonomials.h" -#include "util/lp/nla_defs.h" -#include "util/lp/nla_core.h" +#include "math/lp/emonomials.h" +#include "math/lp/nla_defs.h" +#include "math/lp/nla_core.h" namespace nla { diff --git a/src/util/lp/emonomials.h b/src/math/lp/emonomials.h similarity index 99% rename from src/util/lp/emonomials.h rename to src/math/lp/emonomials.h index dd0325282..5b0979946 100644 --- a/src/util/lp/emonomials.h +++ b/src/math/lp/emonomials.h @@ -20,9 +20,9 @@ --*/ #pragma once -#include "util/lp/lp_utils.h" -#include "util/lp/var_eqs.h" -#include "util/lp/monomial.h" +#include "math/lp/lp_utils.h" +#include "math/lp/var_eqs.h" +#include "math/lp/monomial.h" #include "util/region.h" namespace nla { diff --git a/src/util/lp/eta_matrix.cpp b/src/math/lp/eta_matrix.cpp similarity index 96% rename from src/util/lp/eta_matrix.cpp rename to src/math/lp/eta_matrix.cpp index 4cb43d87f..77f538426 100644 --- a/src/util/lp/eta_matrix.cpp +++ b/src/math/lp/eta_matrix.cpp @@ -19,8 +19,8 @@ Revision History: --*/ #include #include "util/vector.h" -#include "util/lp/numeric_pair.h" -#include "util/lp/eta_matrix_def.h" +#include "math/lp/numeric_pair.h" +#include "math/lp/eta_matrix_def.h" #ifdef Z3DEBUG template double lp::eta_matrix::get_elem(unsigned int, unsigned int) const; template lp::mpq lp::eta_matrix::get_elem(unsigned int, unsigned int) const; diff --git a/src/util/lp/eta_matrix.h b/src/math/lp/eta_matrix.h similarity index 96% rename from src/util/lp/eta_matrix.h rename to src/math/lp/eta_matrix.h index a811492f7..14fe3ffea 100644 --- a/src/util/lp/eta_matrix.h +++ b/src/math/lp/eta_matrix.h @@ -20,8 +20,8 @@ Revision History: #pragma once #include "util/vector.h" -#include "util/lp/tail_matrix.h" -#include "util/lp/permutation_matrix.h" +#include "math/lp/tail_matrix.h" +#include "math/lp/permutation_matrix.h" namespace lp { // This is the sum of a unit matrix and a one-column matrix diff --git a/src/util/lp/eta_matrix_def.h b/src/math/lp/eta_matrix_def.h similarity index 99% rename from src/util/lp/eta_matrix_def.h rename to src/math/lp/eta_matrix_def.h index 774cc89dc..a6c908572 100644 --- a/src/util/lp/eta_matrix_def.h +++ b/src/math/lp/eta_matrix_def.h @@ -20,7 +20,7 @@ Revision History: #pragma once #include "util/vector.h" -#include "util/lp/eta_matrix.h" +#include "math/lp/eta_matrix.h" namespace lp { // This is the sum of a unit matrix and a one-column matrix diff --git a/src/util/lp/explanation.h b/src/math/lp/explanation.h similarity index 97% rename from src/util/lp/explanation.h rename to src/math/lp/explanation.h index 9388e1d53..b2558818e 100644 --- a/src/util/lp/explanation.h +++ b/src/math/lp/explanation.h @@ -19,7 +19,7 @@ Revision History: --*/ #pragma once #include -#include "util/lp/lp_utils.h" +#include "math/lp/lp_utils.h" namespace lp { class explanation { vector> m_explanation; diff --git a/src/util/lp/factorization.cpp b/src/math/lp/factorization.cpp similarity index 99% rename from src/util/lp/factorization.cpp rename to src/math/lp/factorization.cpp index ec112b6de..7f51c2f50 100644 --- a/src/util/lp/factorization.cpp +++ b/src/math/lp/factorization.cpp @@ -1,5 +1,5 @@ #include "util/vector.h" -#include "util/lp/factorization.h" +#include "math/lp/factorization.h" namespace nla { void const_iterator_mon::init_vars_by_the_mask(unsigned_vector & k_vars, unsigned_vector & j_vars) const { diff --git a/src/util/lp/factorization.h b/src/math/lp/factorization.h similarity index 98% rename from src/util/lp/factorization.h rename to src/math/lp/factorization.h index 75a86f119..9e3981fe4 100644 --- a/src/util/lp/factorization.h +++ b/src/math/lp/factorization.h @@ -20,8 +20,8 @@ --*/ #pragma once #include "util/rational.h" -#include "util/lp/monomial.h" -#include "util/lp/nla_defs.h" +#include "math/lp/monomial.h" +#include "math/lp/nla_defs.h" namespace nla { diff --git a/src/util/lp/factorization_factory_imp.cpp b/src/math/lp/factorization_factory_imp.cpp similarity index 91% rename from src/util/lp/factorization_factory_imp.cpp rename to src/math/lp/factorization_factory_imp.cpp index faed2ea2e..e60c83514 100644 --- a/src/util/lp/factorization_factory_imp.cpp +++ b/src/math/lp/factorization_factory_imp.cpp @@ -17,8 +17,8 @@ --*/ -#include "util/lp/factorization_factory_imp.h" -#include "util/lp/nla_core.h" +#include "math/lp/factorization_factory_imp.h" +#include "math/lp/nla_core.h" namespace nla { factorization_factory_imp::factorization_factory_imp(const monomial& rm, const core& s) : diff --git a/src/util/lp/factorization_factory_imp.h b/src/math/lp/factorization_factory_imp.h similarity index 95% rename from src/util/lp/factorization_factory_imp.h rename to src/math/lp/factorization_factory_imp.h index 7278d9af8..b24c2bfe7 100644 --- a/src/util/lp/factorization_factory_imp.h +++ b/src/math/lp/factorization_factory_imp.h @@ -18,7 +18,7 @@ --*/ #pragma once -#include "util/lp/factorization.h" +#include "math/lp/factorization.h" namespace nla { class core; diff --git a/src/util/lp/general_matrix.h b/src/math/lp/general_matrix.h similarity index 100% rename from src/util/lp/general_matrix.h rename to src/math/lp/general_matrix.h diff --git a/src/util/lp/gomory.cpp b/src/math/lp/gomory.cpp similarity index 99% rename from src/util/lp/gomory.cpp rename to src/math/lp/gomory.cpp index 80a87467a..aa12e3efd 100644 --- a/src/util/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -17,10 +17,10 @@ --*/ -#include "util/lp/gomory.h" -#include "util/lp/int_solver.h" -#include "util/lp/lar_solver.h" -#include "util/lp/lp_utils.h" +#include "math/lp/gomory.h" +#include "math/lp/int_solver.h" +#include "math/lp/lar_solver.h" +#include "math/lp/lp_utils.h" namespace lp { class gomory::imp { diff --git a/src/util/lp/gomory.h b/src/math/lp/gomory.h similarity index 79% rename from src/util/lp/gomory.h rename to src/math/lp/gomory.h index 7e5e081e1..48c79cffe 100644 --- a/src/util/lp/gomory.h +++ b/src/math/lp/gomory.h @@ -16,10 +16,10 @@ Author: Revision History: --*/ #pragma once -#include "util/lp/lar_term.h" -#include "util/lp/lia_move.h" -#include "util/lp/explanation.h" -#include "util/lp/static_matrix.h" +#include "math/lp/lar_term.h" +#include "math/lp/lia_move.h" +#include "math/lp/explanation.h" +#include "math/lp/static_matrix.h" namespace lp { class int_solver; diff --git a/src/util/lp/hnf.h b/src/math/lp/hnf.h similarity index 99% rename from src/util/lp/hnf.h rename to src/math/lp/hnf.h index b6828d053..75a69393f 100644 --- a/src/util/lp/hnf.h +++ b/src/math/lp/hnf.h @@ -27,7 +27,7 @@ Revision History: --*/ #pragma once -#include "util/lp/numeric_pair.h" +#include "math/lp/numeric_pair.h" #include "util/ext_gcd.h" namespace lp { namespace hnf_calc { diff --git a/src/util/lp/hnf_cutter.h b/src/math/lp/hnf_cutter.h similarity index 97% rename from src/util/lp/hnf_cutter.h rename to src/math/lp/hnf_cutter.h index 2e59e4be3..65c545613 100644 --- a/src/util/lp/hnf_cutter.h +++ b/src/math/lp/hnf_cutter.h @@ -17,12 +17,12 @@ Revision History: --*/ #pragma once -#include "util/lp/lar_term.h" -#include "util/lp/hnf.h" -#include "util/lp/general_matrix.h" -#include "util/lp/var_register.h" -#include "util/lp/lia_move.h" -#include "util/lp/explanation.h" +#include "math/lp/lar_term.h" +#include "math/lp/hnf.h" +#include "math/lp/general_matrix.h" +#include "math/lp/var_register.h" +#include "math/lp/lia_move.h" +#include "math/lp/explanation.h" namespace lp { class hnf_cutter { diff --git a/src/util/lp/implied_bound.h b/src/math/lp/implied_bound.h similarity index 95% rename from src/util/lp/implied_bound.h rename to src/math/lp/implied_bound.h index 6c5f26cf2..9435edcdc 100644 --- a/src/util/lp/implied_bound.h +++ b/src/math/lp/implied_bound.h @@ -18,8 +18,8 @@ Revision History: --*/ #pragma once -#include "util/lp/lp_settings.h" -#include "util/lp/lar_constraints.h" +#include "math/lp/lp_settings.h" +#include "math/lp/lar_constraints.h" namespace lp { struct implied_bound { mpq m_bound; diff --git a/src/util/lp/incremental_vector.h b/src/math/lp/incremental_vector.h similarity index 100% rename from src/util/lp/incremental_vector.h rename to src/math/lp/incremental_vector.h diff --git a/src/util/lp/indexed_value.h b/src/math/lp/indexed_value.h similarity index 100% rename from src/util/lp/indexed_value.h rename to src/math/lp/indexed_value.h diff --git a/src/util/lp/indexed_vector.cpp b/src/math/lp/indexed_vector.cpp similarity index 98% rename from src/util/lp/indexed_vector.cpp rename to src/math/lp/indexed_vector.cpp index 11378f151..d7cde2e1d 100644 --- a/src/util/lp/indexed_vector.cpp +++ b/src/math/lp/indexed_vector.cpp @@ -18,7 +18,7 @@ Revision History: --*/ #include "util/vector.h" -#include "util/lp/indexed_vector_def.h" +#include "math/lp/indexed_vector_def.h" namespace lp { template void indexed_vector::clear(); template void indexed_vector::clear_all(); diff --git a/src/util/lp/indexed_vector.h b/src/math/lp/indexed_vector.h similarity index 98% rename from src/util/lp/indexed_vector.h rename to src/math/lp/indexed_vector.h index 24078ce84..22d51e190 100644 --- a/src/util/lp/indexed_vector.h +++ b/src/math/lp/indexed_vector.h @@ -23,8 +23,8 @@ Revision History: #include "util/debug.h" #include #include -#include "util/lp/lp_utils.h" -#include "util/lp/lp_settings.h" +#include "math/lp/lp_utils.h" +#include "math/lp/lp_settings.h" #include namespace lp { diff --git a/src/util/lp/indexed_vector_def.h b/src/math/lp/indexed_vector_def.h similarity index 97% rename from src/util/lp/indexed_vector_def.h rename to src/math/lp/indexed_vector_def.h index a133eb379..443ca160e 100644 --- a/src/util/lp/indexed_vector_def.h +++ b/src/math/lp/indexed_vector_def.h @@ -18,8 +18,8 @@ Revision History: --*/ #include "util/vector.h" -#include "util/lp/indexed_vector.h" -#include "util/lp/lp_settings.h" +#include "math/lp/indexed_vector.h" +#include "math/lp/lp_settings.h" namespace lp { template diff --git a/src/util/lp/indexer_of_constraints.h b/src/math/lp/indexer_of_constraints.h similarity index 94% rename from src/util/lp/indexer_of_constraints.h rename to src/math/lp/indexer_of_constraints.h index 30976d496..9bda22bc1 100644 --- a/src/util/lp/indexer_of_constraints.h +++ b/src/math/lp/indexer_of_constraints.h @@ -19,7 +19,7 @@ Revision History: --*/ #pragma once -#include "util/lp/binary_heap_priority_queue.h" +#include "math/lp/binary_heap_priority_queue.h" namespace lp { class indexer_of_constraints { diff --git a/src/util/lp/int_set.h b/src/math/lp/int_set.h similarity index 97% rename from src/util/lp/int_set.h rename to src/math/lp/int_set.h index 058cf4114..3b749b93c 100644 --- a/src/util/lp/int_set.h +++ b/src/math/lp/int_set.h @@ -19,7 +19,7 @@ Revision History: --*/ #pragma once #include "util/vector.h" -#include "util/lp/indexed_vector.h" +#include "math/lp/indexed_vector.h" #include namespace lp { // serves at a set of non-negative integers smaller than the set size diff --git a/src/util/lp/int_solver.cpp b/src/math/lp/int_solver.cpp similarity index 99% rename from src/util/lp/int_solver.cpp rename to src/math/lp/int_solver.cpp index 20c398f49..b63af29c0 100644 --- a/src/util/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -3,12 +3,12 @@ Author: Lev Nachmanson */ -#include "util/lp/int_solver.h" -#include "util/lp/lar_solver.h" -#include "util/lp/lp_utils.h" +#include "math/lp/int_solver.h" +#include "math/lp/lar_solver.h" +#include "math/lp/lp_utils.h" #include -#include "util/lp/monomial.h" -#include "util/lp/gomory.h" +#include "math/lp/monomial.h" +#include "math/lp/gomory.h" namespace lp { diff --git a/src/util/lp/int_solver.h b/src/math/lp/int_solver.h similarity index 95% rename from src/util/lp/int_solver.h rename to src/math/lp/int_solver.h index fc4a3f5b1..a249df756 100644 --- a/src/util/lp/int_solver.h +++ b/src/math/lp/int_solver.h @@ -18,14 +18,14 @@ Revision History: --*/ #pragma once -#include "util/lp/lp_settings.h" -#include "util/lp/static_matrix.h" -#include "util/lp/int_set.h" -#include "util/lp/lar_term.h" -#include "util/lp/lar_constraints.h" -#include "util/lp/hnf_cutter.h" -#include "util/lp/lia_move.h" -#include "util/lp/explanation.h" +#include "math/lp/lp_settings.h" +#include "math/lp/static_matrix.h" +#include "math/lp/int_set.h" +#include "math/lp/lar_term.h" +#include "math/lp/lar_constraints.h" +#include "math/lp/hnf_cutter.h" +#include "math/lp/lia_move.h" +#include "math/lp/explanation.h" namespace lp { class lar_solver; diff --git a/src/util/lp/lar_constraints.h b/src/math/lp/lar_constraints.h similarity index 96% rename from src/util/lp/lar_constraints.h rename to src/math/lp/lar_constraints.h index ae6e3fd74..931f46687 100644 --- a/src/util/lp/lar_constraints.h +++ b/src/math/lp/lar_constraints.h @@ -24,9 +24,9 @@ Revision History: #include #include #include -#include "util/lp/lp_utils.h" -#include "util/lp/ul_pair.h" -#include "util/lp/lar_term.h" +#include "math/lp/lp_utils.h" +#include "math/lp/ul_pair.h" +#include "math/lp/lar_term.h" namespace lp { inline lconstraint_kind flip_kind(lconstraint_kind t) { return static_cast( - static_cast(t)); diff --git a/src/util/lp/lar_core_solver.cpp b/src/math/lp/lar_core_solver.cpp similarity index 86% rename from src/util/lp/lar_core_solver.cpp rename to src/math/lp/lar_core_solver.cpp index 95e516135..09d01f4cc 100644 --- a/src/util/lp/lar_core_solver.cpp +++ b/src/math/lp/lar_core_solver.cpp @@ -22,4 +22,4 @@ Revision History: #include #include "util/vector.h" #include -#include "util/lp/lar_core_solver_def.h" +#include "math/lp/lar_core_solver_def.h" diff --git a/src/util/lp/lar_core_solver.h b/src/math/lp/lar_core_solver.h similarity index 98% rename from src/util/lp/lar_core_solver.h rename to src/math/lp/lar_core_solver.h index 6c91850a1..67609aeb1 100644 --- a/src/util/lp/lar_core_solver.h +++ b/src/math/lp/lar_core_solver.h @@ -21,15 +21,15 @@ Revision History: #include "util/vector.h" #include #include -#include "util/lp/lp_core_solver_base.h" +#include "math/lp/lp_core_solver_base.h" #include -#include "util/lp/indexed_vector.h" -#include "util/lp/binary_heap_priority_queue.h" -#include "util/lp/breakpoint.h" -#include "util/lp/lp_primal_core_solver.h" -#include "util/lp/stacked_vector.h" -#include "util/lp/lar_solution_signature.h" -#include "util/lp/stacked_value.h" +#include "math/lp/indexed_vector.h" +#include "math/lp/binary_heap_priority_queue.h" +#include "math/lp/breakpoint.h" +#include "math/lp/lp_primal_core_solver.h" +#include "math/lp/stacked_vector.h" +#include "math/lp/lar_solution_signature.h" +#include "math/lp/stacked_value.h" namespace lp { class lar_core_solver { diff --git a/src/util/lp/lar_core_solver_def.h b/src/math/lp/lar_core_solver_def.h similarity index 99% rename from src/util/lp/lar_core_solver_def.h rename to src/math/lp/lar_core_solver_def.h index 7c54a3b6b..56fe669c4 100644 --- a/src/util/lp/lar_core_solver_def.h +++ b/src/math/lp/lar_core_solver_def.h @@ -38,8 +38,8 @@ Revision History: --*/ #include #include "util/vector.h" -#include "util/lp/lar_core_solver.h" -#include "util/lp/lar_solution_signature.h" +#include "math/lp/lar_core_solver.h" +#include "math/lp/lar_solution_signature.h" namespace lp { lar_core_solver::lar_core_solver( lp_settings & settings, diff --git a/src/util/lp/lar_solution_signature.h b/src/math/lp/lar_solution_signature.h similarity index 91% rename from src/util/lp/lar_solution_signature.h rename to src/math/lp/lar_solution_signature.h index 08551a2d0..5b8bfae48 100644 --- a/src/util/lp/lar_solution_signature.h +++ b/src/math/lp/lar_solution_signature.h @@ -21,7 +21,7 @@ Revision History: #pragma once #include "util/vector.h" #include "util/debug.h" -#include "util/lp/lp_settings.h" +#include "math/lp/lp_settings.h" #include namespace lp { typedef std::unordered_map lar_solution_signature; diff --git a/src/util/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp similarity index 99% rename from src/util/lp/lar_solver.cpp rename to src/math/lp/lar_solver.cpp index ae45198ce..53ef1f84f 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1,4 +1,4 @@ -#include "util/lp/lar_solver.h" +#include "math/lp/lar_solver.h" /* Copyright (c) 2017 Microsoft Corporation Author: Nikolaj Bjorner, Lev Nachmanson diff --git a/src/util/lp/lar_solver.h b/src/math/lp/lar_solver.h similarity index 97% rename from src/util/lp/lar_solver.h rename to src/math/lp/lar_solver.h index 8e117b67a..b3aa2ab7b 100644 --- a/src/util/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -25,23 +25,23 @@ Revision History: #include #include #include -#include "util/lp/lar_constraints.h" +#include "math/lp/lar_constraints.h" #include -#include "util/lp/lar_core_solver.h" +#include "math/lp/lar_core_solver.h" #include -#include "util/lp/numeric_pair.h" -#include "util/lp/scaler.h" -#include "util/lp/lp_primal_core_solver.h" -#include "util/lp/random_updater.h" +#include "math/lp/numeric_pair.h" +#include "math/lp/scaler.h" +#include "math/lp/lp_primal_core_solver.h" +#include "math/lp/random_updater.h" #include -#include "util/lp/stacked_value.h" -#include "util/lp/stacked_vector.h" -#include "util/lp/implied_bound.h" -#include "util/lp/bound_analyzer_on_row.h" -#include "util/lp/conversion_helper.h" -#include "util/lp/int_solver.h" -#include "util/lp/nra_solver.h" -#include "util/lp/bound_propagator.h" +#include "math/lp/stacked_value.h" +#include "math/lp/stacked_vector.h" +#include "math/lp/implied_bound.h" +#include "math/lp/bound_analyzer_on_row.h" +#include "math/lp/conversion_helper.h" +#include "math/lp/int_solver.h" +#include "math/lp/nra_solver.h" +#include "math/lp/bound_propagator.h" namespace lp { diff --git a/src/util/lp/lar_term.h b/src/math/lp/lar_term.h similarity index 99% rename from src/util/lp/lar_term.h rename to src/math/lp/lar_term.h index 53c5f2b16..cefbf0ce6 100644 --- a/src/util/lp/lar_term.h +++ b/src/math/lp/lar_term.h @@ -18,7 +18,7 @@ --*/ #pragma once -#include "util/lp/indexed_vector.h" +#include "math/lp/indexed_vector.h" #include "util/map.h" namespace lp { class lar_term { diff --git a/src/util/lp/lia_move.h b/src/math/lp/lia_move.h similarity index 100% rename from src/util/lp/lia_move.h rename to src/math/lp/lia_move.h diff --git a/src/util/lp/lp_bound_propagator.cpp b/src/math/lp/lp_bound_propagator.cpp similarity index 98% rename from src/util/lp/lp_bound_propagator.cpp rename to src/math/lp/lp_bound_propagator.cpp index a5c7c976a..ee25d8dd0 100644 --- a/src/util/lp/lp_bound_propagator.cpp +++ b/src/math/lp/lp_bound_propagator.cpp @@ -2,7 +2,7 @@ Copyright (c) 2017 Microsoft Corporation Author: Lev Nachmanson */ -#include "util/lp/lar_solver.h" +#include "math/lp/lar_solver.h" namespace lp { bound_propagator::bound_propagator(lar_solver & ls): m_lar_solver(ls) {} diff --git a/src/util/lp/lp_core_solver_base.cpp b/src/math/lp/lp_core_solver_base.cpp similarity index 99% rename from src/util/lp/lp_core_solver_base.cpp rename to src/math/lp/lp_core_solver_base.cpp index e71f65d5d..8219c3f26 100644 --- a/src/util/lp/lp_core_solver_base.cpp +++ b/src/math/lp/lp_core_solver_base.cpp @@ -22,7 +22,7 @@ Revision History: #include #include "util/vector.h" #include -#include "util/lp/lp_core_solver_base_def.h" +#include "math/lp/lp_core_solver_base_def.h" template bool lp::lp_core_solver_base::A_mult_x_is_off() const; template bool lp::lp_core_solver_base::A_mult_x_is_off_on_index(const vector &) const; template bool lp::lp_core_solver_base::basis_heading_is_correct() const; diff --git a/src/util/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h similarity index 98% rename from src/util/lp/lp_core_solver_base.h rename to src/math/lp/lp_core_solver_base.h index c88e33dd2..db7fd70ce 100644 --- a/src/util/lp/lp_core_solver_base.h +++ b/src/math/lp/lp_core_solver_base.h @@ -21,13 +21,13 @@ Revision History: #include #include "util/vector.h" #include -#include "util/lp/lp_utils.h" -#include "util/lp/core_solver_pretty_printer.h" -#include "util/lp/numeric_pair.h" -#include "util/lp/static_matrix.h" -#include "util/lp/lu.h" -#include "util/lp/permutation_matrix.h" -#include "util/lp/column_namer.h" +#include "math/lp/lp_utils.h" +#include "math/lp/core_solver_pretty_printer.h" +#include "math/lp/numeric_pair.h" +#include "math/lp/static_matrix.h" +#include "math/lp/lu.h" +#include "math/lp/permutation_matrix.h" +#include "math/lp/column_namer.h" namespace lp { diff --git a/src/util/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h similarity index 99% rename from src/util/lp/lp_core_solver_base_def.h rename to src/math/lp/lp_core_solver_base_def.h index 23529ffff..b5f5c222f 100644 --- a/src/util/lp/lp_core_solver_base_def.h +++ b/src/math/lp/lp_core_solver_base_def.h @@ -20,8 +20,8 @@ Revision History: #include #include #include "util/vector.h" -#include "util/lp/lp_utils.h" -#include "util/lp/lp_core_solver_base.h" +#include "math/lp/lp_utils.h" +#include "math/lp/lp_core_solver_base.h" namespace lp { template lp_core_solver_base:: diff --git a/src/util/lp/lp_dual_core_solver.cpp b/src/math/lp/lp_dual_core_solver.cpp similarity index 97% rename from src/util/lp/lp_dual_core_solver.cpp rename to src/math/lp/lp_dual_core_solver.cpp index bd8f605a7..8cf45f7c6 100644 --- a/src/util/lp/lp_dual_core_solver.cpp +++ b/src/math/lp/lp_dual_core_solver.cpp @@ -22,7 +22,7 @@ Revision History: #include #include "util/vector.h" #include -#include "util/lp/lp_dual_core_solver_def.h" +#include "math/lp/lp_dual_core_solver_def.h" template void lp::lp_dual_core_solver::start_with_initial_basis_and_make_it_dual_feasible(); template void lp::lp_dual_core_solver::solve(); template lp::lp_dual_core_solver::lp_dual_core_solver(lp::static_matrix&, vector&, diff --git a/src/util/lp/lp_dual_core_solver.h b/src/math/lp/lp_dual_core_solver.h similarity index 98% rename from src/util/lp/lp_dual_core_solver.h rename to src/math/lp/lp_dual_core_solver.h index c620aa096..f4aa4b44d 100644 --- a/src/util/lp/lp_dual_core_solver.h +++ b/src/math/lp/lp_dual_core_solver.h @@ -18,8 +18,8 @@ Revision History: --*/ #pragma once -#include "util/lp/static_matrix.h" -#include "util/lp/lp_core_solver_base.h" +#include "math/lp/static_matrix.h" +#include "math/lp/lp_core_solver_base.h" #include #include #include diff --git a/src/util/lp/lp_dual_core_solver_def.h b/src/math/lp/lp_dual_core_solver_def.h similarity index 99% rename from src/util/lp/lp_dual_core_solver_def.h rename to src/math/lp/lp_dual_core_solver_def.h index fba192f06..1e6553458 100644 --- a/src/util/lp/lp_dual_core_solver_def.h +++ b/src/math/lp/lp_dual_core_solver_def.h @@ -20,7 +20,7 @@ Revision History: #include #include #include "util/vector.h" -#include "util/lp/lp_dual_core_solver.h" +#include "math/lp/lp_dual_core_solver.h" namespace lp { diff --git a/src/util/lp/lp_dual_simplex.cpp b/src/math/lp/lp_dual_simplex.cpp similarity index 92% rename from src/util/lp/lp_dual_simplex.cpp rename to src/math/lp/lp_dual_simplex.cpp index ff71b7b4f..aaf612f56 100644 --- a/src/util/lp/lp_dual_simplex.cpp +++ b/src/math/lp/lp_dual_simplex.cpp @@ -17,7 +17,7 @@ Revision History: --*/ -#include "util/lp/lp_dual_simplex_def.h" +#include "math/lp/lp_dual_simplex_def.h" template lp::mpq lp::lp_dual_simplex::get_current_cost() const; template void lp::lp_dual_simplex::find_maximal_solution(); template double lp::lp_dual_simplex::get_current_cost() const; diff --git a/src/util/lp/lp_dual_simplex.h b/src/math/lp/lp_dual_simplex.h similarity index 95% rename from src/util/lp/lp_dual_simplex.h rename to src/math/lp/lp_dual_simplex.h index c33b55031..75ef87492 100644 --- a/src/util/lp/lp_dual_simplex.h +++ b/src/math/lp/lp_dual_simplex.h @@ -19,9 +19,9 @@ Revision History: --*/ #pragma once #include "util/vector.h" -#include "util/lp/lp_utils.h" -#include "util/lp/lp_solver.h" -#include "util/lp/lp_dual_core_solver.h" +#include "math/lp/lp_utils.h" +#include "math/lp/lp_solver.h" +#include "math/lp/lp_dual_core_solver.h" namespace lp { template diff --git a/src/util/lp/lp_dual_simplex_def.h b/src/math/lp/lp_dual_simplex_def.h similarity index 99% rename from src/util/lp/lp_dual_simplex_def.h rename to src/math/lp/lp_dual_simplex_def.h index e32a5e97f..1b12106ea 100644 --- a/src/util/lp/lp_dual_simplex_def.h +++ b/src/math/lp/lp_dual_simplex_def.h @@ -17,7 +17,7 @@ Revision History: --*/ -#include "util/lp/lp_dual_simplex.h" +#include "math/lp/lp_dual_simplex.h" namespace lp{ template void lp_dual_simplex::decide_on_status_after_stage1() { diff --git a/src/util/lp/lp_params.pyg b/src/math/lp/lp_params.pyg similarity index 100% rename from src/util/lp/lp_params.pyg rename to src/math/lp/lp_params.pyg diff --git a/src/util/lp/lp_primal_core_solver.cpp b/src/math/lp/lp_primal_core_solver.cpp similarity index 89% rename from src/util/lp/lp_primal_core_solver.cpp rename to src/math/lp/lp_primal_core_solver.cpp index f3eefa2b9..054391c62 100644 --- a/src/util/lp/lp_primal_core_solver.cpp +++ b/src/math/lp/lp_primal_core_solver.cpp @@ -22,9 +22,9 @@ Revision History: #include #include "util/vector.h" #include -#include "util/lp/lar_solver.h" -#include "util/lp/lp_primal_core_solver_def.h" -#include "util/lp/lp_primal_core_solver_tableau_def.h" +#include "math/lp/lar_solver.h" +#include "math/lp/lp_primal_core_solver_def.h" +#include "math/lp/lp_primal_core_solver_tableau_def.h" namespace lp { template void lp_primal_core_solver::find_feasible_solution(); diff --git a/src/util/lp/lp_primal_core_solver.h b/src/math/lp/lp_primal_core_solver.h similarity index 99% rename from src/util/lp/lp_primal_core_solver.h rename to src/math/lp/lp_primal_core_solver.h index 648c44470..98c8be009 100644 --- a/src/util/lp/lp_primal_core_solver.h +++ b/src/math/lp/lp_primal_core_solver.h @@ -29,14 +29,14 @@ Revision History: #include #include #include -#include "util/lp/lu.h" -#include "util/lp/lp_solver.h" -#include "util/lp/static_matrix.h" -#include "util/lp/core_solver_pretty_printer.h" -#include "util/lp/lp_core_solver_base.h" -#include "util/lp/breakpoint.h" -#include "util/lp/binary_heap_priority_queue.h" -#include "util/lp/int_set.h" +#include "math/lp/lu.h" +#include "math/lp/lp_solver.h" +#include "math/lp/static_matrix.h" +#include "math/lp/core_solver_pretty_printer.h" +#include "math/lp/lp_core_solver_base.h" +#include "math/lp/breakpoint.h" +#include "math/lp/binary_heap_priority_queue.h" +#include "math/lp/int_set.h" namespace lp { // This core solver solves (Ax=b, lower_bound_values \leq x \leq upper_bound_values, maximize costs*x ) diff --git a/src/util/lp/lp_primal_core_solver_def.h b/src/math/lp/lp_primal_core_solver_def.h similarity index 99% rename from src/util/lp/lp_primal_core_solver_def.h rename to src/math/lp/lp_primal_core_solver_def.h index a96abffd6..4e4b2e71e 100644 --- a/src/util/lp/lp_primal_core_solver_def.h +++ b/src/math/lp/lp_primal_core_solver_def.h @@ -23,7 +23,7 @@ Revision History: #include #include #include -#include "util/lp/lp_primal_core_solver.h" +#include "math/lp/lp_primal_core_solver.h" namespace lp { // This core solver solves (Ax=b, lower_bound_values \leq x \leq upper_bound_values, maximize costs*x ) // The right side b is given implicitly by x and the basis diff --git a/src/util/lp/lp_primal_core_solver_tableau_def.h b/src/math/lp/lp_primal_core_solver_tableau_def.h similarity index 99% rename from src/util/lp/lp_primal_core_solver_tableau_def.h rename to src/math/lp/lp_primal_core_solver_tableau_def.h index 2d6eb95d6..fa7b5e883 100644 --- a/src/util/lp/lp_primal_core_solver_tableau_def.h +++ b/src/math/lp/lp_primal_core_solver_tableau_def.h @@ -18,7 +18,7 @@ Revision History: --*/ // this is a part of lp_primal_core_solver that deals with the tableau -#include "util/lp/lp_primal_core_solver.h" +#include "math/lp/lp_primal_core_solver.h" namespace lp { template void lp_primal_core_solver::one_iteration_tableau() { int entering = choose_entering_column_tableau(); diff --git a/src/util/lp/lp_primal_simplex.cpp b/src/math/lp/lp_primal_simplex.cpp similarity index 96% rename from src/util/lp/lp_primal_simplex.cpp rename to src/math/lp/lp_primal_simplex.cpp index 56d4a6134..634f52900 100644 --- a/src/util/lp/lp_primal_simplex.cpp +++ b/src/math/lp/lp_primal_simplex.cpp @@ -22,7 +22,7 @@ Revision History: #include #include "util/vector.h" #include -#include "util/lp/lp_primal_simplex_def.h" +#include "math/lp/lp_primal_simplex_def.h" template bool lp::lp_primal_simplex::bounds_hold(std::unordered_map, std::equal_to, std::allocator > > const&); template bool lp::lp_primal_simplex::row_constraints_hold(std::unordered_map, std::equal_to, std::allocator > > const&); template double lp::lp_primal_simplex::get_current_cost() const; diff --git a/src/util/lp/lp_primal_simplex.h b/src/math/lp/lp_primal_simplex.h similarity index 94% rename from src/util/lp/lp_primal_simplex.h rename to src/math/lp/lp_primal_simplex.h index d0f5d7d7d..77e12d088 100644 --- a/src/util/lp/lp_primal_simplex.h +++ b/src/math/lp/lp_primal_simplex.h @@ -22,10 +22,10 @@ Revision History: #include #include #include -#include "util/lp/lp_utils.h" -#include "util/lp/column_info.h" -#include "util/lp/lp_primal_core_solver.h" -#include "util/lp/lp_solver.h" +#include "math/lp/lp_utils.h" +#include "math/lp/column_info.h" +#include "math/lp/lp_primal_core_solver.h" +#include "math/lp/lp_solver.h" namespace lp { template class lp_primal_simplex: public lp_solver { diff --git a/src/util/lp/lp_primal_simplex_def.h b/src/math/lp/lp_primal_simplex_def.h similarity index 99% rename from src/util/lp/lp_primal_simplex_def.h rename to src/math/lp/lp_primal_simplex_def.h index ad644838f..e805ecc88 100644 --- a/src/util/lp/lp_primal_simplex_def.h +++ b/src/math/lp/lp_primal_simplex_def.h @@ -19,7 +19,7 @@ Revision History: --*/ #include #include "util/vector.h" -#include "util/lp/lp_primal_simplex.h" +#include "math/lp/lp_primal_simplex.h" namespace lp { template void lp_primal_simplex::fill_costs_and_x_for_first_stage_solver(unsigned original_number_of_columns) { diff --git a/src/util/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp similarity index 91% rename from src/util/lp/lp_settings.cpp rename to src/math/lp/lp_settings.cpp index 147319ed2..fa5570538 100644 --- a/src/util/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -19,7 +19,7 @@ Revision History: --*/ #include #include "util/vector.h" -#include "util/lp/lp_settings_def.h" +#include "math/lp/lp_settings_def.h" template bool lp::vectors_are_equal(vector const&, vector const&); template bool lp::vectors_are_equal(vector const&, vector const&); diff --git a/src/util/lp/lp_settings.h b/src/math/lp/lp_settings.h similarity index 99% rename from src/util/lp/lp_settings.h rename to src/math/lp/lp_settings.h index c36342632..a7c619498 100644 --- a/src/util/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -24,9 +24,9 @@ Revision History: #include #include #include -#include "util/lp/lp_utils.h" +#include "math/lp/lp_utils.h" #include "util/stopwatch.h" -#include "util/lp/lp_types.h" +#include "math/lp/lp_types.h" namespace lp { diff --git a/src/util/lp/lp_settings_def.h b/src/math/lp/lp_settings_def.h similarity index 99% rename from src/util/lp/lp_settings_def.h rename to src/math/lp/lp_settings_def.h index 02963718e..247cb98d3 100644 --- a/src/util/lp/lp_settings_def.h +++ b/src/math/lp/lp_settings_def.h @@ -20,7 +20,7 @@ Revision History: #include #include #include "util/vector.h" -#include "util/lp/lp_settings.h" +#include "math/lp/lp_settings.h" namespace lp { std::string column_type_to_string(column_type t) { switch (t) { diff --git a/src/util/lp/lp_solver.cpp b/src/math/lp/lp_solver.cpp similarity index 98% rename from src/util/lp/lp_solver.cpp rename to src/math/lp/lp_solver.cpp index ea88dd14c..fc9514098 100644 --- a/src/util/lp/lp_solver.cpp +++ b/src/math/lp/lp_solver.cpp @@ -18,7 +18,7 @@ Revision History: --*/ #include -#include "util/lp/lp_solver_def.h" +#include "math/lp/lp_solver_def.h" template void lp::lp_solver::add_constraint(lp::lp_relation, double, unsigned int); template void lp::lp_solver::cleanup(); template void lp::lp_solver::count_slacks_and_artificials(); diff --git a/src/util/lp/lp_solver.h b/src/math/lp/lp_solver.h similarity index 97% rename from src/util/lp/lp_solver.h rename to src/math/lp/lp_solver.h index cd36991f8..9b0b8fb0a 100644 --- a/src/util/lp/lp_solver.h +++ b/src/math/lp/lp_solver.h @@ -23,12 +23,12 @@ Revision History: #include #include #include "util/vector.h" -#include "util/lp/lp_settings.h" -#include "util/lp/column_info.h" -#include "util/lp/static_matrix.h" -#include "util/lp/lp_core_solver_base.h" -#include "util/lp/scaler.h" -#include "util/lp/bound_analyzer_on_row.h" +#include "math/lp/lp_settings.h" +#include "math/lp/column_info.h" +#include "math/lp/static_matrix.h" +#include "math/lp/lp_core_solver_base.h" +#include "math/lp/scaler.h" +#include "math/lp/bound_analyzer_on_row.h" namespace lp { enum lp_relation { Less_or_equal, diff --git a/src/util/lp/lp_solver_def.h b/src/math/lp/lp_solver_def.h similarity index 99% rename from src/util/lp/lp_solver_def.h rename to src/math/lp/lp_solver_def.h index e84535170..a9ae6dfef 100644 --- a/src/util/lp/lp_solver_def.h +++ b/src/math/lp/lp_solver_def.h @@ -20,7 +20,7 @@ Revision History: #include #include #include "util/vector.h" -#include "util/lp/lp_solver.h" +#include "math/lp/lp_solver.h" namespace lp { template column_info * lp_solver::get_or_create_column_info(unsigned column) { auto it = m_map_from_var_index_to_column_info.find(column); diff --git a/src/util/lp/lp_types.h b/src/math/lp/lp_types.h similarity index 100% rename from src/util/lp/lp_types.h rename to src/math/lp/lp_types.h diff --git a/src/util/lp/lp_utils.cpp b/src/math/lp/lp_utils.cpp similarity index 90% rename from src/util/lp/lp_utils.cpp rename to src/math/lp/lp_utils.cpp index 98ab022d1..9ce3b9894 100644 --- a/src/util/lp/lp_utils.cpp +++ b/src/math/lp/lp_utils.cpp @@ -17,7 +17,7 @@ Revision History: --*/ -#include "util/lp/lp_utils.h" +#include "math/lp/lp_utils.h" #ifdef lp_for_z3 namespace lp { double numeric_traits::g_zero = 0.0; diff --git a/src/util/lp/lp_utils.h b/src/math/lp/lp_utils.h similarity index 99% rename from src/util/lp/lp_utils.h rename to src/math/lp/lp_utils.h index 573c93abd..900ab47f8 100644 --- a/src/util/lp/lp_utils.h +++ b/src/math/lp/lp_utils.h @@ -19,7 +19,7 @@ Revision History: --*/ #pragma once #include -#include "util/lp/numeric_pair.h" +#include "math/lp/numeric_pair.h" #include "util/debug.h" #include #include diff --git a/src/util/lp/lu.cpp b/src/math/lp/lu.cpp similarity index 99% rename from src/util/lp/lu.cpp rename to src/math/lp/lu.cpp index ac29dd71a..6c9bcc5f6 100644 --- a/src/util/lp/lu.cpp +++ b/src/math/lp/lu.cpp @@ -22,7 +22,7 @@ Revision History: #include #include "util/vector.h" #include "util/debug.h" -#include "util/lp/lu_def.h" +#include "math/lp/lu_def.h" namespace lp { template double dot_product(vector const&, vector const&); template lu>::lu(static_matrix const&, vector&, lp_settings&); diff --git a/src/util/lp/lu.h b/src/math/lp/lu.h similarity index 98% rename from src/util/lp/lu.h rename to src/math/lp/lu.h index 95c00414e..f5289211f 100644 --- a/src/util/lp/lu.h +++ b/src/math/lp/lu.h @@ -29,15 +29,15 @@ Revision History: #include "util/debug.h" #include #include -#include "util/lp/square_sparse_matrix.h" -#include "util/lp/static_matrix.h" +#include "math/lp/square_sparse_matrix.h" +#include "math/lp/static_matrix.h" #include -#include "util/lp/numeric_pair.h" +#include "math/lp/numeric_pair.h" #include #include -#include "util/lp/row_eta_matrix.h" -#include "util/lp/square_dense_submatrix.h" -#include "util/lp/dense_matrix.h" +#include "math/lp/row_eta_matrix.h" +#include "math/lp/square_dense_submatrix.h" +#include "math/lp/dense_matrix.h" namespace lp { template // print the nr x nc submatrix at the top left corner void print_submatrix(square_sparse_matrix & m, unsigned mr, unsigned nc); diff --git a/src/util/lp/lu_def.h b/src/math/lp/lu_def.h similarity index 99% rename from src/util/lp/lu_def.h rename to src/math/lp/lu_def.h index 00d0466b7..c4bf648c8 100644 --- a/src/util/lp/lu_def.h +++ b/src/math/lp/lu_def.h @@ -23,7 +23,7 @@ Revision History: #include "util/vector.h" #include #include "util/debug.h" -#include "util/lp/lu.h" +#include "math/lp/lu.h" namespace lp { template // print the nr x nc submatrix at the top left corner void print_submatrix(square_sparse_matrix & m, unsigned mr, unsigned nc, std::ostream & out) { diff --git a/src/util/lp/matrix.cpp b/src/math/lp/matrix.cpp similarity index 89% rename from src/util/lp/matrix.cpp rename to src/math/lp/matrix.cpp index 7d3fba08d..5367c74d0 100644 --- a/src/util/lp/matrix.cpp +++ b/src/math/lp/matrix.cpp @@ -17,9 +17,9 @@ Revision History: --*/ -#include "util/lp/lp_settings.h" -#include "util/lp/matrix_def.h" -#include "util/lp/static_matrix.h" +#include "math/lp/lp_settings.h" +#include "math/lp/matrix_def.h" +#include "math/lp/static_matrix.h" #include #ifdef Z3DEBUG template bool lp::matrix::is_equal(lp::matrix const&); diff --git a/src/util/lp/matrix.h b/src/math/lp/matrix.h similarity index 96% rename from src/util/lp/matrix.h rename to src/math/lp/matrix.h index 8b2fc4220..df2b97bc7 100644 --- a/src/util/lp/matrix.h +++ b/src/math/lp/matrix.h @@ -18,10 +18,10 @@ Revision History: --*/ #pragma once -#include "util/lp/numeric_pair.h" +#include "math/lp/numeric_pair.h" #include "util/vector.h" #include -#include "util/lp/lp_settings.h" +#include "math/lp/lp_settings.h" namespace lp { // used for debugging purposes only template diff --git a/src/util/lp/matrix_def.h b/src/math/lp/matrix_def.h similarity index 99% rename from src/util/lp/matrix_def.h rename to src/math/lp/matrix_def.h index b74e59443..8dba9d0b8 100644 --- a/src/util/lp/matrix_def.h +++ b/src/math/lp/matrix_def.h @@ -20,7 +20,7 @@ Revision History: #include #include -#include "util/lp/matrix.h" +#include "math/lp/matrix.h" namespace lp { #ifdef Z3DEBUG template diff --git a/src/util/lp/mon_eq.cpp b/src/math/lp/mon_eq.cpp similarity index 94% rename from src/util/lp/mon_eq.cpp rename to src/math/lp/mon_eq.cpp index 07a1b7577..355a493c0 100644 --- a/src/util/lp/mon_eq.cpp +++ b/src/math/lp/mon_eq.cpp @@ -2,8 +2,8 @@ Copyright (c) 2017 Microsoft Corporation Author: Nikolaj Bjorner */ -#include "util/lp/lar_solver.h" -#include "util/lp/monomial.h" +#include "math/lp/lar_solver.h" +#include "math/lp/monomial.h" namespace nla { template diff --git a/src/util/lp/monomial.h b/src/math/lp/monomial.h similarity index 96% rename from src/util/lp/monomial.h rename to src/math/lp/monomial.h index e6b8c8930..a6ce6b28a 100644 --- a/src/util/lp/monomial.h +++ b/src/math/lp/monomial.h @@ -5,10 +5,10 @@ */ #pragma once -#include "util/lp/lp_settings.h" +#include "math/lp/lp_settings.h" #include "util/vector.h" -#include "util/lp/lar_solver.h" -#include "util/lp/nla_defs.h" +#include "math/lp/lar_solver.h" +#include "math/lp/nla_defs.h" namespace nla { /* * represents definition m_v = v1*v2*...*vn, diff --git a/src/util/lp/mps_reader.h b/src/math/lp/mps_reader.h similarity index 99% rename from src/util/lp/mps_reader.h rename to src/math/lp/mps_reader.h index bc2a8432e..128425353 100644 --- a/src/util/lp/mps_reader.h +++ b/src/math/lp/mps_reader.h @@ -29,11 +29,11 @@ Revision History: #include #include #include -#include "util/lp/lp_primal_simplex.h" -#include "util/lp/lp_dual_simplex.h" -#include "util/lp/lar_solver.h" -#include "util/lp/lp_utils.h" -#include "util/lp/lp_solver.h" +#include "math/lp/lp_primal_simplex.h" +#include "math/lp/lp_dual_simplex.h" +#include "math/lp/lar_solver.h" +#include "math/lp/lp_utils.h" +#include "math/lp/lp_solver.h" namespace lp { inline bool my_white_space(const char & a) { return a == ' ' || a == '\t'; diff --git a/src/util/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp similarity index 99% rename from src/util/lp/nla_basics_lemmas.cpp rename to src/math/lp/nla_basics_lemmas.cpp index 8588d0673..8abd3fcbf 100644 --- a/src/util/lp/nla_basics_lemmas.cpp +++ b/src/math/lp/nla_basics_lemmas.cpp @@ -17,9 +17,9 @@ --*/ -#include "util/lp/nla_basics_lemmas.h" -#include "util/lp/nla_core.h" -#include "util/lp/factorization_factory_imp.h" +#include "math/lp/nla_basics_lemmas.h" +#include "math/lp/nla_core.h" +#include "math/lp/factorization_factory_imp.h" namespace nla { basics::basics(core * c) : common(c) {} diff --git a/src/util/lp/nla_basics_lemmas.h b/src/math/lp/nla_basics_lemmas.h similarity index 97% rename from src/util/lp/nla_basics_lemmas.h rename to src/math/lp/nla_basics_lemmas.h index 67c77b3d2..1f4acf48c 100644 --- a/src/util/lp/nla_basics_lemmas.h +++ b/src/math/lp/nla_basics_lemmas.h @@ -18,9 +18,9 @@ --*/ #pragma once -#include "util/lp/monomial.h" -#include "util/lp/factorization.h" -#include "util/lp/nla_common.h" +#include "math/lp/monomial.h" +#include "math/lp/factorization.h" +#include "math/lp/nla_common.h" namespace nla { diff --git a/src/util/lp/nla_common.cpp b/src/math/lp/nla_common.cpp similarity index 98% rename from src/util/lp/nla_common.cpp rename to src/math/lp/nla_common.cpp index 97e3942c6..700003817 100644 --- a/src/util/lp/nla_common.cpp +++ b/src/math/lp/nla_common.cpp @@ -17,8 +17,8 @@ --*/ -#include "util/lp/nla_common.h" -#include "util/lp/nla_core.h" +#include "math/lp/nla_common.h" +#include "math/lp/nla_core.h" namespace nla { bool common::done() const { return c().done(); } diff --git a/src/util/lp/nla_common.h b/src/math/lp/nla_common.h similarity index 94% rename from src/util/lp/nla_common.h rename to src/math/lp/nla_common.h index 73a6282ef..140746e4b 100644 --- a/src/util/lp/nla_common.h +++ b/src/math/lp/nla_common.h @@ -19,11 +19,11 @@ --*/ #pragma once #include "util/rational.h" -#include "util/lp/nla_defs.h" -#include "util/lp/lar_term.h" -#include "util/lp/monomial.h" -#include "util/lp/emonomials.h" -#include "util/lp/factorization.h" +#include "math/lp/nla_defs.h" +#include "math/lp/lar_term.h" +#include "math/lp/monomial.h" +#include "math/lp/emonomials.h" +#include "math/lp/factorization.h" namespace nla { diff --git a/src/util/lp/nla_core.cpp b/src/math/lp/nla_core.cpp similarity index 99% rename from src/util/lp/nla_core.cpp rename to src/math/lp/nla_core.cpp index 84c025908..16afe48ad 100644 --- a/src/util/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -17,8 +17,8 @@ Revision History: --*/ -#include "util/lp/nla_core.h" -#include "util/lp/factorization_factory_imp.h" +#include "math/lp/nla_core.h" +#include "math/lp/factorization_factory_imp.h" namespace nla { core::core(lp::lar_solver& s) : diff --git a/src/util/lp/nla_core.h b/src/math/lp/nla_core.h similarity index 97% rename from src/util/lp/nla_core.h rename to src/math/lp/nla_core.h index e6062d2fe..466df1213 100644 --- a/src/util/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -18,14 +18,15 @@ --*/ #pragma once -#include "util/lp/factorization.h" -#include "util/lp/lp_types.h" -#include "util/lp/var_eqs.h" -#include "util/lp/nla_tangent_lemmas.h" -#include "util/lp/nla_basics_lemmas.h" -#include "util/lp/nla_order_lemmas.h" -#include "util/lp/nla_monotone_lemmas.h" -#include "util/lp/emonomials.h" +#include "math/lp/factorization.h" +#include "math/lp/lp_types.h" +#include "math/lp/var_eqs.h" +#include "math/lp/nla_tangent_lemmas.h" +#include "math/lp/nla_basics_lemmas.h" +#include "math/lp/nla_order_lemmas.h" +#include "math/lp/nla_monotone_lemmas.h" +#include "math/lp/emonomials.h" +#include "math/lp/nla_settings.h" namespace nla { template diff --git a/src/util/lp/nla_defs.h b/src/math/lp/nla_defs.h similarity index 96% rename from src/util/lp/nla_defs.h rename to src/math/lp/nla_defs.h index 4d3f13069..464a42321 100644 --- a/src/util/lp/nla_defs.h +++ b/src/math/lp/nla_defs.h @@ -18,9 +18,9 @@ --*/ #pragma once -#include "util/lp/lp_types.h" -#include "util/lp/column_info.h" -#include "util/lp/explanation.h" +#include "math/lp/lp_types.h" +#include "math/lp/column_info.h" +#include "math/lp/explanation.h" namespace nla { typedef lp::constraint_index lpci; diff --git a/src/util/lp/nla_monotone_lemmas.cpp b/src/math/lp/nla_monotone_lemmas.cpp similarity index 96% rename from src/util/lp/nla_monotone_lemmas.cpp rename to src/math/lp/nla_monotone_lemmas.cpp index 564a35933..ea9ac0c5f 100644 --- a/src/util/lp/nla_monotone_lemmas.cpp +++ b/src/math/lp/nla_monotone_lemmas.cpp @@ -17,9 +17,9 @@ --*/ -#include "util/lp/nla_basics_lemmas.h" -#include "util/lp/nla_core.h" -// #include "util/lp/factorization_factory_imp.h" +#include "math/lp/nla_basics_lemmas.h" +#include "math/lp/nla_core.h" +// #include "math/lp/factorization_factory_imp.h" namespace nla { monotone::monotone(core * c) : common(c) {} diff --git a/src/util/lp/nla_monotone_lemmas.h b/src/math/lp/nla_monotone_lemmas.h similarity index 100% rename from src/util/lp/nla_monotone_lemmas.h rename to src/math/lp/nla_monotone_lemmas.h diff --git a/src/util/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp similarity index 98% rename from src/util/lp/nla_order_lemmas.cpp rename to src/math/lp/nla_order_lemmas.cpp index 87becb05c..059d5de22 100644 --- a/src/util/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -17,10 +17,10 @@ --*/ -#include "util/lp/nla_order_lemmas.h" -#include "util/lp/nla_core.h" -#include "util/lp/nla_common.h" -#include "util/lp/factorization_factory_imp.h" +#include "math/lp/nla_order_lemmas.h" +#include "math/lp/nla_core.h" +#include "math/lp/nla_common.h" +#include "math/lp/factorization_factory_imp.h" namespace nla { diff --git a/src/util/lp/nla_order_lemmas.h b/src/math/lp/nla_order_lemmas.h similarity index 97% rename from src/util/lp/nla_order_lemmas.h rename to src/math/lp/nla_order_lemmas.h index ea6328aee..1582828f6 100644 --- a/src/util/lp/nla_order_lemmas.h +++ b/src/math/lp/nla_order_lemmas.h @@ -18,8 +18,8 @@ --*/ #pragma once -#include "util/lp/factorization.h" -#include "util/lp/nla_common.h" +#include "math/lp/factorization.h" +#include "math/lp/nla_common.h" namespace nla { class core; diff --git a/src/util/lp/nla_params.pyg b/src/math/lp/nla_params.pyg similarity index 100% rename from src/util/lp/nla_params.pyg rename to src/math/lp/nla_params.pyg diff --git a/src/math/lp/nla_settings.h b/src/math/lp/nla_settings.h new file mode 100644 index 000000000..bc9de779f --- /dev/null +++ b/src/math/lp/nla_settings.h @@ -0,0 +1,34 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + + +Abstract: + + + +Author: + + Lev Nachmanson (levnach) + +Revision History: + + +--*/ + +#pragma once +namespace nla { +class nla_settings { + bool m_run_order; + bool m_run_tangents; +public: + nla_settings() : m_run_order(true), m_run_tangents(true) {} + bool run_order() const { return m_run_order; } + bool& run_order() { return m_run_order; } + + bool run_tangents() const { return m_run_tangents; } + bool& run_tangents() { return m_run_tangents; } +}; +} diff --git a/src/util/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp similarity index 81% rename from src/util/lp/nla_solver.cpp rename to src/math/lp/nla_solver.cpp index 04ae2f4c4..7df1fee72 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -17,13 +17,13 @@ --*/ -#include "util/lp/nla_solver.h" +#include "math/lp/nla_solver.h" #include -#include "util/lp/monomial.h" -#include "util/lp/lp_utils.h" -#include "util/lp/var_eqs.h" -#include "util/lp/factorization.h" -#include "util/lp/nla_solver.h" +#include "math/lp/monomial.h" +#include "math/lp/lp_utils.h" +#include "math/lp/var_eqs.h" +#include "math/lp/factorization.h" +#include "math/lp/nla_solver.h" namespace nla { // returns the monomial index diff --git a/src/util/lp/nla_solver.h b/src/math/lp/nla_solver.h similarity index 85% rename from src/util/lp/nla_solver.h rename to src/math/lp/nla_solver.h index 80d33beea..44f57908c 100644 --- a/src/util/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -19,13 +19,13 @@ Revision History: --*/ #pragma once #include "util/vector.h" -#include "util/lp/lp_settings.h" +#include "math/lp/lp_settings.h" #include "util/rlimit.h" #include "util/params.h" #include "nlsat/nlsat_solver.h" -#include "util/lp/lar_solver.h" -#include "util/lp/monomial.h" -#include "util/lp/nla_core.h" +#include "math/lp/lar_solver.h" +#include "math/lp/monomial.h" +#include "math/lp/nla_core.h" namespace nla { // nonlinear integer incremental linear solver diff --git a/src/util/lp/nla_tangent_lemmas.cpp b/src/math/lp/nla_tangent_lemmas.cpp similarity index 98% rename from src/util/lp/nla_tangent_lemmas.cpp rename to src/math/lp/nla_tangent_lemmas.cpp index 8ae9a606c..6d32da442 100644 --- a/src/util/lp/nla_tangent_lemmas.cpp +++ b/src/math/lp/nla_tangent_lemmas.cpp @@ -17,8 +17,8 @@ --*/ -#include "util/lp/nla_tangent_lemmas.h" -#include "util/lp/nla_core.h" +#include "math/lp/nla_tangent_lemmas.h" +#include "math/lp/nla_core.h" namespace nla { template rational tangents::val(T const& t) const { return m_core->val(t); } diff --git a/src/util/lp/nla_tangent_lemmas.h b/src/math/lp/nla_tangent_lemmas.h similarity index 97% rename from src/util/lp/nla_tangent_lemmas.h rename to src/math/lp/nla_tangent_lemmas.h index 059cbea41..9edc67211 100644 --- a/src/util/lp/nla_tangent_lemmas.h +++ b/src/math/lp/nla_tangent_lemmas.h @@ -19,8 +19,8 @@ --*/ #pragma once #include "util/rational.h" -#include "util/lp/factorization.h" -#include "util/lp/nla_common.h" +#include "math/lp/factorization.h" +#include "math/lp/nla_common.h" namespace nla { class core; diff --git a/src/util/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp similarity index 98% rename from src/util/lp/nra_solver.cpp rename to src/math/lp/nra_solver.cpp index d95680671..2c59077e7 100644 --- a/src/util/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -3,13 +3,13 @@ Author: Nikolaj Bjorner */ -#include "util/lp/lar_solver.h" -#include "util/lp/nra_solver.h" +#include "math/lp/lar_solver.h" +#include "math/lp/nra_solver.h" #include "nlsat/nlsat_solver.h" #include "math/polynomial/polynomial.h" #include "math/polynomial/algebraic_numbers.h" #include "util/map.h" -#include "util/lp/monomial.h" +#include "math/lp/monomial.h" namespace nra { diff --git a/src/util/lp/nra_solver.h b/src/math/lp/nra_solver.h similarity index 97% rename from src/util/lp/nra_solver.h rename to src/math/lp/nra_solver.h index 8431d2c34..a7b586aee 100644 --- a/src/util/lp/nra_solver.h +++ b/src/math/lp/nra_solver.h @@ -5,7 +5,7 @@ #pragma once #include "util/vector.h" -#include "util/lp/lp_settings.h" +#include "math/lp/lp_settings.h" #include "util/rlimit.h" #include "util/params.h" #include "nlsat/nlsat_solver.h" diff --git a/src/util/lp/numeric_pair.h b/src/math/lp/numeric_pair.h similarity index 99% rename from src/util/lp/numeric_pair.h rename to src/math/lp/numeric_pair.h index b4ddae7df..f0e8c9764 100644 --- a/src/util/lp/numeric_pair.h +++ b/src/math/lp/numeric_pair.h @@ -23,9 +23,9 @@ Revision History: #include #include #ifdef lp_for_z3 -#include "../rational.h" -#include "../sstream.h" -#include "../z3_exception.h" +#include "util/rational.h" +#include "util/sstream.h" +#include "util/z3_exception.h" #else // include "util/numerics/mpq.h" // include "util/numerics/numeric_traits.h" diff --git a/src/util/lp/permutation_matrix.cpp b/src/math/lp/permutation_matrix.cpp similarity index 98% rename from src/util/lp/permutation_matrix.cpp rename to src/math/lp/permutation_matrix.cpp index 8b57cfe00..28319c2ee 100644 --- a/src/util/lp/permutation_matrix.cpp +++ b/src/math/lp/permutation_matrix.cpp @@ -19,8 +19,8 @@ Revision History: --*/ #include #include "util/vector.h" -#include "util/lp/permutation_matrix_def.h" -#include "util/lp/numeric_pair.h" +#include "math/lp/permutation_matrix_def.h" +#include "math/lp/numeric_pair.h" template void lp::permutation_matrix::apply_from_right(vector&); template void lp::permutation_matrix::init(unsigned int); template void lp::permutation_matrix::init(unsigned int); diff --git a/src/util/lp/permutation_matrix.h b/src/math/lp/permutation_matrix.h similarity index 96% rename from src/util/lp/permutation_matrix.h rename to src/math/lp/permutation_matrix.h index d1422ef86..8ec78c14a 100644 --- a/src/util/lp/permutation_matrix.h +++ b/src/math/lp/permutation_matrix.h @@ -22,11 +22,11 @@ Revision History: #include #include "util/debug.h" #include -#include "util/lp/sparse_vector.h" -#include "util/lp/indexed_vector.h" -#include "util/lp/lp_settings.h" -#include "util/lp/matrix.h" -#include "util/lp/tail_matrix.h" +#include "math/lp/sparse_vector.h" +#include "math/lp/indexed_vector.h" +#include "math/lp/lp_settings.h" +#include "math/lp/matrix.h" +#include "math/lp/tail_matrix.h" namespace lp { #ifdef Z3DEBUG inline bool is_even(int k) { return (k/2)*2 == k; } diff --git a/src/util/lp/permutation_matrix_def.h b/src/math/lp/permutation_matrix_def.h similarity index 99% rename from src/util/lp/permutation_matrix_def.h rename to src/math/lp/permutation_matrix_def.h index 76af12ed8..c6ad20a39 100644 --- a/src/util/lp/permutation_matrix_def.h +++ b/src/math/lp/permutation_matrix_def.h @@ -18,7 +18,7 @@ Revision History: --*/ #include "util/vector.h" -#include "util/lp/permutation_matrix.h" +#include "math/lp/permutation_matrix.h" namespace lp { template permutation_matrix::permutation_matrix(unsigned length): m_permutation(length), m_rev(length), m_T_buffer(length), m_X_buffer(length) { for (unsigned i = 0; i < length; i++) { // do not change the direction of the loop because of the vectorization bug in clang3.3 diff --git a/src/util/lp/polynomial.h b/src/math/lp/polynomial.h similarity index 100% rename from src/util/lp/polynomial.h rename to src/math/lp/polynomial.h diff --git a/src/util/lp/random_updater.cpp b/src/math/lp/random_updater.cpp similarity index 80% rename from src/util/lp/random_updater.cpp rename to src/math/lp/random_updater.cpp index 564885ea0..a88df76e5 100644 --- a/src/util/lp/random_updater.cpp +++ b/src/math/lp/random_updater.cpp @@ -17,5 +17,5 @@ Revision History: --*/ -#include "util/lp/random_updater_def.h" +#include "math/lp/random_updater_def.h" diff --git a/src/util/lp/random_updater.h b/src/math/lp/random_updater.h similarity index 97% rename from src/util/lp/random_updater.h rename to src/math/lp/random_updater.h index e5067f2e5..fbf4ced1d 100644 --- a/src/util/lp/random_updater.h +++ b/src/math/lp/random_updater.h @@ -24,7 +24,7 @@ Revision History: #include #include #include -#include "util/lp/lp_settings.h" +#include "math/lp/lp_settings.h" // see http://research.microsoft.com/projects/z3/smt07.pdf // The class searches for a feasible solution with as many different values of variables as it can find namespace lp { diff --git a/src/util/lp/random_updater_def.h b/src/math/lp/random_updater_def.h similarity index 95% rename from src/util/lp/random_updater_def.h rename to src/math/lp/random_updater_def.h index c972cc175..fd8c2305a 100644 --- a/src/util/lp/random_updater_def.h +++ b/src/math/lp/random_updater_def.h @@ -17,9 +17,9 @@ Revision History: --*/ -#include "util/lp/random_updater.h" -#include "util/lp/static_matrix.h" -#include "util/lp/lar_solver.h" +#include "math/lp/random_updater.h" +#include "math/lp/static_matrix.h" +#include "math/lp/lar_solver.h" #include "util/vector.h" namespace lp { diff --git a/src/util/lp/row_eta_matrix.cpp b/src/math/lp/row_eta_matrix.cpp similarity index 97% rename from src/util/lp/row_eta_matrix.cpp rename to src/math/lp/row_eta_matrix.cpp index c74ce9186..6fafb83ed 100644 --- a/src/util/lp/row_eta_matrix.cpp +++ b/src/math/lp/row_eta_matrix.cpp @@ -19,8 +19,8 @@ Revision History: --*/ #include #include "util/vector.h" -#include "util/lp/row_eta_matrix_def.h" -#include "util/lp/lu.h" +#include "math/lp/row_eta_matrix_def.h" +#include "math/lp/lu.h" namespace lp { template void row_eta_matrix::conjugate_by_permutation(permutation_matrix&); template void row_eta_matrix >::conjugate_by_permutation(permutation_matrix >&); diff --git a/src/util/lp/row_eta_matrix.h b/src/math/lp/row_eta_matrix.h similarity index 95% rename from src/util/lp/row_eta_matrix.h rename to src/math/lp/row_eta_matrix.h index 497e7935c..50c500f00 100644 --- a/src/util/lp/row_eta_matrix.h +++ b/src/math/lp/row_eta_matrix.h @@ -22,9 +22,9 @@ Revision History: #include "util/vector.h" #include "util/debug.h" #include -#include "util/lp/sparse_vector.h" -#include "util/lp/indexed_vector.h" -#include "util/lp/permutation_matrix.h" +#include "math/lp/sparse_vector.h" +#include "math/lp/indexed_vector.h" +#include "math/lp/permutation_matrix.h" namespace lp { // This is the sum of a unit matrix and a lower triangular matrix // with non-zero elements only in one row diff --git a/src/util/lp/row_eta_matrix_def.h b/src/math/lp/row_eta_matrix_def.h similarity index 99% rename from src/util/lp/row_eta_matrix_def.h rename to src/math/lp/row_eta_matrix_def.h index 46b187a24..817d39481 100644 --- a/src/util/lp/row_eta_matrix_def.h +++ b/src/math/lp/row_eta_matrix_def.h @@ -18,7 +18,7 @@ Revision History: --*/ #include "util/vector.h" -#include "util/lp/row_eta_matrix.h" +#include "math/lp/row_eta_matrix.h" namespace lp { template void row_eta_matrix::apply_from_left(vector & w, lp_settings &) { diff --git a/src/util/lp/scaler.cpp b/src/math/lp/scaler.cpp similarity index 89% rename from src/util/lp/scaler.cpp rename to src/math/lp/scaler.cpp index dcb4cd308..46330e2a1 100644 --- a/src/util/lp/scaler.cpp +++ b/src/math/lp/scaler.cpp @@ -17,6 +17,6 @@ Revision History: --*/ -#include "util/lp/scaler_def.h" +#include "math/lp/scaler_def.h" template bool lp::scaler::scale(); template bool lp::scaler::scale(); diff --git a/src/util/lp/scaler.h b/src/math/lp/scaler.h similarity index 96% rename from src/util/lp/scaler.h rename to src/math/lp/scaler.h index f98be83bd..dd21b5c28 100644 --- a/src/util/lp/scaler.h +++ b/src/math/lp/scaler.h @@ -24,8 +24,8 @@ Revision History: #include #include /* printf, fopen */ #include /* exit, EXIT_FAILURE */ -#include "util/lp/lp_utils.h" -#include "util/lp/static_matrix.h" +#include "math/lp/lp_utils.h" +#include "math/lp/static_matrix.h" namespace lp { // for scaling an LP template diff --git a/src/util/lp/scaler_def.h b/src/math/lp/scaler_def.h similarity index 99% rename from src/util/lp/scaler_def.h rename to src/math/lp/scaler_def.h index 489f42c56..c05b25a16 100644 --- a/src/util/lp/scaler_def.h +++ b/src/math/lp/scaler_def.h @@ -18,8 +18,8 @@ Revision History: --*/ #include -#include "util/lp/scaler.h" -#include "util/lp/numeric_pair.h" +#include "math/lp/scaler.h" +#include "math/lp/numeric_pair.h" namespace lp { // for scaling an LP template T scaler::right_side_balance() { diff --git a/src/util/lp/signature_bound_evidence.h b/src/math/lp/signature_bound_evidence.h similarity index 89% rename from src/util/lp/signature_bound_evidence.h rename to src/math/lp/signature_bound_evidence.h index 7e09f720f..53136a6ef 100644 --- a/src/util/lp/signature_bound_evidence.h +++ b/src/math/lp/signature_bound_evidence.h @@ -18,8 +18,8 @@ Revision History: --*/ #pragma once -#include "util/lp/lp_settings.h" -#include "util/lp/lar_constraints.h" +#include "math/lp/lp_settings.h" +#include "math/lp/lar_constraints.h" namespace lp { struct bound_signature { unsigned m_i; diff --git a/src/util/lp/sparse_vector.h b/src/math/lp/sparse_vector.h similarity index 93% rename from src/util/lp/sparse_vector.h rename to src/math/lp/sparse_vector.h index 67ea97a9d..1c27a8d96 100644 --- a/src/util/lp/sparse_vector.h +++ b/src/math/lp/sparse_vector.h @@ -22,8 +22,8 @@ Revision History: #include "util/vector.h" #include #include "util/debug.h" -#include "util/lp/lp_utils.h" -#include "util/lp/lp_settings.h" +#include "math/lp/lp_utils.h" +#include "math/lp/lp_settings.h" namespace lp { template diff --git a/src/util/lp/square_dense_submatrix.cpp b/src/math/lp/square_dense_submatrix.cpp similarity index 98% rename from src/util/lp/square_dense_submatrix.cpp rename to src/math/lp/square_dense_submatrix.cpp index 802f3d74a..4d9fcec13 100644 --- a/src/util/lp/square_dense_submatrix.cpp +++ b/src/math/lp/square_dense_submatrix.cpp @@ -19,7 +19,7 @@ Revision History: --*/ #include #include "util/vector.h" -#include "util/lp/square_dense_submatrix_def.h" +#include "math/lp/square_dense_submatrix_def.h" template void lp::square_dense_submatrix::init(lp::square_sparse_matrix*, unsigned int); template lp::square_dense_submatrix::square_dense_submatrix(lp::square_sparse_matrix*, unsigned int); template void lp::square_dense_submatrix::update_parent_matrix(lp::lp_settings&); diff --git a/src/util/lp/square_dense_submatrix.h b/src/math/lp/square_dense_submatrix.h similarity index 95% rename from src/util/lp/square_dense_submatrix.h rename to src/math/lp/square_dense_submatrix.h index 0c6bbdec3..308f9eadc 100644 --- a/src/util/lp/square_dense_submatrix.h +++ b/src/math/lp/square_dense_submatrix.h @@ -20,21 +20,21 @@ Revision History: #pragma once #include "util/vector.h" -#include "util/lp/permutation_matrix.h" +#include "math/lp/permutation_matrix.h" #include -#include "util/lp/static_matrix.h" +#include "math/lp/static_matrix.h" #include #include #include #include #include -#include "util/lp/indexed_value.h" -#include "util/lp/indexed_vector.h" +#include "math/lp/indexed_value.h" +#include "math/lp/indexed_vector.h" #include -#include "util/lp/lp_settings.h" -#include "util/lp/eta_matrix.h" -#include "util/lp/binary_heap_upair_queue.h" -#include "util/lp/square_sparse_matrix.h" +#include "math/lp/lp_settings.h" +#include "math/lp/eta_matrix.h" +#include "math/lp/binary_heap_upair_queue.h" +#include "math/lp/square_sparse_matrix.h" namespace lp { template class square_dense_submatrix : public tail_matrix { diff --git a/src/util/lp/square_dense_submatrix_def.h b/src/math/lp/square_dense_submatrix_def.h similarity index 99% rename from src/util/lp/square_dense_submatrix_def.h rename to src/math/lp/square_dense_submatrix_def.h index 54f6e5327..8b565f92e 100644 --- a/src/util/lp/square_dense_submatrix_def.h +++ b/src/math/lp/square_dense_submatrix_def.h @@ -18,7 +18,7 @@ Revision History: --*/ #include "util/vector.h" -#include "util/lp/square_dense_submatrix.h" +#include "math/lp/square_dense_submatrix.h" namespace lp { template square_dense_submatrix::square_dense_submatrix (square_sparse_matrix *parent_matrix, unsigned index_start) : diff --git a/src/util/lp/square_sparse_matrix.cpp b/src/math/lp/square_sparse_matrix.cpp similarity index 98% rename from src/util/lp/square_sparse_matrix.cpp rename to src/math/lp/square_sparse_matrix.cpp index 6c65cd863..35d38e529 100644 --- a/src/util/lp/square_sparse_matrix.cpp +++ b/src/math/lp/square_sparse_matrix.cpp @@ -19,10 +19,10 @@ Revision History: --*/ #include #include "util/vector.h" -#include "util/lp/lp_settings.h" -#include "util/lp/lu.h" -#include "util/lp/square_sparse_matrix_def.h" -#include "util/lp/dense_matrix.h" +#include "math/lp/lp_settings.h" +#include "math/lp/lu.h" +#include "math/lp/square_sparse_matrix_def.h" +#include "math/lp/dense_matrix.h" namespace lp { template double square_sparse_matrix::dot_product_with_row(unsigned int, vector const&) const; template void square_sparse_matrix::add_new_element(unsigned int, unsigned int, const double&); diff --git a/src/util/lp/square_sparse_matrix.h b/src/math/lp/square_sparse_matrix.h similarity index 97% rename from src/util/lp/square_sparse_matrix.h rename to src/math/lp/square_sparse_matrix.h index cb5193b2d..c8361895f 100644 --- a/src/util/lp/square_sparse_matrix.h +++ b/src/math/lp/square_sparse_matrix.h @@ -20,22 +20,22 @@ Revision History: #pragma once #include "util/vector.h" -#include "util/lp/permutation_matrix.h" +#include "math/lp/permutation_matrix.h" #include -#include "util/lp/static_matrix.h" +#include "math/lp/static_matrix.h" #include #include #include #include #include -#include "util/lp/indexed_value.h" -#include "util/lp/indexed_vector.h" +#include "math/lp/indexed_value.h" +#include "math/lp/indexed_vector.h" #include -#include "util/lp/lp_settings.h" -#include "util/lp/eta_matrix.h" -#include "util/lp/binary_heap_upair_queue.h" -#include "util/lp/numeric_pair.h" -#include "util/lp/int_set.h" +#include "math/lp/lp_settings.h" +#include "math/lp/eta_matrix.h" +#include "math/lp/binary_heap_upair_queue.h" +#include "math/lp/numeric_pair.h" +#include "math/lp/int_set.h" namespace lp { // it is a square matrix template diff --git a/src/util/lp/square_sparse_matrix_def.h b/src/math/lp/square_sparse_matrix_def.h similarity index 99% rename from src/util/lp/square_sparse_matrix_def.h rename to src/math/lp/square_sparse_matrix_def.h index 2fc101666..3419ad5b7 100644 --- a/src/util/lp/square_sparse_matrix_def.h +++ b/src/math/lp/square_sparse_matrix_def.h @@ -19,7 +19,7 @@ Revision History: --*/ #include "util/vector.h" -#include "util/lp/square_sparse_matrix.h" +#include "math/lp/square_sparse_matrix.h" #include #include namespace lp { diff --git a/src/util/lp/stacked_value.h b/src/math/lp/stacked_value.h similarity index 100% rename from src/util/lp/stacked_value.h rename to src/math/lp/stacked_value.h diff --git a/src/util/lp/stacked_vector.h b/src/math/lp/stacked_vector.h similarity index 100% rename from src/util/lp/stacked_vector.h rename to src/math/lp/stacked_vector.h diff --git a/src/util/lp/static_matrix.cpp b/src/math/lp/static_matrix.cpp similarity index 94% rename from src/util/lp/static_matrix.cpp rename to src/math/lp/static_matrix.cpp index 9d12087bb..571e9b1d0 100644 --- a/src/util/lp/static_matrix.cpp +++ b/src/math/lp/static_matrix.cpp @@ -21,13 +21,13 @@ Revision History: #include "util/vector.h" #include #include -#include "util/lp/static_matrix_def.h" -#include "util/lp/lp_core_solver_base.h" -#include "util/lp/lp_dual_core_solver.h" -#include "util/lp/lp_dual_simplex.h" -#include "util/lp/lp_primal_core_solver.h" -#include "util/lp/scaler.h" -#include "util/lp/lar_solver.h" +#include "math/lp/static_matrix_def.h" +#include "math/lp/lp_core_solver_base.h" +#include "math/lp/lp_dual_core_solver.h" +#include "math/lp/lp_dual_simplex.h" +#include "math/lp/lp_primal_core_solver.h" +#include "math/lp/scaler.h" +#include "math/lp/lar_solver.h" namespace lp { template void static_matrix::add_columns_at_the_end(unsigned int); template void static_matrix::clear(); diff --git a/src/util/lp/static_matrix.h b/src/math/lp/static_matrix.h similarity index 99% rename from src/util/lp/static_matrix.h rename to src/math/lp/static_matrix.h index 1bf0c4afb..295c7f01e 100644 --- a/src/util/lp/static_matrix.h +++ b/src/math/lp/static_matrix.h @@ -23,9 +23,9 @@ Revision History: #include #include #include -#include "util/lp/sparse_vector.h" -#include "util/lp/indexed_vector.h" -#include "util/lp/permutation_matrix.h" +#include "math/lp/sparse_vector.h" +#include "math/lp/indexed_vector.h" +#include "math/lp/permutation_matrix.h" #include namespace lp { diff --git a/src/util/lp/static_matrix_def.h b/src/math/lp/static_matrix_def.h similarity index 99% rename from src/util/lp/static_matrix_def.h rename to src/math/lp/static_matrix_def.h index 7949573de..405ca18e8 100644 --- a/src/util/lp/static_matrix_def.h +++ b/src/math/lp/static_matrix_def.h @@ -20,7 +20,7 @@ Revision History: #include "util/vector.h" #include #include -#include "util/lp/static_matrix.h" +#include "math/lp/static_matrix.h" namespace lp { // each assignment for this matrix should be issued only once!!! template diff --git a/src/util/lp/tail_matrix.h b/src/math/lp/tail_matrix.h similarity index 91% rename from src/util/lp/tail_matrix.h rename to src/math/lp/tail_matrix.h index 2a851bc16..2047e8c7e 100644 --- a/src/util/lp/tail_matrix.h +++ b/src/math/lp/tail_matrix.h @@ -20,9 +20,9 @@ Revision History: #pragma once #include "util/vector.h" -#include "util/lp/indexed_vector.h" -#include "util/lp/matrix.h" -#include "util/lp/lp_settings.h" +#include "math/lp/indexed_vector.h" +#include "math/lp/matrix.h" +#include "math/lp/lp_settings.h" // These matrices appear at the end of the list namespace lp { diff --git a/src/util/lp/test_bound_analyzer.h b/src/math/lp/test_bound_analyzer.h similarity index 99% rename from src/util/lp/test_bound_analyzer.h rename to src/math/lp/test_bound_analyzer.h index 7cee0cf56..1ca99d637 100644 --- a/src/util/lp/test_bound_analyzer.h +++ b/src/math/lp/test_bound_analyzer.h @@ -20,8 +20,8 @@ Revision History: #if 0 #pragma once #include "util/vector.h" -#include "util/lp/implied_bound.h" -#include "util/lp/lp_settings.h" +#include "math/lp/implied_bound.h" +#include "math/lp/lp_settings.h" #include // this class is for testing only diff --git a/src/util/lp/ul_pair.h b/src/math/lp/ul_pair.h similarity index 97% rename from src/util/lp/ul_pair.h rename to src/math/lp/ul_pair.h index 78e361c51..e40fe98f8 100644 --- a/src/util/lp/ul_pair.h +++ b/src/math/lp/ul_pair.h @@ -23,8 +23,8 @@ Revision History: #include #include #include -#include "util/lp/column_info.h" -#include "util/lp/lp_types.h" +#include "math/lp/column_info.h" +#include "math/lp/lp_types.h" namespace lp { diff --git a/src/util/lp/var_eqs.h b/src/math/lp/var_eqs.h similarity index 99% rename from src/util/lp/var_eqs.h rename to src/math/lp/var_eqs.h index 468f51371..880f085ca 100644 --- a/src/util/lp/var_eqs.h +++ b/src/math/lp/var_eqs.h @@ -20,10 +20,10 @@ #pragma once #include "util/union_find.h" -#include "util/lp/nla_defs.h" +#include "math/lp/nla_defs.h" #include "util/rational.h" -#include "util/lp/explanation.h" -#include "util/lp/incremental_vector.h" +#include "math/lp/explanation.h" +#include "math/lp/incremental_vector.h" namespace nla { diff --git a/src/util/lp/var_register.h b/src/math/lp/var_register.h similarity index 100% rename from src/util/lp/var_register.h rename to src/math/lp/var_register.h diff --git a/src/shell/lp_frontend.cpp b/src/shell/lp_frontend.cpp index 28cfaed33..8704147c3 100644 --- a/src/shell/lp_frontend.cpp +++ b/src/shell/lp_frontend.cpp @@ -7,9 +7,9 @@ Author: --*/ -#include "util/lp/lp_params.hpp" -#include "util/lp/lp_settings.h" -#include "util/lp/mps_reader.h" +#include "math/lp/lp_params.hpp" +#include "math/lp/lp_settings.h" +#include "math/lp/mps_reader.h" #include "util/timeout.h" #include "util/cancel_eh.h" #include "util/scoped_timer.h" diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 0796471b1..5e558ca37 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -16,7 +16,7 @@ Author: Notes: --*/ -#include "util/lp/lp_params.hpp" +#include "math/lp/lp_params.hpp" #include "ast/rewriter/rewriter_types.h" #include "ast/ast_util.h" #include "smt/smt_kernel.h" diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 94e5a7b6e..e31f6d02e 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -19,14 +19,15 @@ --*/ #include "util/stopwatch.h" -#include "util/lp/lp_solver.h" -#include "util/lp/lp_primal_simplex.h" -#include "util/lp/lp_dual_simplex.h" -#include "util/lp/indexed_value.h" -#include "util/lp/lar_solver.h" +#include "math/lp/lp_solver.h" +#include "math/lp/lp_primal_simplex.h" +#include "math/lp/lp_dual_simplex.h" +#include "math/lp/indexed_value.h" +#include "math/lp/lar_solver.h" #include "util/nat_set.h" #include "util/optional.h" -#include "util/lp/lp_params.hpp" +#include "math/lp/lp_params.hpp" +#include "math/lp/nla_params.hpp" #include "util/inf_rational.h" #include "util/cancel_eh.h" #include "util/scoped_timer.h" @@ -39,13 +40,15 @@ #include "smt/theory_lra.h" #include "smt/smt_model_generator.h" #include "smt/arith_eq_adapter.h" +#include "util/nat_set.h" +#include "math/lp/nra_solver.h" #include "tactic/generic_model_converter.h" #include "math/polynomial/algebraic_numbers.h" #include "math/polynomial/polynomial.h" #include "ast/ast_pp.h" #include "util/cancel_eh.h" #include "util/scoped_timer.h" -#include "util/lp/nla_solver.h" +#include "math/lp/nla_solver.h" typedef lp::var_index lpvar; diff --git a/src/test/lp/gomory_test.h b/src/test/lp/gomory_test.h index 304ef52f1..b26cfab0b 100644 --- a/src/test/lp/gomory_test.h +++ b/src/test/lp/gomory_test.h @@ -1,5 +1,5 @@ namespace lp { -#include "util/lp/lp_utils.h" +#include "math/lp/lp_utils.h" struct gomory_test { gomory_test( std::function name_function_p, diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index 01a9f16c6..8fd7d3679 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -32,29 +32,29 @@ #include #include #include -#include "util/lp/lp_utils.h" -#include "util/lp/lp_primal_simplex.h" -#include "util/lp/mps_reader.h" +#include "math/lp/lp_utils.h" +#include "math/lp/lp_primal_simplex.h" +#include "math/lp/mps_reader.h" #include "test/lp/smt_reader.h" -#include "util/lp/binary_heap_priority_queue.h" +#include "math/lp/binary_heap_priority_queue.h" #include "test/lp/argument_parser.h" #include "test/lp/test_file_reader.h" -#include "util/lp/indexed_value.h" -#include "util/lp/lar_solver.h" -#include "util/lp/numeric_pair.h" -#include "util/lp/binary_heap_upair_queue.h" -#include "util/lp/stacked_value.h" -#include "util/lp/int_set.h" +#include "math/lp/indexed_value.h" +#include "math/lp/lar_solver.h" +#include "math/lp/numeric_pair.h" +#include "math/lp/binary_heap_upair_queue.h" +#include "math/lp/stacked_value.h" +#include "math/lp/int_set.h" #include "util/stopwatch.h" #include #include "test/lp/gomory_test.h" -#include "util/lp/matrix.h" -#include "util/lp/hnf.h" -#include "util/lp/square_sparse_matrix_def.h" -#include "util/lp/lu_def.h" -#include "util/lp/general_matrix.h" -#include "util/lp/bound_propagator.h" -#include "util/lp/nla_solver.h" +#include "math/lp/matrix.h" +#include "math/lp/hnf.h" +#include "math/lp/square_sparse_matrix_def.h" +#include "math/lp/lu_def.h" +#include "math/lp/general_matrix.h" +#include "math/lp/bound_propagator.h" +#include "math/lp/nla_solver.h" namespace nla { void test_order_lemma(); void test_monotone_lemma(); @@ -1507,127 +1507,127 @@ void fill_file_names(vector &file_names, std::set & m return; } std::string home_dir_str(home_dir); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/l0redund.mps"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/l1.mps"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/l2.mps"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/l3.mps"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/l4.mps"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/l4fix.mps"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/plan.mps"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/samp2.mps"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/murtagh.mps"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/l0.mps"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/AFIRO.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SC50B.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SC50A.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/KB2.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SC105.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/STOCFOR1.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/ADLITTLE.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/BLEND.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SCAGR7.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SC205.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SHARE2B.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/RECIPELP.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/LOTFI.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/VTP-BASE.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SHARE1B.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/BOEING2.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/BORE3D.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SCORPION.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/CAPRI.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/BRANDY.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SCAGR25.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SCTAP1.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/ISRAEL.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SCFXM1.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/BANDM.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/E226.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/AGG.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/GROW7.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/ETAMACRO.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/FINNIS.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SCSD1.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/STANDATA.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/STANDGUB.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/BEACONFD.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/STAIR.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/STANDMPS.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/GFRD-PNC.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SCRS8.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/BOEING1.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/MODSZK1.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/DEGEN2.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/FORPLAN.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/AGG2.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/AGG3.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SCFXM2.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SHELL.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/PILOT4.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SCSD6.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SHIP04S.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SEBA.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/GROW15.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/FFFFF800.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/BNL1.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/PEROLD.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/QAP8.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SCFXM3.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SHIP04L.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/GANGES.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SCTAP2.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/GROW22.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SHIP08S.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/PILOT-WE.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/MAROS.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/STOCFOR2.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/25FV47.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SHIP12S.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SCSD8.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/FIT1P.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SCTAP3.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SIERRA.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/PILOTNOV.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/CZPROB.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/FIT1D.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/PILOT-JA.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SHIP08L.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/BNL2.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/NESM.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/CYCLE.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/acc-tight5.mps"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/SHIP12L.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/DEGEN3.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/GREENBEA.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/GREENBEB.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/80BAU3B.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/TRUSS.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/D2Q06C.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/WOODW.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/QAP12.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/D6CUBE.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/PILOT.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/DFL001.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/WOOD1P.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/FIT2P.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/PILOT87.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/STOCFOR3.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/QAP15.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/FIT2D.SIF"); - file_names.push_back(home_dir_str + "/projects/lp/src/tests/util/lp/test_files/netlib/MAROS-R7.SIF"); - minimums.insert("/projects/lp/src/tests/util/lp/test_files/netlib/FIT2P.SIF"); - minimums.insert("/projects/lp/src/tests/util/lp/test_files/netlib/DFL001.SIF"); - minimums.insert("/projects/lp/src/tests/util/lp/test_files/netlib/D2Q06C.SIF"); - minimums.insert("/projects/lp/src/tests/util/lp/test_files/netlib/80BAU3B.SIF"); - minimums.insert("/projects/lp/src/tests/util/lp/test_files/netlib/GREENBEB.SIF"); - minimums.insert("/projects/lp/src/tests/util/lp/test_files/netlib/GREENBEA.SIF"); - minimums.insert("/projects/lp/src/tests/util/lp/test_files/netlib/BNL2.SIF"); - minimums.insert("/projects/lp/src/tests/util/lp/test_files/netlib/SHIP08L.SIF"); - minimums.insert("/projects/lp/src/tests/util/lp/test_files/netlib/FIT1D.SIF"); - minimums.insert("/projects/lp/src/tests/util/lp/test_files/netlib/SCTAP3.SIF"); - minimums.insert("/projects/lp/src/tests/util/lp/test_files/netlib/SCSD8.SIF"); - minimums.insert("/projects/lp/src/tests/util/lp/test_files/netlib/SCSD6.SIF"); - minimums.insert("/projects/lp/src/tests/util/lp/test_files/netlib/MAROS-R7.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/l0redund.mps"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/l1.mps"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/l2.mps"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/l3.mps"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/l4.mps"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/l4fix.mps"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/plan.mps"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/samp2.mps"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/murtagh.mps"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/l0.mps"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/AFIRO.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SC50B.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SC50A.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/KB2.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SC105.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/STOCFOR1.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/ADLITTLE.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/BLEND.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SCAGR7.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SC205.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SHARE2B.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/RECIPELP.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/LOTFI.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/VTP-BASE.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SHARE1B.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/BOEING2.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/BORE3D.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SCORPION.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/CAPRI.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/BRANDY.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SCAGR25.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SCTAP1.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/ISRAEL.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SCFXM1.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/BANDM.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/E226.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/AGG.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/GROW7.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/ETAMACRO.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/FINNIS.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SCSD1.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/STANDATA.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/STANDGUB.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/BEACONFD.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/STAIR.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/STANDMPS.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/GFRD-PNC.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SCRS8.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/BOEING1.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/MODSZK1.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/DEGEN2.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/FORPLAN.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/AGG2.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/AGG3.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SCFXM2.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SHELL.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/PILOT4.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SCSD6.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SHIP04S.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SEBA.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/GROW15.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/FFFFF800.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/BNL1.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/PEROLD.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/QAP8.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SCFXM3.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SHIP04L.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/GANGES.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SCTAP2.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/GROW22.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SHIP08S.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/PILOT-WE.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/MAROS.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/STOCFOR2.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/25FV47.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SHIP12S.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SCSD8.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/FIT1P.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SCTAP3.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SIERRA.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/PILOTNOV.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/CZPROB.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/FIT1D.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/PILOT-JA.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SHIP08L.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/BNL2.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/NESM.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/CYCLE.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/acc-tight5.mps"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/SHIP12L.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/DEGEN3.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/GREENBEA.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/GREENBEB.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/80BAU3B.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/TRUSS.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/D2Q06C.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/WOODW.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/QAP12.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/D6CUBE.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/PILOT.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/DFL001.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/WOOD1P.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/FIT2P.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/PILOT87.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/STOCFOR3.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/QAP15.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/FIT2D.SIF"); + file_names.push_back(home_dir_str + "/projects/lp/src/tests/math/lp/test_files/netlib/MAROS-R7.SIF"); + minimums.insert("/projects/lp/src/tests/math/lp/test_files/netlib/FIT2P.SIF"); + minimums.insert("/projects/lp/src/tests/math/lp/test_files/netlib/DFL001.SIF"); + minimums.insert("/projects/lp/src/tests/math/lp/test_files/netlib/D2Q06C.SIF"); + minimums.insert("/projects/lp/src/tests/math/lp/test_files/netlib/80BAU3B.SIF"); + minimums.insert("/projects/lp/src/tests/math/lp/test_files/netlib/GREENBEB.SIF"); + minimums.insert("/projects/lp/src/tests/math/lp/test_files/netlib/GREENBEA.SIF"); + minimums.insert("/projects/lp/src/tests/math/lp/test_files/netlib/BNL2.SIF"); + minimums.insert("/projects/lp/src/tests/math/lp/test_files/netlib/SHIP08L.SIF"); + minimums.insert("/projects/lp/src/tests/math/lp/test_files/netlib/FIT1D.SIF"); + minimums.insert("/projects/lp/src/tests/math/lp/test_files/netlib/SCTAP3.SIF"); + minimums.insert("/projects/lp/src/tests/math/lp/test_files/netlib/SCSD8.SIF"); + minimums.insert("/projects/lp/src/tests/math/lp/test_files/netlib/SCSD6.SIF"); + minimums.insert("/projects/lp/src/tests/math/lp/test_files/netlib/MAROS-R7.SIF"); } void test_out_dir(std::string out_dir) { diff --git a/src/test/lp/nla_solver_test.cpp b/src/test/lp/nla_solver_test.cpp index 0363c58de..fcaa6b2d6 100644 --- a/src/test/lp/nla_solver_test.cpp +++ b/src/test/lp/nla_solver_test.cpp @@ -17,7 +17,7 @@ Revision History: --*/ -#include "util/lp/nla_solver.h" +#include "math/lp/nla_solver.h" namespace nla { void create_abcde(solver & nla, unsigned lp_a, @@ -482,7 +482,7 @@ void test_basic_sign_lemma() { } void test_order_lemma_params(bool var_equiv, int sign) { - enable_trace("nla_solver"); + /* enable_trace("nla_solver"); lp::lar_solver s; unsigned a = 0, b = 1, c = 2, d = 3, e = 4, f = 5, i = 8, j = 9, @@ -614,9 +614,11 @@ void test_order_lemma_params(bool var_equiv, int sign) { // } // SASSERT(found); + */ } void test_monotone_lemma() { + /* enable_trace("nla_solver"); lp::lar_solver s; unsigned a = 0, b = 1, c = 2, d = 3, e = 4, f = 5, @@ -679,9 +681,11 @@ void test_monotone_lemma() { vector lemma; SASSERT(nla.get_core()->test_check(lemma) == l_false); nla.get_core()->print_lemma(std::cout); + */ } void test_tangent_lemma_reg() { + /* enable_trace("nla_solver"); lp::lar_solver s; unsigned a = 0, b = 1, ab = 10; @@ -714,9 +718,11 @@ void test_tangent_lemma_reg() { vector lemma; SASSERT(nla.get_core()->test_check(lemma) == l_false); nla.get_core()->print_lemma(std::cout); + */ } void test_tangent_lemma_equiv() { + /* enable_trace("nla_solver"); lp::lar_solver s; unsigned a = 0, b = 1, k = 2, ab = 10; @@ -759,6 +765,7 @@ void test_tangent_lemma_equiv() { SASSERT(nla.get_core()->test_check(lemma) == l_false); nla.get_core()->print_lemma(std::cout); + */ } diff --git a/src/test/lp/smt_reader.h b/src/test/lp/smt_reader.h index 4bce99765..dcbe8121e 100644 --- a/src/test/lp/smt_reader.h +++ b/src/test/lp/smt_reader.h @@ -24,16 +24,16 @@ Revision History: #include #include #include -#include "util/lp/lp_primal_simplex.h" -#include "util/lp/lp_dual_simplex.h" -#include "util/lp/lar_solver.h" +#include "math/lp/lp_primal_simplex.h" +#include "math/lp/lp_dual_simplex.h" +#include "math/lp/lar_solver.h" #include #include #include #include -#include "util/lp/mps_reader.h" -#include "util/lp/ul_pair.h" -#include "util/lp/lar_constraints.h" +#include "math/lp/mps_reader.h" +#include "math/lp/ul_pair.h" +#include "math/lp/lar_constraints.h" #include #include namespace lp { diff --git a/src/test/lp/test_file_reader.h b/src/test/lp/test_file_reader.h index 74dad419b..8f461ea1c 100644 --- a/src/test/lp/test_file_reader.h +++ b/src/test/lp/test_file_reader.h @@ -26,8 +26,8 @@ Revision History: #include #include #include -#include "util/lp/lp_utils.h" -#include "util/lp/lp_solver.h" +#include "math/lp/lp_utils.h" +#include "math/lp/lp_solver.h" namespace lp {