Merge branch 'master' of https://github.com/z3prover/z3

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
+    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')
-    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_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))
+        fout.write('  ADD_TACTIC_CMD("%s", "%s", %s);\n' % data)
-        idx = idx + 1
     for data in ADD_PROBE_DATA:
         fout.write('  ADD_PROBE("%s", "%s", %s);\n' % data)
     fout.write('}\n')

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));
         }
     }
 

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);
     }

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),

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;
+    symbol         m_name;
-    char const *     m_descr;
+    char const *   m_descr;
-    tactic_factory * m_factory;
+    tactic_factory m_factory;
 public:
-    tactic_cmd(symbol const & n, char const * d, tactic_factory * f):
+    tactic_cmd(symbol const & n, char const * d, tactic_factory f):
-        m_name(n), m_descr(d), m_factory(f) {
+        m_name(n), m_descr(d), m_factory(f) {}
-        SASSERT(m_factory);
-    }
-
-    ~tactic_cmd();
 
     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);

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());
                 }
             }
 

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)")
 */

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);
             }
         }
 

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("search failed");
-                throw tactic_exception(s.c_str()); 
             }        
         }
 

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;
         }

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) {

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_ctx->last_failure_as_string());
-                throw tactic_exception(m_failure.c_str());
             }
         }
         catch (rewriter_exception & ex) {

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()) {

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<tactic> m_tactic;
 public:
@@ -284,24 +289,23 @@ public:
 };
 
 class tactic_factory2solver_factory : public solver_factory {
-    scoped_ptr<tactic_factory> 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);
 }
 

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

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());
         }
     };
 

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));
     }
 }

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);
 

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(); }
 };

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));
                 }
             }
 

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 && msg):default_exception(std::move(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, 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): 

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));
     }
 };
 

src/util/lp/lp_utils.h

@@ -36,8 +36,8 @@ bool contains(const std::unordered_map<A, B> & map, const A& key) {
 }
 
 namespace lp {
-    inline void throw_exception(const std::string & str) {
+    inline void throw_exception(std::string && str) {
-        throw default_exception(str);
+        throw default_exception(std::move(str));
     }
     typedef z3_exception exception;
 

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;
+static scoped_timer * g_timeout = nullptr;
-void (* g_on_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) 

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(); 
 }

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;