From 9f2b18cac514c9b79c0f7d0da3e96ecf5680ac1c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 7 Dec 2021 13:37:57 -0800 Subject: [PATCH] add tactic name Signed-off-by: Nikolaj Bjorner --- .../ackermannize_bv_tactic.cpp | 2 + .../subpaving/tactic/subpaving_tactic.cpp | 2 + src/muz/fp/horn_tactic.cpp | 2 + src/nlsat/tactic/nlsat_tactic.cpp | 2 + src/qe/nlqsat.cpp | 2 + src/qe/qe_lite.cpp | 2 + src/qe/qe_tactic.cpp | 2 + src/qe/qsat.cpp | 2 + src/sat/tactic/sat_tactic.cpp | 2 + src/smt/tactic/ctx_solver_simplify_tactic.cpp | 2 + src/smt/tactic/smt_tactic_core.cpp | 12 +-- src/smt/tactic/unit_subsumption_tactic.cpp | 2 + src/solver/parallel_tactic.cpp | 2 + src/solver/solver2tactic.cpp | 2 + src/tactic/aig/aig_tactic.cpp | 2 + src/tactic/arith/add_bounds_tactic.cpp | 2 + src/tactic/arith/arith_bounds_tactic.cpp | 2 + src/tactic/arith/card2bv_tactic.cpp | 2 + src/tactic/arith/degree_shift_tactic.cpp | 2 + src/tactic/arith/diff_neq_tactic.cpp | 2 + src/tactic/arith/eq2bv_tactic.cpp | 2 + src/tactic/arith/factor_tactic.cpp | 2 + src/tactic/arith/fix_dl_var_tactic.cpp | 2 + src/tactic/arith/fm_tactic.cpp | 2 + src/tactic/arith/lia2card_tactic.cpp | 2 + src/tactic/arith/lia2pb_tactic.cpp | 2 + src/tactic/arith/nla2bv_tactic.cpp | 2 + src/tactic/arith/normalize_bounds_tactic.cpp | 2 + src/tactic/arith/pb2bv_tactic.cpp | 2 + src/tactic/arith/propagate_ineqs_tactic.cpp | 2 + src/tactic/arith/purify_arith_tactic.cpp | 2 + src/tactic/arith/recover_01_tactic.cpp | 2 + src/tactic/bv/bit_blaster_tactic.cpp | 2 + src/tactic/bv/bv1_blaster_tactic.cpp | 2 + src/tactic/bv/bv_bound_chk_tactic.cpp | 1 + src/tactic/bv/bv_size_reduction_tactic.cpp | 2 + src/tactic/bv/bvarray2uf_tactic.cpp | 2 + src/tactic/bv/dt2bv_tactic.cpp | 2 + src/tactic/bv/elim_small_bv_tactic.cpp | 2 + src/tactic/bv/max_bv_sharing_tactic.cpp | 2 + src/tactic/core/blast_term_ite_tactic.cpp | 2 + src/tactic/core/cofactor_term_ite_tactic.cpp | 1 + src/tactic/core/collect_statistics_tactic.cpp | 2 + src/tactic/core/ctx_simplify_tactic.h | 2 + src/tactic/core/der_tactic.cpp | 2 + src/tactic/core/distribute_forall_tactic.cpp | 2 + src/tactic/core/dom_simplify_tactic.cpp | 1 + src/tactic/core/dom_simplify_tactic.h | 2 + src/tactic/core/elim_term_ite_tactic.cpp | 2 + src/tactic/core/elim_uncnstr_tactic.cpp | 2 + src/tactic/core/injectivity_tactic.cpp | 2 + src/tactic/core/nnf_tactic.cpp | 2 + src/tactic/core/occf_tactic.cpp | 2 + src/tactic/core/pb_preprocess_tactic.cpp | 2 + src/tactic/core/propagate_values_tactic.cpp | 2 + src/tactic/core/reduce_args_tactic.cpp | 102 ++++++++---------- src/tactic/core/reduce_invertible_tactic.cpp | 2 + src/tactic/core/simplify_tactic.h | 2 + src/tactic/core/solve_eqs_tactic.cpp | 2 + src/tactic/core/special_relations_tactic.h | 2 + src/tactic/core/split_clause_tactic.cpp | 2 + src/tactic/core/symmetry_reduce_tactic.cpp | 2 + src/tactic/core/tseitin_cnf_tactic.cpp | 2 + src/tactic/fpa/fpa2bv_tactic.cpp | 2 + .../portfolio/solver_subsumption_tactic.cpp | 2 + src/tactic/sls/sls_tactic.cpp | 2 + src/tactic/smtlogics/qfufbv_tactic.cpp | 2 + src/tactic/tactic.cpp | 2 + src/tactic/tactic.h | 2 + src/tactic/tactical.cpp | 30 ++++++ src/tactic/ufbv/macro_finder_tactic.cpp | 2 + src/tactic/ufbv/quasi_macros_tactic.cpp | 2 + src/tactic/ufbv/ufbv_rewriter_tactic.cpp | 2 + 73 files changed, 218 insertions(+), 63 deletions(-) diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp index dcf6a7c5923..79cad2fb224 100644 --- a/src/ackermannization/ackermannize_bv_tactic.cpp +++ b/src/ackermannization/ackermannize_bv_tactic.cpp @@ -31,6 +31,8 @@ class ackermannize_bv_tactic : public tactic { ~ackermannize_bv_tactic() override { } + char const* name() const override { return "ackermannize_bv"; } + void operator()(goal_ref const & g, goal_ref_buffer & result) override { tactic_report report("ackermannize_bv", *g); fail_if_unsat_core_generation("ackermannize", g); diff --git a/src/math/subpaving/tactic/subpaving_tactic.cpp b/src/math/subpaving/tactic/subpaving_tactic.cpp index c453806bff1..1bc0cb6307d 100644 --- a/src/math/subpaving/tactic/subpaving_tactic.cpp +++ b/src/math/subpaving/tactic/subpaving_tactic.cpp @@ -220,6 +220,8 @@ class subpaving_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "subpaving"; } + tactic * translate(ast_manager & m) override { return alloc(subpaving_tactic, m, m_params); } diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp index 591e5794456..b66ddf27588 100644 --- a/src/muz/fp/horn_tactic.cpp +++ b/src/muz/fp/horn_tactic.cpp @@ -392,6 +392,8 @@ class horn_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "horn"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp index 8de4781992b..ddf85ce19c5 100644 --- a/src/nlsat/tactic/nlsat_tactic.cpp +++ b/src/nlsat/tactic/nlsat_tactic.cpp @@ -223,6 +223,8 @@ class nlsat_tactic : public tactic { SASSERT(m_imp == 0); } + char const* name() const override { return "nlsat"; } + void updt_params(params_ref const & p) override { m_params = p; } diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index 6439a91c906..28cfa5c3e9c 100644 --- a/src/qe/nlqsat.cpp +++ b/src/qe/nlqsat.cpp @@ -839,6 +839,8 @@ namespace qe { ~nlqsat() override { } + char const* name() const override { return "nlqsat"; } + void updt_params(params_ref const & p) override { params_ref p2(p); p2.set_bool("factor", false); diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 58fe3b29363..f6dd9c7127e 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -2459,6 +2459,8 @@ class qe_lite_tactic : public tactic { m_params(p), m_qe(m, p, true) {} + char const* name() const override { return "qe_lite"; } + tactic * translate(ast_manager & m) override { return alloc(qe_lite_tactic, m, m_params); } diff --git a/src/qe/qe_tactic.cpp b/src/qe/qe_tactic.cpp index 0aa3824e783..da1ce5efd8f 100644 --- a/src/qe/qe_tactic.cpp +++ b/src/qe/qe_tactic.cpp @@ -100,6 +100,8 @@ class qe_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "qe"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 537a7ab560b..767b96e5d55 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -1257,6 +1257,8 @@ namespace qe { ~qsat() override { clear(); } + + char const* name() const override { return "qsat"; } void updt_params(params_ref const & p) override { } diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index 521a70fb77b..38c25eae37c 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -198,6 +198,8 @@ class sat_tactic : public tactic { SASSERT(m_imp == 0); } + char const* name() const override { return "sat"; } + void updt_params(params_ref const & p) override { m_params = p; if (m_imp) m_imp->updt_params(p); diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp index fd05c4a8e66..6b1d1b7f460 100644 --- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp +++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp @@ -63,6 +63,8 @@ class ctx_solver_simplify_tactic : public tactic { m_fns.reset(); } + char const* name() const override { return "ctx_solver_simplify"; } + void updt_params(params_ref const & p) override { m_solver.updt_params(p); } diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp index 9e9d3a9de8b..5cbe469fd74 100644 --- a/src/smt/tactic/smt_tactic_core.cpp +++ b/src/smt/tactic/smt_tactic_core.cpp @@ -41,18 +41,16 @@ class smt_tactic : public tactic { smt_params m_params; params_ref m_params_ref; statistics m_stats; - smt::kernel * m_ctx; + smt::kernel* m_ctx = nullptr; symbol m_logic; - progress_callback * m_callback; - bool m_candidate_models; - bool m_fail_if_inconclusive; + progress_callback* m_callback = nullptr; + bool m_candidate_models = false; + bool m_fail_if_inconclusive = false; public: smt_tactic(ast_manager& m, params_ref const & p): m(m), m_params_ref(p), - m_ctx(nullptr), - m_callback(nullptr), m_vars(m) { updt_params_core(p); TRACE("smt_tactic", tout << "p: " << p << "\n";); @@ -66,6 +64,8 @@ class smt_tactic : public tactic { SASSERT(m_ctx == nullptr); } + char const* name() const override { return "smt"; } + smt_params & fparams() { return m_params; } diff --git a/src/smt/tactic/unit_subsumption_tactic.cpp b/src/smt/tactic/unit_subsumption_tactic.cpp index 44086aa7ef3..97ce4a1c1a1 100644 --- a/src/smt/tactic/unit_subsumption_tactic.cpp +++ b/src/smt/tactic/unit_subsumption_tactic.cpp @@ -38,6 +38,8 @@ struct unit_subsumption_tactic : public tactic { m_clauses(m) { } + char const* name() const override { return "unit_subsumption"; } + void cleanup() override {} void operator()(/* in */ goal_ref const & in, diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp index 8336f005096..2f3ba7798a7 100644 --- a/src/solver/parallel_tactic.cpp +++ b/src/solver/parallel_tactic.cpp @@ -757,6 +757,8 @@ class parallel_tactic : public tactic { init(); } + char const* name() const override { return "parallel_tactic"; } + void operator()(const goal_ref & g,goal_ref_buffer & result) override { cleanup(); fail_if_proof_generation("parallel-tactic", g); diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp index 8641a2aa876..389ee124b11 100644 --- a/src/solver/solver2tactic.cpp +++ b/src/solver/solver2tactic.cpp @@ -186,6 +186,8 @@ class solver2tactic : public tactic { tactic * translate(ast_manager & m) override { return alloc(solver2tactic, m_solver->translate(m, m_params)); } + + char const* name() const override { return "solver2tactic"; } }; tactic* mk_solver2tactic(solver* s) { return alloc(solver2tactic, s); } diff --git a/src/tactic/aig/aig_tactic.cpp b/src/tactic/aig/aig_tactic.cpp index 7b80582fe83..5ffc0dc20ff 100644 --- a/src/tactic/aig/aig_tactic.cpp +++ b/src/tactic/aig/aig_tactic.cpp @@ -45,6 +45,8 @@ class aig_tactic : public tactic { aig_tactic(params_ref const & p = params_ref()):m_aig_manager(nullptr) { updt_params(p); } + + char const* name() const override { return "aig"; } tactic * translate(ast_manager & m) override { aig_tactic * t = alloc(aig_tactic); diff --git a/src/tactic/arith/add_bounds_tactic.cpp b/src/tactic/arith/add_bounds_tactic.cpp index b1367ea212c..4493568bf40 100644 --- a/src/tactic/arith/add_bounds_tactic.cpp +++ b/src/tactic/arith/add_bounds_tactic.cpp @@ -145,6 +145,8 @@ class add_bounds_tactic : public tactic { ~add_bounds_tactic() override { dealloc(m_imp); } + + char const* name() const override { return "add_bounds"; } void updt_params(params_ref const & p) override { m_params = p; diff --git a/src/tactic/arith/arith_bounds_tactic.cpp b/src/tactic/arith/arith_bounds_tactic.cpp index a8fcc4e0000..87308078a6d 100644 --- a/src/tactic/arith/arith_bounds_tactic.cpp +++ b/src/tactic/arith/arith_bounds_tactic.cpp @@ -27,6 +27,8 @@ struct arith_bounds_tactic : public tactic { /* out */ goal_ref_buffer & result) override { bounds_arith_subsumption(in, result); } + + char const* name() const override { return "arith_bounds"; } tactic* translate(ast_manager & mgr) override { return alloc(arith_bounds_tactic, mgr); diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp index 55227055191..fce096f230d 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -42,6 +42,8 @@ class card2bv_tactic : public tactic { ~card2bv_tactic() override { } + char const* name() const override { return "card2bv"; } + void updt_params(params_ref const & p) override { m_params = p; } diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp index d3c5bb74c92..e34910e78a5 100644 --- a/src/tactic/arith/degree_shift_tactic.cpp +++ b/src/tactic/arith/degree_shift_tactic.cpp @@ -284,6 +284,8 @@ class degree_shift_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "degree_shift"; } + void operator()(goal_ref const & in, goal_ref_buffer & result) override { (*m_imp)(in, result); diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp index a2ca66af267..92ce7cd295d 100644 --- a/src/tactic/arith/diff_neq_tactic.cpp +++ b/src/tactic/arith/diff_neq_tactic.cpp @@ -357,6 +357,8 @@ class diff_neq_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "diff_neq"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp index 865c268a1d7..a1a1a56ccc2 100644 --- a/src/tactic/arith/eq2bv_tactic.cpp +++ b/src/tactic/arith/eq2bv_tactic.cpp @@ -268,6 +268,8 @@ class eq2bv_tactic : public tactic { tactic * translate(ast_manager & m) override { return alloc(eq2bv_tactic, m); } + + char const* name() const override { return "eq2bv"; } void collect_param_descrs(param_descrs & r) override { } diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp index 7875aaf6dd5..07b59a3f941 100644 --- a/src/tactic/arith/factor_tactic.cpp +++ b/src/tactic/arith/factor_tactic.cpp @@ -294,6 +294,8 @@ class factor_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "factor"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->m_rw.cfg().updt_params(p); diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp index c5d11968550..f2039c37834 100644 --- a/src/tactic/arith/fix_dl_var_tactic.cpp +++ b/src/tactic/arith/fix_dl_var_tactic.cpp @@ -300,6 +300,8 @@ class fix_dl_var_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "fix_dl_var"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp index 4f10b0b3f19..ef8109de06c 100644 --- a/src/tactic/arith/fm_tactic.cpp +++ b/src/tactic/arith/fm_tactic.cpp @@ -1642,6 +1642,8 @@ class fm_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "fm"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index ae0467039ce..77786e26713 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -132,6 +132,8 @@ class lia2card_tactic : public tactic { dealloc(m_todo); } + char const* name() const override { return "lia2card"; } + void updt_params(params_ref const & p) override { m_params = p; m_compile_equality = p.get_bool("compile_equality", true); diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index 9af642e6919..d67f49a3735 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -305,6 +305,8 @@ class lia2pb_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "lia2pb"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp index 43def0741db..887cc9e31ae 100644 --- a/src/tactic/arith/nla2bv_tactic.cpp +++ b/src/tactic/arith/nla2bv_tactic.cpp @@ -438,6 +438,8 @@ class nla2bv_tactic : public tactic { ~nla2bv_tactic() override { } + char const* name() const override { return "nla2bv"; } + void updt_params(params_ref const & p) override { m_params.append(p); } diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp index 957859cc73d..b7ef28f4970 100644 --- a/src/tactic/arith/normalize_bounds_tactic.cpp +++ b/src/tactic/arith/normalize_bounds_tactic.cpp @@ -153,6 +153,8 @@ class normalize_bounds_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "normalize_bounds"; } + void updt_params(params_ref const & p) override { m_imp->updt_params(p); } diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index 98724923bb2..b63c85f1b15 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -1007,6 +1007,8 @@ class pb2bv_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "pb2bv"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/arith/propagate_ineqs_tactic.cpp b/src/tactic/arith/propagate_ineqs_tactic.cpp index f4169cfba05..d55ea4ecf11 100644 --- a/src/tactic/arith/propagate_ineqs_tactic.cpp +++ b/src/tactic/arith/propagate_ineqs_tactic.cpp @@ -49,6 +49,8 @@ class propagate_ineqs_tactic : public tactic { ~propagate_ineqs_tactic() override; + char const* name() const override { return "propagate_ineqs"; } + void updt_params(params_ref const & p) override; void collect_param_descrs(param_descrs & r) override {} diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 1691fe29a34..db43a3ee60a 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -903,6 +903,8 @@ class purify_arith_tactic : public tactic { ~purify_arith_tactic() override { } + char const* name() const override { return "purify_arith"; } + void updt_params(params_ref const & p) override { m_params = p; } diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp index 7e1fe17ca9e..a7cef82e3f4 100644 --- a/src/tactic/arith/recover_01_tactic.cpp +++ b/src/tactic/arith/recover_01_tactic.cpp @@ -398,6 +398,8 @@ class recover_01_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "recover_01"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/bv/bit_blaster_tactic.cpp b/src/tactic/bv/bit_blaster_tactic.cpp index 60dabbf5b29..744f207f357 100644 --- a/src/tactic/bv/bit_blaster_tactic.cpp +++ b/src/tactic/bv/bit_blaster_tactic.cpp @@ -119,6 +119,8 @@ class bit_blaster_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "bit_blaster"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp index 9fd077599d6..3af58bf6648 100644 --- a/src/tactic/bv/bv1_blaster_tactic.cpp +++ b/src/tactic/bv/bv1_blaster_tactic.cpp @@ -431,6 +431,8 @@ class bv1_blaster_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "bv1_blaster"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->m_rw.cfg().updt_params(p); diff --git a/src/tactic/bv/bv_bound_chk_tactic.cpp b/src/tactic/bv/bv_bound_chk_tactic.cpp index baef6c4f2b5..e0b6e4d8122 100644 --- a/src/tactic/bv/bv_bound_chk_tactic.cpp +++ b/src/tactic/bv/bv_bound_chk_tactic.cpp @@ -140,6 +140,7 @@ class bv_bound_chk_tactic : public tactic { void cleanup() override; void collect_statistics(statistics & st) const override; void reset_statistics() override; + char const* name() const override { return "bv_bound_chk"; } }; class bv_bound_chk_tactic::imp { diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index 5b9a4b21e24..a9d15a2a6a2 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -54,6 +54,8 @@ class bv_size_reduction_tactic : public tactic { return alloc(bv_size_reduction_tactic, m); } + char const* name() const override { return "bv_size"; } + void operator()(goal_ref const & g, goal_ref_buffer & result) override; void cleanup() override { diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp index 0d1925a4a23..d0bd6538b3c 100644 --- a/src/tactic/bv/bvarray2uf_tactic.cpp +++ b/src/tactic/bv/bvarray2uf_tactic.cpp @@ -113,6 +113,8 @@ class bvarray2uf_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "bvarray2uf"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp index 3b18222af92..4f9ae6e9ddc 100644 --- a/src/tactic/bv/dt2bv_tactic.cpp +++ b/src/tactic/bv/dt2bv_tactic.cpp @@ -104,6 +104,8 @@ class dt2bv_tactic : public tactic { dt2bv_tactic(ast_manager& m, params_ref const& p): m(m), m_params(p), m_dt(m), m_bv(m), m_is_fd(*this) {} + + char const* name() const override { return "dt2bv"; } tactic * translate(ast_manager & m) override { return alloc(dt2bv_tactic, m, m_params); diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp index 178a8fc77da..7c72abde978 100644 --- a/src/tactic/bv/elim_small_bv_tactic.cpp +++ b/src/tactic/bv/elim_small_bv_tactic.cpp @@ -234,6 +234,8 @@ class elim_small_bv_tactic : public tactic { m_params(p) { } + char const* name() const override { return "elim_small_bv"; } + tactic * translate(ast_manager & m) override { return alloc(elim_small_bv_tactic, m, m_params); } diff --git a/src/tactic/bv/max_bv_sharing_tactic.cpp b/src/tactic/bv/max_bv_sharing_tactic.cpp index 16e4b9679dd..0efe4f58cdf 100644 --- a/src/tactic/bv/max_bv_sharing_tactic.cpp +++ b/src/tactic/bv/max_bv_sharing_tactic.cpp @@ -277,6 +277,8 @@ class max_bv_sharing_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "max_bv_sharing"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->m_rw.cfg().updt_params(p); diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp index 97662a0c949..fe126973210 100644 --- a/src/tactic/core/blast_term_ite_tactic.cpp +++ b/src/tactic/core/blast_term_ite_tactic.cpp @@ -171,6 +171,8 @@ class blast_term_ite_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "blast_term_ite"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->m_rw.m_cfg.updt_params(p); diff --git a/src/tactic/core/cofactor_term_ite_tactic.cpp b/src/tactic/core/cofactor_term_ite_tactic.cpp index 8260d59c758..d1b8f5b1bbe 100644 --- a/src/tactic/core/cofactor_term_ite_tactic.cpp +++ b/src/tactic/core/cofactor_term_ite_tactic.cpp @@ -51,6 +51,7 @@ class cofactor_term_ite_tactic : public tactic { } ~cofactor_term_ite_tactic() override {} + char const* name() const override { return "cofactor"; } void updt_params(params_ref const & p) override { m_params = p; m_elim_ite.updt_params(p); } void collect_param_descrs(param_descrs & r) override { m_elim_ite.collect_param_descrs(r); } diff --git a/src/tactic/core/collect_statistics_tactic.cpp b/src/tactic/core/collect_statistics_tactic.cpp index b3c6d0e24d0..3d8ebfb1291 100644 --- a/src/tactic/core/collect_statistics_tactic.cpp +++ b/src/tactic/core/collect_statistics_tactic.cpp @@ -53,6 +53,8 @@ class collect_statistics_tactic : public tactic { ~collect_statistics_tactic() override {} + char const* name() const override { return "collect_statistics"; } + tactic * translate(ast_manager & m_) override { return alloc(collect_statistics_tactic, m_, m_params); } diff --git a/src/tactic/core/ctx_simplify_tactic.h b/src/tactic/core/ctx_simplify_tactic.h index e7c1660c8cd..0beced06e68 100644 --- a/src/tactic/core/ctx_simplify_tactic.h +++ b/src/tactic/core/ctx_simplify_tactic.h @@ -49,6 +49,8 @@ class ctx_simplify_tactic : public tactic { ~ctx_simplify_tactic() override; + char const* name() const override { return "ctx_simplify"; } + void updt_params(params_ref const & p) override; static void get_param_descrs(param_descrs & r); void collect_param_descrs(param_descrs & r) override { get_param_descrs(r); } diff --git a/src/tactic/core/der_tactic.cpp b/src/tactic/core/der_tactic.cpp index f2620201553..0118048032b 100644 --- a/src/tactic/core/der_tactic.cpp +++ b/src/tactic/core/der_tactic.cpp @@ -68,6 +68,8 @@ class der_tactic : public tactic { ~der_tactic() override { dealloc(m_imp); } + + char const* name() const override { return "der"; } void operator()(goal_ref const & in, goal_ref_buffer & result) override { diff --git a/src/tactic/core/distribute_forall_tactic.cpp b/src/tactic/core/distribute_forall_tactic.cpp index cb7eac49875..1d171aae3fa 100644 --- a/src/tactic/core/distribute_forall_tactic.cpp +++ b/src/tactic/core/distribute_forall_tactic.cpp @@ -102,6 +102,8 @@ class distribute_forall_tactic : public tactic { return alloc(distribute_forall_tactic); } + char const* name() const override { return "distribute_forall"; } + void operator()(goal_ref const & g, goal_ref_buffer & result) override { ast_manager & m = g->m(); diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 719de891150..1dda062c8c8 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -182,6 +182,7 @@ tactic * dom_simplify_tactic::translate(ast_manager & m) { return alloc(dom_simplify_tactic, m, m_simplifier->translate(m), m_params); } + void dom_simplify_tactic::operator()(goal_ref const & in, goal_ref_buffer & result) { tactic_report report("dom-simplify", *in.get()); simplify_goal(*(in.get())); diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index 541d50838c2..b1f452d42bd 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -131,6 +131,8 @@ class dom_simplify_tactic : public tactic { ~dom_simplify_tactic() override; + char const* dom_simplify_tactic::name() const { return "dom_simplify"; } + tactic * translate(ast_manager & m) override; void updt_params(params_ref const & p) override {} static void get_param_descrs(param_descrs & r) {} diff --git a/src/tactic/core/elim_term_ite_tactic.cpp b/src/tactic/core/elim_term_ite_tactic.cpp index c2d972b6230..42adf04a971 100644 --- a/src/tactic/core/elim_term_ite_tactic.cpp +++ b/src/tactic/core/elim_term_ite_tactic.cpp @@ -136,6 +136,8 @@ class elim_term_ite_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "elim_term_ite"; } + tactic * translate(ast_manager & m) override { return alloc(elim_term_ite_tactic, m, m_params); } diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index 4df4d1fc4d7..915a0f3c01e 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -853,6 +853,8 @@ class elim_uncnstr_tactic : public tactic { updt_params(p); } + char const* name() const override { return "elim_uncstr"; } + tactic * translate(ast_manager & m) override { return alloc(elim_uncnstr_tactic, m, m_params); } diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp index 82e78d771f6..485eda4dd0e 100644 --- a/src/tactic/core/injectivity_tactic.cpp +++ b/src/tactic/core/injectivity_tactic.cpp @@ -255,6 +255,8 @@ class injectivity_tactic : public tactic { dealloc(m_map); } + char const* name() const override { return "injectivity"; } + void updt_params(params_ref const & p) override { m_params = p; m_finder->updt_params(p); diff --git a/src/tactic/core/nnf_tactic.cpp b/src/tactic/core/nnf_tactic.cpp index 72ebb949d33..164cf93116b 100644 --- a/src/tactic/core/nnf_tactic.cpp +++ b/src/tactic/core/nnf_tactic.cpp @@ -49,6 +49,8 @@ class nnf_tactic : public tactic { ~nnf_tactic() override {} + char const* name() const override { return "nnf"; } + void updt_params(params_ref const & p) override { m_params = p; } void collect_param_descrs(param_descrs & r) override { nnf::get_param_descrs(r); } diff --git a/src/tactic/core/occf_tactic.cpp b/src/tactic/core/occf_tactic.cpp index b1f9d3f9347..c3c027fef1c 100644 --- a/src/tactic/core/occf_tactic.cpp +++ b/src/tactic/core/occf_tactic.cpp @@ -196,6 +196,8 @@ class occf_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "occf"; } + void updt_params(params_ref const & p) override {} void collect_param_descrs(param_descrs & r) override {} diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp index 1d4805c6761..ef3db804bb0 100644 --- a/src/tactic/core/pb_preprocess_tactic.cpp +++ b/src/tactic/core/pb_preprocess_tactic.cpp @@ -107,6 +107,8 @@ class pb_preprocess_tactic : public tactic { tactic * translate(ast_manager & m) override { return alloc(pb_preprocess_tactic, m); } + + char const* name() const override { return "pb_preprocess"; } void operator()( goal_ref const & g, diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp index 6cf340e571e..b735de4b708 100644 --- a/src/tactic/core/propagate_values_tactic.cpp +++ b/src/tactic/core/propagate_values_tactic.cpp @@ -216,6 +216,8 @@ class propagate_values_tactic : public tactic { return alloc(propagate_values_tactic, m, m_params); } + char const* name() const override { return "propagate_values"; } + void updt_params(params_ref const & p) override { m_params = p; m_r.updt_params(p); diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index 8a1833bb4f4..e0859392280 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -73,6 +73,8 @@ class reduce_args_tactic : public tactic { } ~reduce_args_tactic() override; + + char const* name() const override { return "reduce_args"; } void operator()(goal_ref const & g, goal_ref_buffer & result) override; void cleanup() override; @@ -86,15 +88,14 @@ tactic * mk_reduce_args_tactic(ast_manager & m, params_ref const & p) { struct reduce_args_tactic::imp { expr_ref_vector m_vars; - ast_manager & m_manager; + ast_manager & m; bv_util m_bv; array_util m_ar; - ast_manager & m() const { return m_manager; } imp(ast_manager & m): m_vars(m), - m_manager(m), + m(m), m_bv(m), m_ar(m) { } @@ -120,17 +121,17 @@ struct reduce_args_tactic::imp { } void checkpoint() { - tactic::checkpoint(m_manager); + tactic::checkpoint(m); } struct find_non_candidates_proc { - ast_manager & m_manager; + ast_manager & m; bv_util & m_bv; array_util & m_ar; obj_hashtable & m_non_candidates; find_non_candidates_proc(ast_manager & m, bv_util & bv, array_util& ar, obj_hashtable & non_candidates): - m_manager(m), + m(m), m_bv(bv), m_ar(ar), m_non_candidates(non_candidates) { @@ -156,7 +157,7 @@ struct reduce_args_tactic::imp { unsigned j = n->get_num_args(); while (j > 0) { --j; - if (may_be_unique(m_manager, m_bv, n->get_arg(j))) + if (may_be_unique(m, m_bv, n->get_arg(j))) return; } m_non_candidates.insert(d); @@ -172,7 +173,7 @@ struct reduce_args_tactic::imp { for (expr* v : m_vars) if (is_app(v)) non_candidates.insert(to_app(v)->get_decl()); - find_non_candidates_proc proc(m_manager, m_bv, m_ar, non_candidates); + find_non_candidates_proc proc(m, m_bv, m_ar, non_candidates); expr_fast_mark1 visited; unsigned sz = g.size(); for (unsigned i = 0; i < sz; i++) { @@ -187,14 +188,14 @@ struct reduce_args_tactic::imp { } struct populate_decl2args_proc { - ast_manager & m_manager; + ast_manager & m; bv_util & m_bv; obj_hashtable & m_non_candidates; obj_map & m_decl2args; obj_map > m_decl2base; // for args = base + offset populate_decl2args_proc(ast_manager & m, bv_util & bv, obj_hashtable & nc, obj_map & d): - m_manager(m), m_bv(bv), m_non_candidates(nc), m_decl2args(d) {} + m(m), m_bv(bv), m_non_candidates(nc), m_decl2args(d) {} void operator()(var * n) {} void operator()(quantifier * n) {} @@ -218,7 +219,7 @@ struct reduce_args_tactic::imp { it->m_value.reserve(j); while (j > 0) { --j; - it->m_value.set(j, may_be_unique(m_manager, m_bv, n->get_arg(j), base)); + it->m_value.set(j, may_be_unique(m, m_bv, n->get_arg(j), base)); bases[j] = base; } } else { @@ -226,7 +227,7 @@ struct reduce_args_tactic::imp { SASSERT(j == it->m_value.size()); while (j > 0) { --j; - it->m_value.set(j, it->m_value.get(j) && may_be_unique(m_manager, m_bv, n->get_arg(j), base) && bases[j] == base); + it->m_value.set(j, it->m_value.get(j) && may_be_unique(m, m_bv, n->get_arg(j), base) && bases[j] == base); } } } @@ -237,7 +238,7 @@ struct reduce_args_tactic::imp { obj_map & decl2args) { expr_fast_mark1 visited; decl2args.reset(); - populate_decl2args_proc proc(m_manager, m_bv, non_candidates, decl2args); + populate_decl2args_proc proc(m, m_bv, non_candidates, decl2args); unsigned sz = g.size(); for (unsigned i = 0; i < sz; i++) { checkpoint(); @@ -246,28 +247,24 @@ struct reduce_args_tactic::imp { // Remove all cases where the simplification is not applicable. ptr_buffer bad_decls; - obj_map::iterator it = decl2args.begin(); - obj_map::iterator end = decl2args.end(); - for (; it != end; it++) { + for (auto const& [k, v] : decl2args) { bool is_zero = true; - for (unsigned i = 0; i < it->m_value.size() && is_zero ; i++) { - if (it->m_value.get(i)) + for (unsigned i = 0; i < v.size() && is_zero; i++) { + if (v.get(i)) is_zero = false; } - if (is_zero) - bad_decls.push_back(it->m_key); + if (is_zero) + bad_decls.push_back(k); } - ptr_buffer::iterator it2 = bad_decls.begin(); - ptr_buffer::iterator end2 = bad_decls.end(); - for (; it2 != end2; ++it2) - decl2args.erase(*it2); + for (func_decl* a : bad_decls) + decl2args.erase(a); TRACE("reduce_args", tout << "decl2args:" << std::endl; - for (obj_map::iterator it = decl2args.begin() ; it != decl2args.end() ; it++) { - tout << it->m_key->get_name() << ": "; - for (unsigned i = 0 ; i < it->m_value.size() ; i++) - tout << (it->m_value.get(i) ? "1" : "0"); + for (auto const& [k, v] : decl2args) { + tout << k->get_name() << ": "; + for (auto b : v) + tout << (b ? "1" : "0"); tout << std::endl; }); } @@ -311,22 +308,17 @@ struct reduce_args_tactic::imp { typedef obj_map decl2arg2func_map; struct reduce_args_ctx { - ast_manager & m_manager; + ast_manager & m; decl2arg2func_map m_decl2arg2funcs; - reduce_args_ctx(ast_manager & m): m_manager(m) { + reduce_args_ctx(ast_manager & m): m(m) { } ~reduce_args_ctx() { - obj_map::iterator it = m_decl2arg2funcs.begin(); - obj_map::iterator end = m_decl2arg2funcs.end(); - for (; it != end; ++it) { - arg2func * map = it->m_value; - arg2func::iterator it2 = map->begin(); - arg2func::iterator end2 = map->end(); - for (; it2 != end2; ++it2) { - m_manager.dec_ref(it2->m_key); - m_manager.dec_ref(it2->m_value); + for (auto const& [_, map] : m_decl2arg2funcs) { + for (auto const& [k, v] : *map) { + m.dec_ref(k); + m.dec_ref(v); } dealloc(map); } @@ -340,7 +332,7 @@ struct reduce_args_tactic::imp { decl2arg2func_map & m_decl2arg2funcs; reduce_args_rw_cfg(imp & owner, obj_map & decl2args, decl2arg2func_map & decl2arg2funcs): - m(owner.m_manager), + m(owner.m), m_owner(owner), m_decl2args(decl2args), m_decl2arg2funcs(decl2arg2funcs) { @@ -396,16 +388,16 @@ struct reduce_args_tactic::imp { reduce_args_rw_cfg m_cfg; public: reduce_args_rw(imp & owner, obj_map & decl2args, decl2arg2func_map & decl2arg2funcs): - rewriter_tpl(owner.m_manager, false, m_cfg), + rewriter_tpl(owner.m, false, m_cfg), m_cfg(owner, decl2args, decl2arg2funcs) { } }; model_converter * mk_mc(obj_map & decl2args, decl2arg2func_map & decl2arg2funcs) { ptr_buffer new_args; - var_ref_vector new_vars(m_manager); + var_ref_vector new_vars(m); ptr_buffer new_eqs; - generic_model_converter * f_mc = alloc(generic_model_converter, m_manager, "reduce_args"); + generic_model_converter * f_mc = alloc(generic_model_converter, m, "reduce_args"); for (auto const& kv : decl2arg2funcs) { func_decl * f = kv.m_key; arg2func * map = kv.m_value; @@ -415,18 +407,14 @@ struct reduce_args_tactic::imp { new_vars.reset(); new_args.reset(); for (unsigned i = 0; i < f->get_arity(); i++) { - new_vars.push_back(m_manager.mk_var(i, f->get_domain(i))); + new_vars.push_back(m.mk_var(i, f->get_domain(i))); if (!bv.get(i)) new_args.push_back(new_vars.back()); } - arg2func::iterator it2 = map->begin(); - arg2func::iterator end2 = map->end(); - for (; it2 != end2; ++it2) { - app * t = it2->m_key; - func_decl * new_def = it2->m_value; + for (auto const& [t, new_def] : *map) { f_mc->hide(new_def); SASSERT(new_def->get_arity() == new_args.size()); - app * new_t = m_manager.mk_app(new_def, new_args.size(), new_args.data()); + app * new_t = m.mk_app(new_def, new_args.size(), new_args.data()); if (def == nullptr) { def = new_t; } @@ -434,15 +422,15 @@ struct reduce_args_tactic::imp { new_eqs.reset(); for (unsigned i = 0; i < f->get_arity(); i++) { if (bv.get(i)) - new_eqs.push_back(m_manager.mk_eq(new_vars.get(i), t->get_arg(i))); + new_eqs.push_back(m.mk_eq(new_vars.get(i), t->get_arg(i))); } SASSERT(new_eqs.size() > 0); expr * cond; if (new_eqs.size() == 1) cond = new_eqs[0]; else - cond = m_manager.mk_and(new_eqs.size(), new_eqs.data()); - def = m_manager.mk_ite(cond, new_t, def); + cond = m.mk_and(new_eqs.size(), new_eqs.data()); + def = m.mk_ite(cond, new_t, def); } } SASSERT(def); @@ -464,7 +452,7 @@ struct reduce_args_tactic::imp { if (decl2args.empty()) return; - reduce_args_ctx ctx(m_manager); + reduce_args_ctx ctx(m); reduce_args_rw rw(*this, decl2args, ctx.m_decl2arg2funcs); unsigned sz = g.size(); @@ -472,7 +460,7 @@ struct reduce_args_tactic::imp { if (g.inconsistent()) break; expr * f = g.form(i); - expr_ref new_f(m_manager); + expr_ref new_f(m); rw(f, new_f); g.update(i, new_f); } @@ -499,7 +487,7 @@ void reduce_args_tactic::operator()(goal_ref const & g, goal_ref_buffer & result) { fail_if_unsat_core_generation("reduce-args", g); result.reset(); - if (!m_imp->m().proofs_enabled()) { + if (!m_imp->m.proofs_enabled()) { m_imp->operator()(*(g.get())); } g->inc_depth(); @@ -507,7 +495,7 @@ void reduce_args_tactic::operator()(goal_ref const & g, } void reduce_args_tactic::cleanup() { - ast_manager & m = m_imp->m(); + ast_manager & m = m_imp->m; expr_ref_vector vars = m_imp->m_vars; m_imp->~imp(); m_imp = new (m_imp) imp(m); diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp index a60f20aab50..cfcc42482db 100644 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ b/src/tactic/core/reduce_invertible_tactic.cpp @@ -47,6 +47,8 @@ class reduce_invertible_tactic : public tactic { ~reduce_invertible_tactic() override { } + char const* name() const override { return "reduce_invertible"; } + tactic * translate(ast_manager & m) override { return alloc(reduce_invertible_tactic, m); } diff --git a/src/tactic/core/simplify_tactic.h b/src/tactic/core/simplify_tactic.h index 9fff3419076..fc262f99859 100644 --- a/src/tactic/core/simplify_tactic.h +++ b/src/tactic/core/simplify_tactic.h @@ -43,6 +43,8 @@ class simplify_tactic : public tactic { tactic * translate(ast_manager & m) override { return alloc(simplify_tactic, m, m_params); } + char const* name() const override { return "simplify"; } + }; tactic * mk_simplify_tactic(ast_manager & m, params_ref const & p = params_ref()); diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index b9feaf949f7..9d844b7ed8d 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -1089,6 +1089,8 @@ class solve_eqs_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "solve_eqs"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/core/special_relations_tactic.h b/src/tactic/core/special_relations_tactic.h index 6bb72852dae..a1cafb7c059 100644 --- a/src/tactic/core/special_relations_tactic.h +++ b/src/tactic/core/special_relations_tactic.h @@ -59,6 +59,8 @@ class special_relations_tactic : public tactic { tactic * translate(ast_manager & m) override { return alloc(special_relations_tactic, m, m_params); } + char const* name() const override { return "special_relations"; } + }; tactic * mk_special_relations_tactic(ast_manager & m, params_ref const & p = params_ref()); diff --git a/src/tactic/core/split_clause_tactic.cpp b/src/tactic/core/split_clause_tactic.cpp index 453e4a218da..12b76b63843 100644 --- a/src/tactic/core/split_clause_tactic.cpp +++ b/src/tactic/core/split_clause_tactic.cpp @@ -91,6 +91,8 @@ class split_clause_tactic : public tactic { ~split_clause_tactic() override { } + char const* name() const override { return "split_clause"; } + void updt_params(params_ref const & p) override { m_largest_clause = p.get_bool("split_largest_clause", false); } diff --git a/src/tactic/core/symmetry_reduce_tactic.cpp b/src/tactic/core/symmetry_reduce_tactic.cpp index 17049e2d18d..9aa4c944841 100644 --- a/src/tactic/core/symmetry_reduce_tactic.cpp +++ b/src/tactic/core/symmetry_reduce_tactic.cpp @@ -37,6 +37,8 @@ class symmetry_reduce_tactic : public tactic { } ~symmetry_reduce_tactic() override; + + char const* name() const override { return "symmetry_reduce"; } void operator()(goal_ref const & g, goal_ref_buffer & result) override; diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp index b466c50fb46..e26fded8f14 100644 --- a/src/tactic/core/tseitin_cnf_tactic.cpp +++ b/src/tactic/core/tseitin_cnf_tactic.cpp @@ -891,6 +891,8 @@ class tseitin_cnf_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "tseitin_cnf"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index 13cb4c3e74e..be98dea005f 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -120,6 +120,8 @@ class fpa2bv_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "fp2bv"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/portfolio/solver_subsumption_tactic.cpp b/src/tactic/portfolio/solver_subsumption_tactic.cpp index 3a23f598467..b2591f05c38 100644 --- a/src/tactic/portfolio/solver_subsumption_tactic.cpp +++ b/src/tactic/portfolio/solver_subsumption_tactic.cpp @@ -133,6 +133,8 @@ class solver_subsumption_tactic : public tactic { ~solver_subsumption_tactic() override {} + char const* name() const override { return "solver_subsumption"; } + void updt_params(params_ref const& p) override { m_params = p; unsigned max_conflicts = p.get_uint("max_conflicts", 2); diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index fd0dcaa3b1e..ece6940f3c9 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -50,6 +50,8 @@ class sls_tactic : public tactic { dealloc(m_engine); } + char const* name() const override { return "sls"; } + void updt_params(params_ref const & p) override { m_params = p; m_engine->updt_params(p); diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index ad9e8b46f4d..57c6ae99a17 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -53,6 +53,8 @@ class qfufbv_ackr_tactic : public tactic { ~qfufbv_ackr_tactic() override { } + char const* name() const override { return "qfufbv_ackr"; } + void operator()(goal_ref const & g, goal_ref_buffer & result) override { ast_manager& m(g->m()); tactic_report report("qfufbv_ackr", *g); diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index 66f58f71e46..5754359040f 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -90,6 +90,8 @@ class fail_tactic : public tactic { void cleanup() override {} + char const* name() const override { return "fail"; } + tactic * translate(ast_manager & m) override { return this; } }; diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index 891f44ef1d3..7f7f293af79 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -86,6 +86,7 @@ class tactic : public user_propagator::core { } unsigned user_propagate_register(expr* e) override { return 0; } + virtual char const* name() const = 0; protected: friend class nary_tactical; @@ -116,6 +117,7 @@ class skip_tactic : public tactic { void operator()(goal_ref const & in, goal_ref_buffer& result) override; void cleanup() override {} tactic * translate(ast_manager & m) override { return this; } + char const* name() const { return "skip"; } }; tactic * mk_skip_tactic(); diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index c6419d95fb5..19009aa4460 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -100,6 +100,8 @@ class and_then_tactical : public binary_tactical { public: and_then_tactical(tactic * t1, tactic * t2):binary_tactical(t1, t2) {} + char const* name() const override { return "and_then"; } + void operator()(goal_ref const & in, goal_ref_buffer& result) override { bool proofs_enabled = in->proofs_enabled(); @@ -313,6 +315,8 @@ class or_else_tactical : public nary_tactical { public: or_else_tactical(unsigned num, tactic * const * ts):nary_tactical(num, ts) { SASSERT(num > 0); } + char const* name() const override { return "or_else"; } + void operator()(goal_ref const & in, goal_ref_buffer& result) override { goal orig(*(in.get())); unsigned sz = m_ts.size(); @@ -414,6 +418,8 @@ class par_tactical : public or_else_tactical { error_code = 0; } + char const* name() const override { return "par"; } + void operator()(goal_ref const & in, goal_ref_buffer& result) override { bool use_seq; use_seq = false; @@ -550,6 +556,8 @@ class par_and_then_tactical : public and_then_tactical { public: par_and_then_tactical(tactic * t1, tactic * t2):and_then_tactical(t1, t2) {} + char const* name() const override { return "par_then"; } + void operator()(goal_ref const & in, goal_ref_buffer& result) override { bool use_seq; use_seq = false; @@ -915,6 +923,8 @@ class repeat_tactical : public unary_tactical { unary_tactical(t), m_max_depth(max_depth) { } + + char const* name() const override { return "repeat"; } void operator()(goal_ref const & in, goal_ref_buffer& result) override { operator()(0, in, result); @@ -935,6 +945,8 @@ class fail_if_branching_tactical : public unary_tactical { public: fail_if_branching_tactical(tactic * t, unsigned threshold):unary_tactical(t), m_threshold(threshold) {} + char const* name() const override { return "fail_if_branching"; } + void operator()(goal_ref const & in, goal_ref_buffer& result) override { m_t->operator()(in, result); if (result.size() > m_threshold) { @@ -957,6 +969,8 @@ class cleanup_tactical : public unary_tactical { public: cleanup_tactical(tactic * t):unary_tactical(t) {} + char const* name() const override { return "cleanup"; } + void operator()(goal_ref const & in, goal_ref_buffer& result) override { m_t->operator()(in, result); m_t->cleanup(); @@ -976,6 +990,8 @@ class try_for_tactical : public unary_tactical { unsigned m_timeout; public: try_for_tactical(tactic * t, unsigned ts):unary_tactical(t), m_timeout(ts) {} + + char const* name() const override { return "try_for"; } void operator()(goal_ref const & in, goal_ref_buffer& result) override { cancel_eh eh(in->m().limit()); @@ -1003,6 +1019,8 @@ class using_params_tactical : public unary_tactical { t->updt_params(p); } + char const* name() const override { return "using_params"; } + void updt_params(params_ref const & p) override { TRACE("using_params", tout << "before p: " << p << "\n"; @@ -1052,6 +1070,8 @@ class annotate_tactical : public unary_tactical { tactic * new_t = m_t->translate(m); return alloc(annotate_tactical, m_name.c_str(), new_t); } + + char const* name() const override { return "annotate"; } }; @@ -1067,6 +1087,8 @@ class cond_tactical : public binary_tactical { m_p(p) { SASSERT(m_p); } + + char const* name() const override { return "cond"; } void operator()(goal_ref const & in, goal_ref_buffer & result) override { if (m_p->operator()(*(in.get())).is_true()) @@ -1098,6 +1120,8 @@ class fail_if_tactic : public tactic { SASSERT(m_p); } + char const* name() const override { return "fail_if"; } + void cleanup() override {} void operator()(goal_ref const & in, goal_ref_buffer& result) override { @@ -1123,6 +1147,8 @@ tactic * fail_if_not(probe * p) { class if_no_proofs_tactical : public unary_tactical { public: if_no_proofs_tactical(tactic * t):unary_tactical(t) {} + + char const* name() const override { return "if_no_proofs"; } void operator()(goal_ref const & in, goal_ref_buffer & result) override { if (in->proofs_enabled()) { @@ -1139,6 +1165,8 @@ class if_no_proofs_tactical : public unary_tactical { class if_no_unsat_cores_tactical : public unary_tactical { public: if_no_unsat_cores_tactical(tactic * t):unary_tactical(t) {} + + char const* name() const override { return "if_no_unsat_cores"; } void operator()(goal_ref const & in, goal_ref_buffer& result) override { if (in->unsat_core_enabled()) { @@ -1155,6 +1183,8 @@ class if_no_unsat_cores_tactical : public unary_tactical { class if_no_models_tactical : public unary_tactical { public: if_no_models_tactical(tactic * t):unary_tactical(t) {} + + char const* name() const override { return "if_no_models"; } void operator()(goal_ref const & in, goal_ref_buffer& result) override { if (in->models_enabled()) { diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp index 86c60653816..c5745d85c62 100644 --- a/src/tactic/ufbv/macro_finder_tactic.cpp +++ b/src/tactic/ufbv/macro_finder_tactic.cpp @@ -105,6 +105,8 @@ class macro_finder_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "macro_finder"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp index 33c2927bb1a..0e0cb7cb2a7 100644 --- a/src/tactic/ufbv/quasi_macros_tactic.cpp +++ b/src/tactic/ufbv/quasi_macros_tactic.cpp @@ -100,6 +100,8 @@ class quasi_macros_tactic : public tactic { dealloc(m_imp); } + char const* name() const override { return "quasi_macros"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp index bb2b4d5be2d..d5bfec8fec2 100644 --- a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp +++ b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp @@ -28,6 +28,8 @@ class ufbv_rewriter_tactic : public tactic { ufbv_rewriter_tactic(ast_manager & m, params_ref const & p): m_manager(m), m_params(p) {} + char const* name() const override { return "ufbv"; } + tactic * translate(ast_manager & m) override { return alloc(ufbv_rewriter_tactic, m, m_params); }