From cef17c22a1d4a75e0335dbfce0f450563c2a870f Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 2 Jul 2018 17:08:02 +0100 Subject: [PATCH 1/8] remove some allocs from exceptions --- src/cmd_context/basic_cmds.cpp | 4 ++-- src/cmd_context/cmd_context.cpp | 2 +- src/muz/fp/horn_tactic.cpp | 2 +- src/parsers/smt2/smt2parser.cpp | 6 +++--- src/qe/nlqsat.cpp | 3 +-- src/qe/qsat.cpp | 4 ++-- src/sat/tactic/goal2sat.cpp | 2 +- src/smt/tactic/smt_tactic.cpp | 6 ++---- src/solver/parallel_tactic.cpp | 2 +- src/tactic/arith/pb2bv_tactic.cpp | 2 +- src/tactic/tactic.cpp | 6 +++--- src/tactic/tactic_exception.h | 2 +- src/tactic/tactical.cpp | 8 ++++---- src/util/cmd_context_types.h | 4 ++-- src/util/gparams.cpp | 8 ++++---- src/util/lp/lp_utils.h | 4 ++-- src/util/timeout.cpp | 6 ++++-- src/util/z3_exception.cpp | 3 --- src/util/z3_exception.h | 2 +- 19 files changed, 36 insertions(+), 40 deletions(-) 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/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/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/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_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; From 1f5d182f6a0fcc6608d4ad29355b502a3d0af4ea Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 2 Jul 2018 09:09:57 -0700 Subject: [PATCH 2/8] update java bindings for arrays Signed-off-by: Nikolaj Bjorner --- src/api/java/Model.java | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/api/java/Model.java b/src/api/java/Model.java index d809b6790..198c9918b 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 FuncInterp(getContext(), n); } } else { From 370abf602c3a2ad6d72054e320d5907d886b65a8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 2 Jul 2018 09:32:58 -0700 Subject: [PATCH 3/8] fix java API Signed-off-by: Nikolaj Bjorner --- src/api/java/Model.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/java/Model.java b/src/api/java/Model.java index 198c9918b..f7db67915 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -95,7 +95,7 @@ public class Model extends Z3Object { long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n); return getFuncInterp(new FuncDecl(getContext(), fd)); } - return FuncInterp(getContext(), n); + return new FuncInterp(getContext(), n); } } else { From 648a53195093dc532e6703196fd74ac89e26899f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 2 Jul 2018 09:50:29 -0700 Subject: [PATCH 4/8] update java example to bypass bit-rot Signed-off-by: Nikolaj Bjorner --- examples/dotnet/Program.cs | 1 + examples/java/JavaExample.java | 6 +++--- src/api/java/Model.java | 2 +- 3 files changed, 5 insertions(+), 4 deletions(-) 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/java/Model.java b/src/api/java/Model.java index f7db67915..8dc8d794b 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -95,7 +95,7 @@ public class Model extends Z3Object { long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n); return getFuncInterp(new FuncDecl(getContext(), fd)); } - return new FuncInterp(getContext(), n); + return null; } } else { From a73d0303212d47b10d1740f8b41d74feb906113f Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 2 Jul 2018 18:29:34 +0100 Subject: [PATCH 5/8] invertible_tactic: add partial support for shifts --- src/ast/bv_decl_plugin.h | 2 + src/tactic/core/reduce_invertible_tactic.cpp | 62 +++++++++++++++----- 2 files changed, 48 insertions(+), 16 deletions(-) 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/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); } - From e13b61eae8ed780a52358102d2aa8ff86d4832bc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 2 Jul 2018 11:10:37 -0700 Subject: [PATCH 6/8] work around regression with use of mk_app_core, returning BR_FAILED if nothing is rewritten Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Context.cs | 12 ++++++------ src/smt/theory_seq.cpp | 2 +- src/solver/smt_logics.cpp | 2 +- 3 files changed, 8 insertions(+), 8 deletions(-) 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/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index ef50cf3b6..51d1d7119 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -5021,7 +5021,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/smt_logics.cpp b/src/solver/smt_logics.cpp index 7ed2b0445..5d845b78b 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" || s == "HORN"; } bool smt_logics::logic_has_datatype(symbol const& s) { From 5e3303ae857262749a3aff7c3f3714d54743623a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 2 Jul 2018 11:46:03 -0700 Subject: [PATCH 7/8] let HORN solver know about cardinality constraints Signed-off-by: Nikolaj Bjorner --- src/ast/pb_decl_plugin.cpp | 2 +- src/cmd_context/check_logic.cpp | 3 ++- src/solver/smt_logics.cpp | 2 +- 3 files changed, 4 insertions(+), 3 deletions(-) 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/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/solver/smt_logics.cpp b/src/solver/smt_logics.cpp index 5d845b78b..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" || s == "HORN"; + return s == "QF_FD" || s == "ALL" || logic_has_horn(s); } bool smt_logics::logic_has_datatype(symbol const& s) { From dc8ec50137d892a70818487e9a4ac49be342890e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 2 Jul 2018 13:53:55 -0700 Subject: [PATCH 8/8] enable proof objects for PB Signed-off-by: Nikolaj Bjorner --- src/smt/theory_pb.cpp | 30 ++++++++++++++++++++++++++---- 1 file changed, 26 insertions(+), 4 deletions(-) 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) {