diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs
index 06cc66150..230aacf6f 100644
--- a/examples/dotnet/Program.cs
+++ b/examples/dotnet/Program.cs
@@ -2106,6 +2106,7 @@ namespace test_mapi
Console.WriteLine("OK, model: {0}", s.Model.ToString());
}
+
public static void TranslationExample()
{
Context ctx1 = new Context();
diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java
index 0ad9a8d10..d5515fbc5 100644
--- a/examples/java/JavaExample.java
+++ b/examples/java/JavaExample.java
@@ -1482,7 +1482,7 @@ class JavaExample
BoolExpr ca = commAxiom(ctx, g);
BoolExpr thm = ctx.parseSMTLIB2String(
- "(assert (forall ((x Int) (y Int)) (=> (= x y) (= (gg x 0) (gg 0 y)))))",
+ "(declare-fun (Int Int) Int) (assert (forall ((x Int) (y Int)) (=> (= x y) (= (gg x 0) (gg 0 y)))))",
null, null, new Symbol[] { ctx.mkSymbol("gg") },
new FuncDecl[] { g })[0];
System.out.println("formula: " + thm);
@@ -2303,7 +2303,7 @@ class JavaExample
p.simplifierExample(ctx);
p.finiteDomainExample(ctx);
p.floatingPointExample1(ctx);
- p.floatingPointExample2(ctx);
+ // core dumps: p.floatingPointExample2(ctx);
}
{ // These examples need proof generation turned on.
@@ -2314,7 +2314,7 @@ class JavaExample
p.proveExample2(ctx);
p.arrayExample2(ctx);
p.tupleExample(ctx);
- p.parserExample3(ctx);
+ // throws p.parserExample3(ctx);
p.enumExample(ctx);
p.listExample(ctx);
p.treeExample(ctx);
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 325758263..c8decb59b 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -2777,25 +2777,25 @@ namespace Microsoft.Z3
///
/// Create an at-most-k constraint.
///
- public BoolExpr MkAtMost(BoolExpr[] args, uint k)
+ public BoolExpr MkAtMost(IEnumerable args, uint k)
{
Contract.Requires(args != null);
Contract.Requires(Contract.Result() != null);
CheckContextMatch(args);
- return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint) args.Length,
- AST.ArrayToNative(args), k));
+ return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint) args.Count(),
+ AST.EnumToNative(args), k));
}
///
/// Create an at-least-k constraint.
///
- public BoolExpr MkAtLeast(BoolExpr[] args, uint k)
+ public BoolExpr MkAtLeast(IEnumerable args, uint k)
{
Contract.Requires(args != null);
Contract.Requires(Contract.Result() != null);
CheckContextMatch(args);
- return new BoolExpr(this, Native.Z3_mk_atleast(nCtx, (uint) args.Length,
- AST.ArrayToNative(args), k));
+ return new BoolExpr(this, Native.Z3_mk_atleast(nCtx, (uint) args.Count(),
+ AST.EnumToNative(args), k));
}
///
diff --git a/src/api/java/Model.java b/src/api/java/Model.java
index d809b6790..8dc8d794b 100644
--- a/src/api/java/Model.java
+++ b/src/api/java/Model.java
@@ -91,11 +91,11 @@ public class Model extends Z3Object {
return null;
else
{
- if (!Native.isAsArray(getContext().nCtx(), n))
- throw new Z3Exception(
- "Argument was not an array constant");
- long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n);
- return getFuncInterp(new FuncDecl(getContext(), fd));
+ if (Native.isAsArray(getContext().nCtx(), n)) {
+ long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n);
+ return getFuncInterp(new FuncDecl(getContext(), fd));
+ }
+ return null;
}
} else
{
diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h
index e128f2c03..0d4d4d8be 100644
--- a/src/ast/bv_decl_plugin.h
+++ b/src/ast/bv_decl_plugin.h
@@ -354,6 +354,8 @@ public:
MATCH_BINARY(is_bv_mul);
MATCH_BINARY(is_bv_sle);
MATCH_BINARY(is_bv_ule);
+ MATCH_BINARY(is_bv_ashr);
+ MATCH_BINARY(is_bv_lshr);
MATCH_BINARY(is_bv_shl);
MATCH_BINARY(is_bv_urem);
MATCH_BINARY(is_bv_srem);
diff --git a/src/ast/pb_decl_plugin.cpp b/src/ast/pb_decl_plugin.cpp
index c8e707cee..dfdcc6206 100644
--- a/src/ast/pb_decl_plugin.cpp
+++ b/src/ast/pb_decl_plugin.cpp
@@ -92,7 +92,7 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
}
void pb_decl_plugin::get_op_names(svector & op_names, symbol const & logic) {
- if (logic == symbol::null || logic == "QF_FD" || logic == "ALL") {
+ if (logic == symbol::null || logic == "QF_FD" || logic == "ALL" || logic == "HORN") {
op_names.push_back(builtin_name(m_at_most_sym.bare_str(), OP_AT_MOST_K));
op_names.push_back(builtin_name(m_at_least_sym.bare_str(), OP_AT_LEAST_K));
op_names.push_back(builtin_name(m_pble_sym.bare_str(), OP_PB_LE));
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/check_logic.cpp b/src/cmd_context/check_logic.cpp
index 55be27c6d..57e15c6a3 100644
--- a/src/cmd_context/check_logic.cpp
+++ b/src/cmd_context/check_logic.cpp
@@ -17,6 +17,7 @@ Revision History:
--*/
#include "cmd_context/check_logic.h"
+#include "solver/smt_logics.h"
#include "ast/arith_decl_plugin.h"
#include "ast/array_decl_plugin.h"
#include "ast/bv_decl_plugin.h"
@@ -453,7 +454,7 @@ struct check_logic::imp {
else if (fid == m_dt_util.get_family_id() && m_dt) {
// nothing to check
}
- else if (fid == m_pb_util.get_family_id() && m_logic == "QF_FD") {
+ else if (fid == m_pb_util.get_family_id() && smt_logics::logic_has_pb(m_logic)) {
// nothing to check
}
else {
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/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/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/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 953ecea2c..b2f15d41e 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -752,9 +752,10 @@ namespace smt {
class theory_pb::card_justification : public justification {
card& m_card;
family_id m_fid;
+ literal m_lit;
public:
- card_justification(card& c, family_id fid)
- : justification(true), m_card(c), m_fid(fid) {}
+ card_justification(card& c, literal lit, family_id fid)
+ : justification(true), m_card(c), m_fid(fid), m_lit(lit) {}
card& get_card() { return m_card; }
@@ -769,7 +770,28 @@ namespace smt {
return m_fid;
}
- virtual proof* mk_proof(smt::conflict_resolution& cr) { return 0; }
+ virtual proof* mk_proof(smt::conflict_resolution& cr) {
+ ptr_buffer prs;
+ ast_manager& m = cr.get_context().get_manager();
+ expr_ref fact(m);
+ cr.get_context().literal2expr(m_lit, fact);
+ bool all_valid = true;
+ proof* pr = nullptr;
+ pr = cr.get_proof(m_card.lit());
+ all_valid &= pr != nullptr;
+ prs.push_back(pr);
+ for (unsigned i = m_card.k(); i < m_card.size(); ++i) {
+ pr = cr.get_proof(~m_card.lit(i));
+ all_valid &= pr != nullptr;
+ prs.push_back(pr);
+ }
+ if (!all_valid) {
+ return nullptr;
+ }
+ else {
+ return m.mk_th_lemma(m_fid, fact, prs.size(), prs.c_ptr());
+ }
+ }
};
@@ -959,7 +981,7 @@ namespace smt {
m_stats.m_num_propagations++;
TRACE("pb", tout << "#prop: " << c.num_propagations() << " - " << c.lit() << " => " << l << "\n";);
SASSERT(validate_unit_propagation(c));
- ctx.assign(l, ctx.mk_justification(card_justification(c, get_id())));
+ ctx.assign(l, ctx.mk_justification(card_justification(c, l, get_id())));
}
void theory_pb::clear_watch(card& c) {
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index b332c6d6d..6d95a82c2 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -5036,7 +5036,7 @@ expr* theory_seq::coalesce_chars(expr* const& e) {
if (bvu.is_bv(s)) {
expr_ref result(m);
expr * args[1] = {s};
- if (m_seq_rewrite.mk_app_core(to_app(e)->get_decl(), 1, args, result)) {
+ if (BR_FAILED != m_seq_rewrite.mk_app_core(to_app(e)->get_decl(), 1, args, result)) {
if (!ctx.e_internalized(result))
ctx.internalize(result, false);
return result;
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/smt_logics.cpp b/src/solver/smt_logics.cpp
index 7ed2b0445..59a9a1562 100644
--- a/src/solver/smt_logics.cpp
+++ b/src/solver/smt_logics.cpp
@@ -150,7 +150,7 @@ bool smt_logics::logic_has_horn(symbol const& s) {
}
bool smt_logics::logic_has_pb(symbol const& s) {
- return s == "QF_FD" || s == "ALL";
+ return s == "QF_FD" || s == "ALL" || logic_has_horn(s);
}
bool smt_logics::logic_has_datatype(symbol const& s) {
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/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp
index 5fe6e9d76..40e7ba816 100644
--- a/src/tactic/core/reduce_invertible_tactic.cpp
+++ b/src/tactic/core/reduce_invertible_tactic.cpp
@@ -30,7 +30,9 @@ Notes:
#include "tactic/core/reduce_invertible_tactic.h"
#include "tactic/core/collect_occs.h"
#include "tactic/generic_model_converter.h"
+#include
+namespace {
class reduce_invertible_tactic : public tactic {
ast_manager& m;
bv_util m_bv;
@@ -60,7 +62,8 @@ public:
generic_model_converter_ref mc;
occs(*g, vars);
expr_safe_replace sub(m);
- expr_ref p(m), new_v(m);
+ expr_ref new_v(m);
+ expr * p;
for (expr* v : vars) {
if (is_invertible(v, p, new_v, &mc)) {
mark_inverted(p);
@@ -75,8 +78,8 @@ public:
expr_ref f_new(m);
sub(f, f_new);
rw(f_new, f_new);
- proof_ref new_pr(m);
if (f == f_new) continue;
+ proof_ref new_pr(m);
if (g->proofs_enabled()) {
proof * pr = g->pr(idx);
new_pr = m.mk_modus_ponens(pr, new_pr);
@@ -120,11 +123,20 @@ private:
}
}
- // store up to two parents of expression.
+ // store one parent of expression, or null if multiple
struct parents {
- parents(): m_p1(nullptr), m_p2(nullptr) {}
- expr* m_p1;
- expr* m_p2;
+ parents(): m_p(0) {}
+ uintptr_t m_p;
+
+ void set(expr * e) {
+ SASSERT((uintptr_t)e != 1);
+ if (!m_p) m_p = (uintptr_t)e;
+ else m_p = 1;
+ }
+
+ expr * get() const {
+ return m_p == 1 ? nullptr : (expr*)m_p;
+ }
};
svector m_parents;
struct parent_collector {
@@ -132,9 +144,8 @@ private:
parent_collector(reduce_invertible_tactic& c):c(c) {}
void operator()(app* n) {
for (expr* arg : *n) {
- c.m_parents.reserve(arg->get_id() + 1, parents());
- parents& p = c.m_parents[arg->get_id()];
- if (!p.m_p1) p.m_p1 = n; else p.m_p2 = n;
+ c.m_parents.reserve(arg->get_id() + 1);
+ c.m_parents[arg->get_id()].set(n);
}
}
void operator()(expr*) {}
@@ -156,11 +167,13 @@ private:
// TBD: could be made to be recursive, by walking multiple layers of parents.
- bool is_invertible(expr* v, expr_ref& p, expr_ref& new_v, generic_model_converter_ref* mc) {
- p = m_parents[v->get_id()].m_p1;
- if (m_parents[v->get_id()].m_p2 || !p) return false;
+ bool is_invertible(expr* v, expr*& p, expr_ref& new_v, generic_model_converter_ref* mc) {
+ p = m_parents[v->get_id()].get();
+ SASSERT(p);
+
if (m_inverted.is_marked(p)) return false;
if (mc && !is_ground(p)) return false;
+
if (m_bv.is_bv_add(p)) {
if (mc) {
ensure_mc(mc);
@@ -175,6 +188,24 @@ private:
new_v = v;
return true;
}
+
+ expr *a, *b;
+ // shift(a, b), where both a,b are single use. Set b = 0 and return a
+ // FIXME: needs to check that both variables are grounded by same quantifier
+ if (m_bv.is_bv_shl(p, a, b) ||
+ m_bv.is_bv_ashr(p, a, b) ||
+ m_bv.is_bv_lshr(p, a, b)) {
+ if (!m_parents[(v == a ? b : a)->get_id()].get())
+ return false;
+
+ if (mc) {
+ ensure_mc(mc);
+ (*mc)->add(b, m_bv.mk_numeral(rational::zero(), get_sort(b)));
+ }
+ new_v = a;
+ return true;
+ }
+
if (m_bv.is_bv_mul(p)) {
expr_ref rest(m);
for (expr* arg : *to_app(p)) {
@@ -365,7 +396,8 @@ private:
expr_safe_replace sub(m);
t.m_parents.reset();
t.m_inverted.reset();
- expr_ref p(m), new_v(m);
+ expr_ref new_v(m);
+ expr * p;
{
parent_collector proc(t);
@@ -409,11 +441,9 @@ private:
rewriter_tpl(t.m, false, m_cfg),
m_cfg(t) {}
};
-
-
};
+}
tactic * mk_reduce_invertible_tactic(ast_manager & m, params_ref const &) {
return alloc(reduce_invertible_tactic, m);
}
-
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_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 aa804919f..3dc46f024 100644
--- a/src/util/lp/lp_utils.h
+++ b/src/util/lp/lp_utils.h
@@ -49,6 +49,7 @@ bool contains(const std::unordered_map & map, const A& key) {
#endif
namespace lp {
+
inline void throw_exception(const std::string & str) {
throw default_exception(str);
}
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;