From 48c0f8694facce9a645cf81beee2a9a7449450da Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 14 Nov 2022 20:01:00 -0800 Subject: [PATCH] euf-completion bug fix, streamline name to solve_eqs --- src/ast/simplifiers/euf_completion.cpp | 3 ++- src/tactic/core/solve_eqs_tactic.h | 15 ++++----------- 2 files changed, 6 insertions(+), 12 deletions(-) diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp index 0f03d7fe1c8..7c27a01bb92 100644 --- a/src/ast/simplifiers/euf_completion.cpp +++ b/src/ast/simplifiers/euf_completion.cpp @@ -90,7 +90,8 @@ namespace euf { return; } - for (unsigned i = m_qhead; i < m_fmls.size(); ++i) { + unsigned sz = m_fmls.size(); + for (unsigned i = m_qhead; i < sz; ++i) { auto [f, d] = m_fmls[i](); expr_dependency_ref dep(d, m); diff --git a/src/tactic/core/solve_eqs_tactic.h b/src/tactic/core/solve_eqs_tactic.h index fa095aad0c3..188f37f3414 100644 --- a/src/tactic/core/solve_eqs_tactic.h +++ b/src/tactic/core/solve_eqs_tactic.h @@ -22,26 +22,19 @@ Module Name: #include "ast/simplifiers/solve_eqs.h" -class solve_eqs2_tactic_factory : public dependent_expr_simplifier_factory { +class solve_eqs_tactic_factory : public dependent_expr_simplifier_factory { public: dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override { return alloc(euf::solve_eqs, m, s); } }; -inline tactic * mk_solve_eqs2_tactic(ast_manager& m, params_ref const& p = params_ref()) { - return alloc(dependent_expr_state_tactic, m, p, alloc(solve_eqs2_tactic_factory), "solve-eqs"); +inline tactic * mk_solve_eqs_tactic(ast_manager& m, params_ref const& p = params_ref()) { + return alloc(dependent_expr_state_tactic, m, p, alloc(solve_eqs_tactic_factory), "solve-eqs"); } -#if 1 -inline tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref()) { - return mk_solve_eqs2_tactic(m, p); -} -#endif - - /* - ADD_TACTIC("solve-eqs", "solve for variables.", "mk_solve_eqs2_tactic(m, p)") + ADD_TACTIC("solve-eqs", "solve for variables.", "mk_solve_eqs_tactic(m, p)") */