diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 2e0bbe2ca..7fa6d4041 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -718,17 +718,11 @@ def mk_install_tactic_cpp_internal(h_files_full_path, path): fullname, line)) raise e # First pass will just generate the tactic factories - idx = 0 - for data in ADD_TACTIC_DATA: - fout.write('MK_SIMPLE_TACTIC_FACTORY(__Z3_local_factory_%s, %s);\n' % (idx, data[2])) - idx = idx + 1 - fout.write('#define ADD_TACTIC_CMD(NAME, DESCR, FACTORY) ctx.insert(alloc(tactic_cmd, symbol(NAME), DESCR, alloc(FACTORY)))\n') + fout.write('#define ADD_TACTIC_CMD(NAME, DESCR, CODE) ctx.insert(alloc(tactic_cmd, symbol(NAME), DESCR, [](ast_manager &m, const params_ref &p) { return CODE; }))\n') fout.write('#define ADD_PROBE(NAME, DESCR, PROBE) ctx.insert(alloc(probe_info, symbol(NAME), DESCR, PROBE))\n') fout.write('void install_tactics(tactic_manager & ctx) {\n') - idx = 0 for data in ADD_TACTIC_DATA: - fout.write(' ADD_TACTIC_CMD("%s", "%s", __Z3_local_factory_%s);\n' % (data[0], data[1], idx)) - idx = idx + 1 + fout.write(' ADD_TACTIC_CMD("%s", "%s", %s);\n' % data) for data in ADD_PROBE_DATA: fout.write(' ADD_PROBE("%s", "%s", %s);\n' % data) fout.write('}\n') diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 846fb1ded..e65eb1b32 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -59,7 +59,7 @@ public: if (c == nullptr) { std::string err_msg("unknown command '"); err_msg = err_msg + s.bare_str() + "'"; - throw cmd_exception(err_msg); + throw cmd_exception(std::move(err_msg)); } m_cmds.push_back(s); } @@ -384,7 +384,7 @@ class set_option_cmd : public set_get_option_cmd { std::string msg = "error setting '"; msg += opt_name.str(); msg += "', option value cannot be modified after initialization"; - throw cmd_exception(msg); + throw cmd_exception(std::move(msg)); } } diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 0b4c5cd3d..585dd0fa6 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -369,7 +369,7 @@ void stream_ref::set(char const * name) { std::string msg = "failed to set output stream '"; msg += name; msg += "'"; - throw cmd_exception(msg); + throw cmd_exception(std::move(msg)); } SASSERT(m_stream); } diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index cbe44da2d..cf0fd5111 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -32,14 +32,6 @@ Notes: #include "cmd_context/cmd_context_to_goal.h" #include "cmd_context/echo_tactic.h" -tactic_cmd::~tactic_cmd() { - dealloc(m_factory); -} - -tactic * tactic_cmd::mk(ast_manager & m) { - return (*m_factory)(m, params_ref()); -} - probe_info::probe_info(symbol const & n, char const * d, probe * p): m_name(n), m_descr(d), diff --git a/src/cmd_context/tactic_cmds.h b/src/cmd_context/tactic_cmds.h index fc15c795b..691771509 100644 --- a/src/cmd_context/tactic_cmds.h +++ b/src/cmd_context/tactic_cmds.h @@ -19,30 +19,28 @@ Notes: #define TACTIC_CMDS_H_ #include "ast/ast.h" +#include "util/params.h" #include "util/cmd_context_types.h" #include "util/ref.h" class tactic; class probe; -class tactic_factory; + +typedef tactic* (*tactic_factory)(ast_manager&, const params_ref&); class tactic_cmd { - symbol m_name; - char const * m_descr; - tactic_factory * m_factory; + symbol m_name; + char const * m_descr; + tactic_factory m_factory; public: - tactic_cmd(symbol const & n, char const * d, tactic_factory * f): - m_name(n), m_descr(d), m_factory(f) { - SASSERT(m_factory); - } - - ~tactic_cmd(); + tactic_cmd(symbol const & n, char const * d, tactic_factory f): + m_name(n), m_descr(d), m_factory(f) {} symbol get_name() const { return m_name; } char const * get_descr() const { return m_descr; } - tactic * mk(ast_manager & m); + tactic * mk(ast_manager & m) { return m_factory(m, params_ref()); } }; void install_core_tactic_cmds(cmd_context & ctx); diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp index eef95915d..65be3e9ae 100644 --- a/src/muz/fp/horn_tactic.cpp +++ b/src/muz/fp/horn_tactic.cpp @@ -211,7 +211,7 @@ class horn_tactic : public tactic { default: msg << "formula is not in Horn fragment: " << mk_pp(g->form(i), m) << "\n"; TRACE("horn", tout << msg.str();); - throw tactic_exception(msg.str().c_str()); + throw tactic_exception(msg.str()); } } diff --git a/src/nlsat/tactic/qfnra_nlsat_tactic.h b/src/nlsat/tactic/qfnra_nlsat_tactic.h index b1a4d8392..29dbadb9e 100644 --- a/src/nlsat/tactic/qfnra_nlsat_tactic.h +++ b/src/nlsat/tactic/qfnra_nlsat_tactic.h @@ -25,8 +25,6 @@ class tactic; tactic * mk_qfnra_nlsat_tactic(ast_manager & m, params_ref const & p = params_ref()); -MK_SIMPLE_TACTIC_FACTORY(qfnra_nlsat_fct, mk_qfnra_nlsat_tactic(m, p)); - /* ADD_TACTIC("qfnra-nlsat", "builtin strategy for solving QF_NRA problems using only nlsat.", "mk_qfnra_nlsat_tactic(m, p)") */ diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 79ad717c0..403ea4c85 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -909,7 +909,7 @@ namespace smt2 { std::string err_msg = "invalid datatype declaration, unknown sort '"; err_msg += missing.str(); err_msg += "'"; - throw parser_exception(err_msg, line, pos); + throw parser_exception(std::move(err_msg), line, pos); } dts->commit(pm()); m_ctx.insert_aux_pdecl(dts.get()); @@ -989,7 +989,7 @@ namespace smt2 { std::string err_msg = "invalid datatype declaration, unknown sort '"; err_msg += missing.str(); err_msg += "'"; - throw parser_exception(err_msg, line, pos); + throw parser_exception(std::move(err_msg), line, pos); } } @@ -999,7 +999,7 @@ namespace smt2 { std::string err_msg = "invalid datatype declaration, repeated accessor identifier '"; err_msg += duplicated.str(); err_msg += "'"; - throw parser_exception(err_msg, line, pos); + throw parser_exception(std::move(err_msg), line, pos); } } diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index 1ae9723c9..695bac07d 100644 --- a/src/qe/nlqsat.cpp +++ b/src/qe/nlqsat.cpp @@ -844,8 +844,7 @@ namespace qe { break; case l_undef: result.push_back(in.get()); - std::string s = "search failed"; - throw tactic_exception(s.c_str()); + throw tactic_exception("search failed"); } } diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 68fd56cdf..c87b1c2eb 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -1279,7 +1279,7 @@ namespace qe { if (s == "ok" || s == "unknown") { s = m_fa.s().reason_unknown(); } - throw tactic_exception(s.c_str()); + throw tactic_exception(std::move(s)); } } @@ -1344,7 +1344,7 @@ namespace qe { s = m_fa.s().reason_unknown(); } - throw tactic_exception(s.c_str()); + throw tactic_exception(std::move(s)); } return l_true; } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 5f0fbec16..029ddf924 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -92,7 +92,7 @@ struct goal2sat::imp { void throw_op_not_handled(std::string const& s) { std::string s0 = "operator " + s + " not supported, apply simplifier before invoking translator"; - throw tactic_exception(s0.c_str()); + throw tactic_exception(std::move(s0)); } void mk_clause(sat::literal l) { diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index cc0f0f207..50fe47985 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -39,7 +39,6 @@ class smt_tactic : public tactic { smt_params m_params; params_ref m_params_ref; statistics m_stats; - std::string m_failure; smt::kernel * m_ctx; symbol m_logic; progress_callback * m_callback; @@ -259,7 +258,7 @@ public: if (m_fail_if_inconclusive && !m_candidate_models) { std::stringstream strm; strm << "smt tactic failed to show goal to be sat/unsat " << m_ctx->last_failure_as_string(); - throw tactic_exception(strm.str().c_str()); + throw tactic_exception(strm.str()); } result.push_back(in.get()); if (m_candidate_models) { @@ -281,8 +280,7 @@ public: break; } } - m_failure = m_ctx->last_failure_as_string(); - throw tactic_exception(m_failure.c_str()); + throw tactic_exception(m_ctx->last_failure_as_string()); } } catch (rewriter_exception & ex) { diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp index 451a62064..142ba4bb8 100644 --- a/src/solver/parallel_tactic.cpp +++ b/src/solver/parallel_tactic.cpp @@ -635,7 +635,7 @@ private: t.join(); m_manager.limit().reset_cancel(); if (m_exn_code == -1) - throw default_exception(m_exn_msg); + throw default_exception(std::move(m_exn_msg)); if (m_exn_code != 0) throw z3_error(m_exn_code); if (!m_models.empty()) { diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 94509e3f6..135d402e6 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -19,6 +19,7 @@ Author: Notes: --*/ +#include "solver/tactic2solver.h" #include "solver/solver_na2as.h" #include "tactic/tactic.h" #include "ast/ast_translation.h" @@ -31,6 +32,8 @@ Notes: option for applications trying to solve many easy queries that a similar to each other. */ + +namespace { class tactic2solver : public solver_na2as { expr_ref_vector m_assertions; unsigned_vector m_scopes; @@ -258,6 +261,7 @@ unsigned tactic2solver::get_num_assertions() const { expr * tactic2solver::get_assertion(unsigned idx) const { return m_assertions.get(idx); } +} solver * mk_tactic2solver(ast_manager & m, @@ -270,6 +274,7 @@ solver * mk_tactic2solver(ast_manager & m, return alloc(tactic2solver, m, t, p, produce_proofs, produce_models, produce_unsat_cores, logic); } +namespace { class tactic2solver_factory : public solver_factory { ref m_tactic; public: @@ -284,24 +289,23 @@ public: }; class tactic_factory2solver_factory : public solver_factory { - scoped_ptr m_factory; + tactic_factory m_factory; public: - tactic_factory2solver_factory(tactic_factory * f):m_factory(f) { + tactic_factory2solver_factory(tactic_factory f):m_factory(f) { } - ~tactic_factory2solver_factory() override {} - solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) override { tactic * t = (*m_factory)(m, p); return mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, logic); } }; +} solver_factory * mk_tactic2solver_factory(tactic * t) { return alloc(tactic2solver_factory, t); } -solver_factory * mk_tactic_factory2solver_factory(tactic_factory * f) { +solver_factory * mk_tactic_factory2solver_factory(tactic_factory f) { return alloc(tactic_factory2solver_factory, f); } diff --git a/src/solver/tactic2solver.h b/src/solver/tactic2solver.h index ddab66dc5..d9fffba24 100644 --- a/src/solver/tactic2solver.h +++ b/src/solver/tactic2solver.h @@ -23,12 +23,14 @@ Notes: #define TACTIC2SOLVER_H_ #include "util/params.h" + class ast_manager; class tactic; -class tactic_factory; class solver; class solver_factory; +typedef tactic* (*tactic_factory)(ast_manager&, const params_ref&); + solver * mk_tactic2solver(ast_manager & m, tactic * t = nullptr, params_ref const & p = params_ref(), @@ -39,6 +41,6 @@ solver * mk_tactic2solver(ast_manager & m, solver_factory * mk_tactic2solver_factory(tactic * t); -solver_factory * mk_tactic_factory2solver_factory(tactic_factory * f); +solver_factory * mk_tactic_factory2solver_factory(tactic_factory f); #endif diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index 836808de1..f36e3a6db 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -968,7 +968,7 @@ private: void throw_tactic(expr* e) { std::stringstream strm; strm << "goal is in a fragment unsupported by pb2bv. Offending expression: " << mk_pp(e, m); - throw tactic_exception(strm.str().c_str()); + throw tactic_exception(strm.str()); } }; diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index 4fa9ca43f..3b3c2444f 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -206,7 +206,7 @@ void fail_if_proof_generation(char const * tactic_name, goal_ref const & in) { if (in->proofs_enabled()) { std::string msg = tactic_name; msg += " does not support proof production"; - throw tactic_exception(msg.c_str()); + throw tactic_exception(std::move(msg)); } } @@ -214,7 +214,7 @@ void fail_if_unsat_core_generation(char const * tactic_name, goal_ref const & in if (in->unsat_core_enabled()) { std::string msg = tactic_name; msg += " does not support unsat core production"; - throw tactic_exception(msg.c_str()); + throw tactic_exception(std::move(msg)); } } @@ -222,6 +222,6 @@ void fail_if_model_generation(char const * tactic_name, goal_ref const & in) { if (in->models_enabled()) { std::string msg = tactic_name; msg += " does not generate models"; - throw tactic_exception(msg.c_str()); + throw tactic_exception(std::move(msg)); } } diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index c9b5a23fd..92cc7315f 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -119,21 +119,6 @@ tactic * mk_fail_if_undecided_tactic(); tactic * mk_report_verbose_tactic(char const * msg, unsigned lvl); tactic * mk_trace_tactic(char const * tag); -class tactic_factory { -public: - virtual ~tactic_factory() {} - virtual tactic * operator()(ast_manager & m, params_ref const & p) = 0; -}; - -#define MK_TACTIC_FACTORY(NAME, CODE) \ -class NAME : public tactic_factory { \ -public: \ - virtual ~NAME() {} \ - virtual tactic * operator()(ast_manager & m, params_ref const & p) { CODE } \ -}; - -#define MK_SIMPLE_TACTIC_FACTORY(NAME, ST) MK_TACTIC_FACTORY(NAME, return ST;) - void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result); lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown); diff --git a/src/tactic/tactic_exception.h b/src/tactic/tactic_exception.h index bdf2636a9..0af6d66b1 100644 --- a/src/tactic/tactic_exception.h +++ b/src/tactic/tactic_exception.h @@ -26,7 +26,7 @@ class tactic_exception : public z3_exception { protected: std::string m_msg; public: - tactic_exception(char const * msg):m_msg(msg) {} + tactic_exception(std::string && msg) : m_msg(std::move(msg)) {} ~tactic_exception() override {} char const * msg() const override { return m_msg.c_str(); } }; diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index bb04a2be7..43087f50f 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -463,9 +463,9 @@ public: if (finished_id == UINT_MAX) { switch (ex_kind) { case ERROR_EX: throw z3_error(error_code); - case TACTIC_EX: throw tactic_exception(ex_msg.c_str()); + case TACTIC_EX: throw tactic_exception(std::move(ex_msg)); default: - throw default_exception(ex_msg.c_str()); + throw default_exception(std::move(ex_msg)); } } } @@ -660,9 +660,9 @@ public: if (failed) { switch (ex_kind) { case ERROR_EX: throw z3_error(error_code); - case TACTIC_EX: throw tactic_exception(ex_msg.c_str()); + case TACTIC_EX: throw tactic_exception(std::move(ex_msg)); default: - throw default_exception(ex_msg.c_str()); + throw default_exception(std::move(ex_msg)); } } diff --git a/src/util/cmd_context_types.h b/src/util/cmd_context_types.h index e82536704..564ae6325 100644 --- a/src/util/cmd_context_types.h +++ b/src/util/cmd_context_types.h @@ -55,8 +55,8 @@ class cmd_exception : public default_exception { } public: cmd_exception(char const * msg):default_exception(msg), m_line(-1), m_pos(-1) {} - cmd_exception(std::string const & msg):default_exception(msg), m_line(-1), m_pos(-1) {} - cmd_exception(std::string const & msg, int line, int pos):default_exception(msg), m_line(line), m_pos(pos) {} + cmd_exception(std::string && msg):default_exception(std::move(msg)), m_line(-1), m_pos(-1) {} + cmd_exception(std::string && msg, int line, int pos):default_exception(std::move(msg)), m_line(line), m_pos(pos) {} cmd_exception(char const * msg, symbol const & s): default_exception(compose(msg,s)),m_line(-1),m_pos(-1) {} cmd_exception(char const * msg, symbol const & s, int line, int pos): diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 5ee49ef16..4ba3b3b5c 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -356,7 +356,7 @@ public: } } if (error) - throw exception(error_msg); + throw exception(std::move(error_msg)); } std::string get_value(params_ref const & ps, symbol const & p) { @@ -417,7 +417,7 @@ public: } } if (error) - throw exception(error_msg); + throw exception(std::move(error_msg)); return r; } @@ -509,7 +509,7 @@ public: } } if (error) - throw exception(error_msg); + throw exception(std::move(error_msg)); } void display_parameter(std::ostream & out, char const * name) { @@ -550,7 +550,7 @@ public: } } if (error) - throw exception(error_msg); + throw exception(std::move(error_msg)); } }; diff --git a/src/util/lp/lp_utils.h b/src/util/lp/lp_utils.h index fce9f4d02..3a5dd2a22 100644 --- a/src/util/lp/lp_utils.h +++ b/src/util/lp/lp_utils.h @@ -36,8 +36,8 @@ bool contains(const std::unordered_map & map, const A& key) { } namespace lp { - inline void throw_exception(const std::string & str) { - throw default_exception(str); + inline void throw_exception(std::string && str) { + throw default_exception(std::move(str)); } typedef z3_exception exception; diff --git a/src/util/timeout.cpp b/src/util/timeout.cpp index 283b4c206..ad02a747d 100644 --- a/src/util/timeout.cpp +++ b/src/util/timeout.cpp @@ -27,9 +27,10 @@ Revision History: #include "util/event_handler.h" #include "util/scoped_timer.h" -scoped_timer * g_timeout = nullptr; -void (* g_on_timeout)() = nullptr; +static scoped_timer * g_timeout = nullptr; +static void (* g_on_timeout)() = nullptr; +namespace { class g_timeout_eh : public event_handler { public: void operator()(event_handler_caller_t caller_id) override { @@ -46,6 +47,7 @@ public: } } }; +} void set_timeout(long ms) { if (g_timeout) diff --git a/src/util/z3_exception.cpp b/src/util/z3_exception.cpp index d028a688a..585313024 100644 --- a/src/util/z3_exception.cpp +++ b/src/util/z3_exception.cpp @@ -67,9 +67,6 @@ default_exception::default_exception(fmt, char const* msg, ...) { m_msg = out.str(); } -default_exception::default_exception(std::string const & msg): m_msg(msg) { -} - char const * default_exception::msg() const { return m_msg.c_str(); } diff --git a/src/util/z3_exception.h b/src/util/z3_exception.h index e3260e89d..b5c1bf55d 100644 --- a/src/util/z3_exception.h +++ b/src/util/z3_exception.h @@ -41,7 +41,7 @@ class default_exception : public z3_exception { std::string m_msg; public: struct fmt {}; - default_exception(std::string const& msg); + default_exception(std::string && msg) : m_msg(std::move(msg)) {} default_exception(fmt, char const* msg, ...); ~default_exception() override {} char const * msg() const override;