add tactic name

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Dec 7, 2021 · 9f2b18c · 9f2b18c
1 parent e3bd5ba
commit 9f2b18c
Show file tree

Hide file tree

Showing 73 changed files with 218 additions and 63 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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); }