From 2c55aa5466197ad5ee92c732fa14305a9ba69f3e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 17 Jan 2024 18:03:46 -0800 Subject: [PATCH] remove unused code Signed-off-by: Nikolaj Bjorner --- src/math/lp/factorization.cpp | 30 +++++++++++++++++---------- src/math/lp/factorization.h | 10 --------- src/math/lp/nla_core.cpp | 39 ----------------------------------- src/math/lp/nla_core.h | 10 +-------- src/math/lp/nla_solver.h | 2 +- src/sat/smt/arith_solver.cpp | 2 +- src/smt/theory_lra.cpp | 2 +- 7 files changed, 23 insertions(+), 72 deletions(-) diff --git a/src/math/lp/factorization.cpp b/src/math/lp/factorization.cpp index 229fca61f83..e1dcff626dd 100644 --- a/src/math/lp/factorization.cpp +++ b/src/math/lp/factorization.cpp @@ -1,3 +1,12 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Author: +Lev Nachmanson (levnach) +Nikolaj Bjorner (nbjorner) + +--*/ + #include "util/vector.h" #include "math/lp/factorization.h" namespace nla { @@ -7,11 +16,10 @@ void const_iterator_mon::init_vars_by_the_mask(unsigned_vector & k_vars, unsigne SASSERT(m_mask.size() + 1 == m_ff->m_vars.size()); k_vars.push_back(m_ff->m_vars.back()); for (unsigned j = 0; j < m_mask.size(); j++) { - if (m_mask[j]) { - k_vars.push_back(m_ff->m_vars[j]); - } else { - j_vars.push_back(m_ff->m_vars[j]); - } + if (m_mask[j]) + k_vars.push_back(m_ff->m_vars[j]); + else + j_vars.push_back(m_ff->m_vars[j]); } } // todo : do we need the sign? @@ -29,9 +37,9 @@ bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const m_full_factorization_returned = true; return false; } - if (k_vars.size() == 1) { - k.set(k_vars[0], factor_type::VAR); - } else { + if (k_vars.size() == 1) + k.set(k_vars[0], factor_type::VAR); + else { unsigned i; if (!m_ff->find_canonical_monic_of_vars(k_vars, i)) { ++m_num_failures; @@ -41,9 +49,9 @@ bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const } m_num_failures = 0; - if (j_vars.size() == 1) { - j.set(j_vars[0], factor_type::VAR); - } else { + if (j_vars.size() == 1) + j.set(j_vars[0], factor_type::VAR); + else { unsigned i; if (!m_ff->find_canonical_monic_of_vars(j_vars, i)) { ++m_num_failures; diff --git a/src/math/lp/factorization.h b/src/math/lp/factorization.h index 04529d033c5..e1096a75f60 100644 --- a/src/math/lp/factorization.h +++ b/src/math/lp/factorization.h @@ -2,20 +2,10 @@ /*++ Copyright (c) 2017 Microsoft Corporation - Module Name: - - - - Abstract: - - - Author: Lev Nachmanson (levnach) Nikolaj Bjorner (nbjorner) - Revision History: - --*/ #pragma once diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index f36fab52e2f..e2db006fa7c 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1434,45 +1434,6 @@ void core::patch_monomials_on_to_refine() { void core::patch_monomials() { m_cautious_patching = true; patch_monomials_on_to_refine(); - if (m_to_refine.size() == 0 || !params().arith_nl_expensive_patching()) { - return; - } - NOT_IMPLEMENTED_YET(); - m_cautious_patching = false; - patch_monomials_on_to_refine(); - lra.push(); - save_tableau(); - constrain_nl_in_tableau(); - if (solve_tableau() && integrality_holds()) { - lra.pop(1); - } else { - lra.pop(); - restore_tableau(); - lra.clear_inf_heap(); - } - SASSERT(lra.ax_is_correct()); -} - -void core::constrain_nl_in_tableau() { - NOT_IMPLEMENTED_YET(); -} - -bool core::solve_tableau() { - NOT_IMPLEMENTED_YET(); - return false; -} - -void core::restore_tableau() { - NOT_IMPLEMENTED_YET(); -} - -void core::save_tableau() { - NOT_IMPLEMENTED_YET(); -} - -bool core::integrality_holds() { - NOT_IMPLEMENTED_YET(); - return false; } /** diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 29effd4e4b7..253306bcd5f 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -424,18 +424,10 @@ class core { vector const& literals() const { return m_literals; } vector const& equalities() const { return m_equalities; } vector const& fixed_equalities() const { return m_fixed_equalities; } - bool check_feasible() const { return m_check_feasible; } + bool should_check_feasible() const { return m_check_feasible; } void add_fixed_equality(lp::lpvar v, rational const& k, lp::explanation const& e) { m_fixed_equalities.push_back({v, k, e}); } void add_equality(lp::lpvar i, lp::lpvar j, lp::explanation const& e) { m_equalities.push_back({i, j, e}); } -private: - void restore_patched_values(); - void constrain_nl_in_tableau(); - bool solve_tableau(); - void restore_tableau(); - void save_tableau(); - bool integrality_holds(); - }; // end of core diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index 1fbafdf6ba7..1e47362fdf4 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -53,6 +53,6 @@ namespace nla { vector const& literals() const; vector const& fixed_equalities() const; vector const& equalities() const; - bool check_feasible() const { return m_core->check_feasible(); } + bool should_check_feasible() const { return m_core->should_check_feasible(); } }; } diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 078515184c1..9b4e40242e1 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -1506,7 +1506,7 @@ namespace arith { } void solver::add_lemmas() { - if (m_nla->check_feasible()) { + if (m_nla->should_check_feasible()) { auto is_sat = make_feasible(); if (l_false == is_sat) { get_infeasibility_explanation_and_set_conflict(); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index b31867790b7..4c9e02738ef 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2151,7 +2151,7 @@ class theory_lra::imp { } void add_lemmas() { - if (m_nla->check_feasible()) { + if (m_nla->should_check_feasible()) { auto is_sat = make_feasible(); if (l_false == is_sat) { get_infeasibility_explanation_and_set_conflict();