diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 6f0190e7a..5c7ed33f8 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -677,25 +677,25 @@ void asserted_formulas::propagate_booleans() { cont = false; unsigned i = m_asserted_qhead; unsigned sz = m_asserted_formulas.size(); -#define PROCESS() { \ - expr * n = m_asserted_formulas.get(i); \ - proof * pr = m_asserted_formula_prs.get(i, 0); \ - expr_ref new_n(m); \ - proof_ref new_pr(m); \ - m_simplifier(n, new_n, new_pr); \ - m_asserted_formulas.set(i, new_n); \ - if (m.proofs_enabled()) { \ - new_pr = m.mk_modus_ponens(pr, new_pr); \ - m_asserted_formula_prs.set(i, new_pr); \ - } \ - if (n != new_n) { \ - cont = true; \ - modified = true; \ - } \ - if (m.is_not(new_n)) \ - m_simplifier.cache_result(to_app(new_n)->get_arg(0), m.mk_false(), m.mk_iff_false(new_pr)); \ - else \ - m_simplifier.cache_result(new_n, m.mk_true(), m.mk_iff_true(new_pr)); \ +#define PROCESS() { \ + expr * n = m_asserted_formulas.get(i); \ + proof * pr = m_asserted_formula_prs.get(i, 0); \ + expr_ref new_n(m); \ + proof_ref new_pr(m); \ + m_simplifier(n, new_n, new_pr); \ + m_asserted_formulas.set(i, new_n); \ + if (m.proofs_enabled()) { \ + new_pr = m.mk_modus_ponens(pr, new_pr); \ + m_asserted_formula_prs.set(i, new_pr); \ + } \ + if (n != new_n) { \ + cont = true; \ + modified = true; \ + } \ + if (m.is_not(new_n)) \ + m_simplifier.cache_result(to_app(new_n)->get_arg(0), m.mk_false(), m.mk_iff_false(new_pr)); \ + else \ + m_simplifier.cache_result(new_n, m.mk_true(), m.mk_iff_true(new_pr)); \ } for (; i < sz; i++) { PROCESS(); @@ -715,43 +715,43 @@ void asserted_formulas::propagate_booleans() { } #define MK_SIMPLIFIER(NAME, FUNCTOR, TAG, MSG, REDUCE) \ -bool asserted_formulas::NAME() { \ - IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \ - TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \ - FUNCTOR; \ - bool changed = false; \ - expr_ref_vector new_exprs(m); \ - proof_ref_vector new_prs(m); \ - unsigned i = m_asserted_qhead; \ - unsigned sz = m_asserted_formulas.size(); \ - for (; i < sz; i++) { \ - expr * n = m_asserted_formulas.get(i); \ - proof * pr = m_asserted_formula_prs.get(i, 0); \ - expr_ref new_n(m); \ - proof_ref new_pr(m); \ - functor(n, new_n, new_pr); \ - if (n == new_n.get()) { \ - push_assertion(n, pr, new_exprs, new_prs); \ - } \ - else if (m.proofs_enabled()) { \ - changed = true; \ - if (!new_pr) new_pr = m.mk_rewrite(n, new_n); \ - new_pr = m.mk_modus_ponens(pr, new_pr); \ - push_assertion(new_n, new_pr, new_exprs, new_prs); \ - } \ - else { \ - changed = true; \ - push_assertion(new_n, 0, new_exprs, new_prs); \ - } \ - } \ - swap_asserted_formulas(new_exprs, new_prs); \ - TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \ - if (changed && REDUCE) { \ - reduce_and_solve(); \ + bool asserted_formulas::NAME() { \ + IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \ TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \ - } \ - return changed; \ -} + FUNCTOR; \ + bool changed = false; \ + expr_ref_vector new_exprs(m); \ + proof_ref_vector new_prs(m); \ + unsigned i = m_asserted_qhead; \ + unsigned sz = m_asserted_formulas.size(); \ + for (; i < sz; i++) { \ + expr * n = m_asserted_formulas.get(i); \ + proof * pr = m_asserted_formula_prs.get(i, 0); \ + expr_ref new_n(m); \ + proof_ref new_pr(m); \ + functor(n, new_n, new_pr); \ + if (n == new_n.get()) { \ + push_assertion(n, pr, new_exprs, new_prs); \ + } \ + else if (m.proofs_enabled()) { \ + changed = true; \ + if (!new_pr) new_pr = m.mk_rewrite(n, new_n); \ + new_pr = m.mk_modus_ponens(pr, new_pr); \ + push_assertion(new_n, new_pr, new_exprs, new_prs); \ + } \ + else { \ + changed = true; \ + push_assertion(new_n, 0, new_exprs, new_prs); \ + } \ + } \ + swap_asserted_formulas(new_exprs, new_prs); \ + TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \ + if (changed && REDUCE) { \ + reduce_and_solve(); \ + TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \ + } \ + return changed; \ + } MK_SIMPLIFIER(pull_cheap_ite_trees, pull_cheap_ite_tree_star functor(m, m_simplifier), "pull_cheap_ite_trees", "pull-cheap-ite-trees", false); @@ -803,30 +803,30 @@ MK_SIMPLIFIER(cheap_quant_fourier_motzkin, elim_bounds_star functor(m), "elim_bo MK_SIMPLIFIER(elim_bvs_from_quantifiers, bv_elim_star functor(m), "bv_elim", "eliminate-bit-vectors-from-quantifiers", true); -#define LIFT_ITE(NAME, FUNCTOR, MSG) \ -void asserted_formulas::NAME() { \ - IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \ - TRACE("lift_ite", display(tout);); \ - FUNCTOR; \ - unsigned i = m_asserted_qhead; \ - unsigned sz = m_asserted_formulas.size(); \ - for (; i < sz; i++) { \ - expr * n = m_asserted_formulas.get(i); \ - proof * pr = m_asserted_formula_prs.get(i, 0); \ - expr_ref new_n(m); \ - proof_ref new_pr(m); \ - functor(n, new_n, new_pr); \ - TRACE("lift_ite_step", tout << mk_pp(n, m) << "\n";); \ - IF_IVERBOSE(10000, verbose_stream() << "lift before: " << get_num_exprs(n) << ", after: " << get_num_exprs(new_n) << "\n";); \ - m_asserted_formulas.set(i, new_n); \ - if (m.proofs_enabled()) { \ - new_pr = m.mk_modus_ponens(pr, new_pr); \ - m_asserted_formula_prs.set(i, new_pr); \ - } \ - } \ - TRACE("lift_ite", display(tout);); \ - reduce_and_solve(); \ -} +#define LIFT_ITE(NAME, FUNCTOR, MSG) \ + void asserted_formulas::NAME() { \ + IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \ + TRACE("lift_ite", display(tout);); \ + FUNCTOR; \ + unsigned i = m_asserted_qhead; \ + unsigned sz = m_asserted_formulas.size(); \ + for (; i < sz; i++) { \ + expr * n = m_asserted_formulas.get(i); \ + proof * pr = m_asserted_formula_prs.get(i, 0); \ + expr_ref new_n(m); \ + proof_ref new_pr(m); \ + functor(n, new_n, new_pr); \ + TRACE("lift_ite_step", tout << mk_pp(n, m) << "\n";); \ + IF_IVERBOSE(10000, verbose_stream() << "lift before: " << get_num_exprs(n) << ", after: " << get_num_exprs(new_n) << "\n";); \ + m_asserted_formulas.set(i, new_n); \ + if (m.proofs_enabled()) { \ + new_pr = m.mk_modus_ponens(pr, new_pr); \ + m_asserted_formula_prs.set(i, new_pr); \ + } \ + } \ + TRACE("lift_ite", display(tout);); \ + reduce_and_solve(); \ + } LIFT_ITE(lift_ite, push_app_ite functor(m_simplifier, m_params.m_lift_ite == LI_CONSERVATIVE), "lifting ite"); LIFT_ITE(ng_lift_ite, ng_push_app_ite functor(m_simplifier, m_params.m_ng_lift_ite == LI_CONSERVATIVE), "lifting ng ite"); diff --git a/src/util/lp/lp_primal_simplex.h b/src/util/lp/lp_primal_simplex.h index fcddb4eb1..715d76408 100644 --- a/src/util/lp/lp_primal_simplex.h +++ b/src/util/lp/lp_primal_simplex.h @@ -55,10 +55,6 @@ public: void set_core_solver_bounds(); - void update_time_limit_from_starting_time(int start_time) { - this->m_settings.time_limit -= (get_millisecond_span(start_time) / 1000.); - } - void find_maximal_solution(); void fill_A_x_and_basis_for_stage_one_total_inf(); diff --git a/src/util/lp/lp_primal_simplex.hpp b/src/util/lp/lp_primal_simplex.hpp index 9e1af2bbe..b6b6006e5 100644 --- a/src/util/lp/lp_primal_simplex.hpp +++ b/src/util/lp/lp_primal_simplex.hpp @@ -152,7 +152,6 @@ template void lp_primal_simplex::set_core_solver_ template void lp_primal_simplex::find_maximal_solution() { - int preprocessing_start_time = get_millisecond_count(); if (this->problem_is_empty()) { this->m_status = lp_status::EMPTY; return; @@ -169,7 +168,6 @@ template void lp_primal_simplex::find_maximal_sol fill_acceptable_values_for_x(); this->count_slacks_and_artificials(); set_core_solver_bounds(); - update_time_limit_from_starting_time(preprocessing_start_time); solve_with_total_inf(); } diff --git a/src/util/lp/lp_settings.h b/src/util/lp/lp_settings.h index 6b6aba2ad..aac3692f9 100644 --- a/src/util/lp/lp_settings.h +++ b/src/util/lp/lp_settings.h @@ -8,9 +8,9 @@ #include #include #include -#include #include #include "util/lp/lp_utils.h" +#include "util/stopwatch.h" namespace lean { typedef unsigned var_index; @@ -69,10 +69,6 @@ enum non_basic_column_value_position { at_low_bound, at_upper_bound, at_fixed, f template bool is_epsilon_small(const X & v, const double& eps); // forward definition -int get_millisecond_count(); -int get_millisecond_span(int start_time); - - class lp_resource_limit { public: virtual bool get_cancel_flag() = 0; @@ -92,12 +88,13 @@ struct lp_settings { private: class default_lp_resource_limit : public lp_resource_limit { lp_settings& m_settings; - int m_start_time; + stopwatch m_sw; public: - default_lp_resource_limit(lp_settings& s): m_settings(s), m_start_time(get_millisecond_count()) {} + default_lp_resource_limit(lp_settings& s): m_settings(s) { + m_sw.start(); + } virtual bool get_cancel_flag() { - int span_in_mills = get_millisecond_span(m_start_time); - return (span_in_mills / 1000.0 > m_settings.time_limit); + return (m_sw.get_current_seconds() > m_settings.time_limit); } }; diff --git a/src/util/lp/lp_settings.hpp b/src/util/lp/lp_settings.hpp index b57a3acda..b27d837e0 100644 --- a/src/util/lp/lp_settings.hpp +++ b/src/util/lp/lp_settings.hpp @@ -52,19 +52,6 @@ lp_status lp_status_from_string(std::string status) { lean_unreachable(); return lp_status::UNKNOWN; // it is unreachable } -int get_millisecond_count() { - timeb tb; - ftime(&tb); - return tb.millitm + (tb.time & 0xfffff) * 1000; -} - -int get_millisecond_span(int start_time) { - int span = get_millisecond_count() - start_time; - if (span < 0) - span += 0x100000 * 1000; - return span; -} - template diff --git a/src/util/lp/sparse_matrix.hpp b/src/util/lp/sparse_matrix.hpp index ff6ac9997..32bb8ed4e 100644 --- a/src/util/lp/sparse_matrix.hpp +++ b/src/util/lp/sparse_matrix.hpp @@ -1050,8 +1050,8 @@ bool sparse_matrix::get_pivot_for_column(unsigned &i, unsigned &j, int c_p if (i_inv < k) continue; unsigned j_inv = adjust_column_inverse(j); if (j_inv < k) continue; - int small = elem_is_too_small(i, j, c_partial_pivoting); - if (!small) { + int _small = elem_is_too_small(i, j, c_partial_pivoting); + if (!_small) { #ifdef LEAN_DEBUG // if (!really_best_pivot(i, j, c_partial_pivoting, k)) { // print_active_matrix(k); @@ -1063,7 +1063,7 @@ bool sparse_matrix::get_pivot_for_column(unsigned &i, unsigned &j, int c_p j = j_inv; return true; } - if (small != 2) { // 2 means that the pair is not in the matrix + if (_small != 2) { // 2 means that the pair is not in the matrix pivots_candidates_that_are_too_small.push_back(std::make_pair(i, j)); } }