From 5d33805c8b1f377bfccabe2cc2d56ca35c54ed40 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 20 Aug 2023 10:07:56 +0100 Subject: [PATCH 01/10] optimize ~relevancy_propagator_imp() so it just dec refs the exprs in the trail It avoid doing all the funky watch stuff One extreme Alive2 test case goes from 40s to 28s :) --- src/smt/smt_relevancy.cpp | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/src/smt/smt_relevancy.cpp b/src/smt/smt_relevancy.cpp index 649d75737..ce6de3ec3 100644 --- a/src/smt/smt_relevancy.cpp +++ b/src/smt/smt_relevancy.cpp @@ -123,7 +123,7 @@ namespace smt { } struct relevancy_propagator_imp : public relevancy_propagator { - unsigned m_qhead; + unsigned m_qhead = 0; expr_ref_vector m_relevant_exprs; uint_set m_is_relevant; typedef list relevancy_ehs; @@ -144,14 +144,18 @@ namespace smt { unsigned m_trail_lim; }; svector m_scopes; - bool m_propagating; + bool m_propagating = false; relevancy_propagator_imp(context & ctx): - relevancy_propagator(ctx), m_qhead(0), m_relevant_exprs(ctx.get_manager()), - m_propagating(false) {} + relevancy_propagator(ctx), m_relevant_exprs(ctx.get_manager()) {} ~relevancy_propagator_imp() override { - undo_trail(0); + ast_manager & m = get_manager(); + unsigned i = m_trail.size(); + while (i != 0) { + --i; + m.dec_ref(m_trail[i].get_node()); + } } relevancy_ehs * get_handlers(expr * n) { From 3b546b2348fec5a19f708746ee268bc701d00023 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 20 Aug 2023 10:34:28 +0100 Subject: [PATCH 02/10] smt_context: we can't assert that the resource limits were exceeded on cancel_exception It happens sometimes that e.g. the internalizer goes above the soft memory limit But since it's only by a small amount, when the exception propagates back to the context, some stuff has been freed already and we are not longer above the memory threshold Just delete these asserts --- src/smt/smt_context.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 7895287ef..64c7bbf2e 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3565,7 +3565,6 @@ namespace smt { try { internalize_assertions(); } catch (cancel_exception&) { - VERIFY(resource_limits_exceeded()); return l_undef; } expr_ref_vector theory_assumptions(m); @@ -3637,7 +3636,6 @@ namespace smt { TRACE("unsat_core_bug", tout << asms << '\n';); init_assumptions(asms); } catch (cancel_exception&) { - VERIFY(resource_limits_exceeded()); return l_undef; } TRACE("before_search", display(tout);); @@ -3664,7 +3662,6 @@ namespace smt { for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef; init_assumptions(asms); } catch (cancel_exception&) { - VERIFY(resource_limits_exceeded()); return l_undef; } for (auto const& clause : clauses) init_clause(clause); From 28884b398c26291f867ae3ef08128b2709db72d5 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 20 Aug 2023 12:57:47 +0100 Subject: [PATCH 03/10] remove unneeded virtual destructor (optimization) --- src/smt/smt_relevancy.h | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/smt/smt_relevancy.h b/src/smt/smt_relevancy.h index f64b7d059..0fae815f9 100644 --- a/src/smt/smt_relevancy.h +++ b/src/smt/smt_relevancy.h @@ -29,7 +29,6 @@ namespace smt { void mark_as_relevant(relevancy_propagator & rp, expr * n); void mark_args_as_relevant(relevancy_propagator & rp, app * n); public: - virtual ~relevancy_eh() = default; /** \brief This method is invoked when n is marked as relevant. */ @@ -41,7 +40,7 @@ namespace smt { /** \brief Fallback for the two previous methods. */ - virtual void operator()(relevancy_propagator & rp) {} + virtual void operator()(relevancy_propagator & rp) = 0; }; class simple_relevancy_eh : public relevancy_eh { From c469c6e1d5a2188859f33faaa4a78c349bf8119a Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 20 Aug 2023 13:39:15 +0100 Subject: [PATCH 04/10] attempt to fix clang buildbots --- src/smt/smt_relevancy.h | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/smt/smt_relevancy.h b/src/smt/smt_relevancy.h index 0fae815f9..c32eabc5d 100644 --- a/src/smt/smt_relevancy.h +++ b/src/smt/smt_relevancy.h @@ -24,6 +24,9 @@ namespace smt { class context; class relevancy_propagator; +#pragma clang diagnostic push +#pragma clang diagnostic ignored "-Wnon-virtual-dtor" + class relevancy_eh { protected: void mark_as_relevant(relevancy_propagator & rp, expr * n); @@ -42,6 +45,7 @@ namespace smt { */ virtual void operator()(relevancy_propagator & rp) = 0; }; +#pragma clang diagnostic pop class simple_relevancy_eh : public relevancy_eh { expr * m_target; From 8210aafb69715e637cdad04e92638f791b27df2a Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 20 Aug 2023 14:09:04 +0100 Subject: [PATCH 05/10] ast compare_nodes: fail faster when comparing quantifier expressions --- src/ast/ast.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index e2e01bbee..0004aaa42 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -479,15 +479,15 @@ bool compare_nodes(ast const * n1, ast const * n2) { return q1->get_kind() == q2->get_kind() && q1->get_num_decls() == q2->get_num_decls() && + q1->get_expr() == q2->get_expr() && + q1->get_weight() == q2->get_weight() && + q1->get_num_patterns() == q2->get_num_patterns() && compare_arrays(q1->get_decl_sorts(), q2->get_decl_sorts(), q1->get_num_decls()) && compare_arrays(q1->get_decl_names(), q2->get_decl_names(), q1->get_num_decls()) && - q1->get_expr() == q2->get_expr() && - q1->get_weight() == q2->get_weight() && - q1->get_num_patterns() == q2->get_num_patterns() && ((q1->get_qid().is_numerical() && q2->get_qid().is_numerical()) || (q1->get_qid() == q2->get_qid())) && compare_arrays(q1->get_patterns(), From a694d2755737bdde9a7cec79e7090b08acb04deb Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 20 Aug 2023 14:20:20 +0100 Subject: [PATCH 06/10] revert removal of virtual destructor of relevancy_eh since clang doesnt play along --- src/smt/smt_relevancy.h | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/smt/smt_relevancy.h b/src/smt/smt_relevancy.h index c32eabc5d..8dea2842f 100644 --- a/src/smt/smt_relevancy.h +++ b/src/smt/smt_relevancy.h @@ -24,14 +24,12 @@ namespace smt { class context; class relevancy_propagator; -#pragma clang diagnostic push -#pragma clang diagnostic ignored "-Wnon-virtual-dtor" - class relevancy_eh { protected: void mark_as_relevant(relevancy_propagator & rp, expr * n); void mark_args_as_relevant(relevancy_propagator & rp, app * n); public: + virtual ~relevancy_eh() = default; /** \brief This method is invoked when n is marked as relevant. */ @@ -45,7 +43,6 @@ namespace smt { */ virtual void operator()(relevancy_propagator & rp) = 0; }; -#pragma clang diagnostic pop class simple_relevancy_eh : public relevancy_eh { expr * m_target; From 57c667e355a906c9bfc129e4a0fa5c979e423017 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 20 Aug 2023 15:16:47 +0100 Subject: [PATCH 07/10] remove unused code --- src/ast/ast.cpp | 16 ---------------- src/ast/ast.h | 5 ----- 2 files changed, 21 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 0004aaa42..56a89d346 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -542,22 +542,6 @@ inline unsigned ast_array_hash(T * const * array, unsigned size, unsigned init_v } } } -unsigned get_asts_hash(unsigned sz, ast * const* ns, unsigned init) { - return ast_array_hash(ns, sz, init); -} -unsigned get_apps_hash(unsigned sz, app * const* ns, unsigned init) { - return ast_array_hash(ns, sz, init); -} -unsigned get_exprs_hash(unsigned sz, expr * const* ns, unsigned init) { - return ast_array_hash(ns, sz, init); -} -unsigned get_sorts_hash(unsigned sz, sort * const* ns, unsigned init) { - return ast_array_hash(ns, sz, init); -} -unsigned get_decl_hash(unsigned sz, func_decl* const* ns, unsigned init) { - return ast_array_hash(ns, sz, init); -} - unsigned get_node_hash(ast const * n) { unsigned a, b, c; diff --git a/src/ast/ast.h b/src/ast/ast.h index d7a715cd1..b4b3b1b2f 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -970,11 +970,6 @@ inline quantifier const * to_quantifier(ast const * n) { SASSERT(is_quantifier(n unsigned get_node_hash(ast const * n); bool compare_nodes(ast const * n1, ast const * n2); unsigned get_node_size(ast const * n); -unsigned get_asts_hash(unsigned sz, ast * const* ns, unsigned init); -unsigned get_apps_hash(unsigned sz, app * const* ns, unsigned init); -unsigned get_exprs_hash(unsigned sz, expr * const* ns, unsigned init); -unsigned get_sorts_hash(unsigned sz, sort * const* ns, unsigned init); -unsigned get_decl_hash(unsigned sz, func_decl* const* ns, unsigned init); // This is the internal comparison functor for hash-consing AST nodes. struct ast_eq_proc { From dda0c8ff4200faa6a441855716b47ec7f93e026e Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 20 Aug 2023 22:28:57 +0100 Subject: [PATCH 08/10] array theory: use expr_ref for mk_default() so it doesnt leak if internalize throws like on timeout/memout --- src/smt/theory_array_full.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index 079c2f62e..345663b6b 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -546,7 +546,7 @@ namespace smt { expr_ref def2(m.mk_app(f, args2.size(), args2.data()), m); ctx.get_rewriter()(def2); - expr* def1 = mk_default(map); + expr_ref def1(mk_default(map), m); ctx.internalize(def1, false); ctx.internalize(def2, false); return try_assign_eq(def1, def2); @@ -561,7 +561,7 @@ namespace smt { SASSERT(is_const(cnst)); TRACE("array", tout << mk_bounded_pp(cnst->get_expr(), m) << "\n";); expr* val = cnst->get_arg(0)->get_expr(); - expr* def = mk_default(cnst->get_expr()); + expr_ref def(mk_default(cnst->get_expr()), m); ctx.internalize(def, false); return try_assign_eq(val, def); } @@ -598,7 +598,7 @@ namespace smt { return false; m_stats.m_num_default_lambda_axiom++; expr* e = arr->get_expr(); - expr* def = mk_default(e); + expr_ref def(mk_default(e), m); quantifier* lam = m.is_lambda_def(arr->get_decl()); TRACE("array", tout << mk_pp(lam, m) << "\n" << mk_pp(e, m) << "\n"); expr_ref_vector args(m); From 37ddaaef69db52097917581f9f7698027d3e536b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 20 Aug 2023 15:30:57 -0700 Subject: [PATCH 09/10] make destructors virtual Signed-off-by: Nikolaj Bjorner --- src/smt/arith_eq_adapter.cpp | 2 ++ src/smt/smt_relevancy.h | 2 ++ 2 files changed, 4 insertions(+) diff --git a/src/smt/arith_eq_adapter.cpp b/src/smt/arith_eq_adapter.cpp index b77a38927..f251d01ae 100644 --- a/src/smt/arith_eq_adapter.cpp +++ b/src/smt/arith_eq_adapter.cpp @@ -67,6 +67,8 @@ namespace smt { m_ge(ge) { } + ~arith_eq_relevancy_eh() override {} + void operator()(relevancy_propagator & rp) override { if (!rp.is_relevant(m_n1)) return; diff --git a/src/smt/smt_relevancy.h b/src/smt/smt_relevancy.h index 8dea2842f..f6e3c4659 100644 --- a/src/smt/smt_relevancy.h +++ b/src/smt/smt_relevancy.h @@ -48,6 +48,7 @@ namespace smt { expr * m_target; public: simple_relevancy_eh(expr * t):m_target(t) {} + ~simple_relevancy_eh() override {} void operator()(relevancy_propagator & rp) override; }; @@ -60,6 +61,7 @@ namespace smt { expr * m_target; public: pair_relevancy_eh(expr * s1, expr * s2, expr * t):m_source1(s1), m_source2(s2), m_target(t) {} + ~pair_relevancy_eh() override {} void operator()(relevancy_propagator & rp) override; }; From b8d8553c4155aa5cdf225d6704964c58089ef19d Mon Sep 17 00:00:00 2001 From: Hari Govind V K Date: Sun, 20 Aug 2023 18:36:22 -0400 Subject: [PATCH 10/10] support or, and, implies, distinct in mbp_basic (#6867) --- src/qe/mbp/mbp_arrays_tg.cpp | 1 - src/qe/mbp/mbp_basic_tg.cpp | 92 ++++++++++++++++++++++++++++++++---- src/qe/mbp/mbp_dt_tg.cpp | 1 - src/qe/mbp/mbp_qel.cpp | 2 +- 4 files changed, 84 insertions(+), 12 deletions(-) diff --git a/src/qe/mbp/mbp_arrays_tg.cpp b/src/qe/mbp/mbp_arrays_tg.cpp index 8f127819d..d3ed1a9eb 100644 --- a/src/qe/mbp/mbp_arrays_tg.cpp +++ b/src/qe/mbp/mbp_arrays_tg.cpp @@ -278,7 +278,6 @@ struct mbp_array_tg::impl { m_tg.get_terms(terms, false); for (unsigned i = 0; i < terms.size(); i++) { term = terms.get(i); - SASSERT(!m.is_distinct(term)); if (m_seen.is_marked(term)) continue; if (m_tg.is_cgr(term)) continue; TRACE("mbp_tg", tout << "processing " << expr_ref(term, m);); diff --git a/src/qe/mbp/mbp_basic_tg.cpp b/src/qe/mbp/mbp_basic_tg.cpp index d85215d17..5eca04151 100644 --- a/src/qe/mbp/mbp_basic_tg.cpp +++ b/src/qe/mbp/mbp_basic_tg.cpp @@ -43,32 +43,106 @@ struct mbp_basic_tg::impl { void mark_seen(expr *t) { m_seen.mark(t); } bool is_seen(expr *t) { return m_seen.is_marked(t); } - //Split on all ite terms, irrespective of whether - //they contain variables/are c-ground + // Split on all ite terms, irrespective of whether + // they contain variables/are c-ground bool apply() { - if (!m_use_mdl) return false; + std::function should_split, is_true, is_false; + if (!m_use_mdl) { + should_split = [&](expr *t) { return m_tg.has_val_in_class(t); }; + is_true = [&](expr *t) { + return m_tg.has_val_in_class(t) && m_mdl.is_true(t); + }; + is_false = [&](expr *t) { + return m_tg.has_val_in_class(t) && m_mdl.is_false(t); + }; + } else { + should_split = [](expr *t) { return true; }; + is_true = [&](expr *t) { return m_mdl.is_true(t); }; + is_false = [&](expr *t) { return m_mdl.is_false(t); }; + } + expr *c, *th, *el; expr_ref nterm(m); bool progress = false; TRACE("mbp_tg", tout << "Iterating over terms of tg";); // Not resetting terms because get_terms calls resize on terms m_tg.get_terms(terms, false); - for (expr* term : terms) { - if (is_seen(term)) - continue; - if (m.is_ite(term, c, th, el)) { + for (expr *term : terms) { + if (is_seen(term)) continue; + if (m.is_ite(term, c, th, el) && should_split(c)) { mark_seen(term); progress = true; if (m_mdl.is_true(c)) { m_tg.add_lit(c); m_tg.add_eq(term, th); - } - else { + } else { nterm = mk_not(m, c); m_tg.add_lit(nterm); m_tg.add_eq(term, el); } } + if (m.is_implies(term, c, th)) { + if (is_true(th) || is_false(c)) { + mark_seen(term); + progress = true; + if (is_true(th)) + m_tg.add_lit(th); + else if (is_false(c)) + m_tg.add_lit(c); + m_tg.add_eq(term, m.mk_true()); + } else if (is_true(c) && is_false(th)) { + mark_seen(term); + progress = true; + m_tg.add_eq(term, m.mk_false()); + } + } + if (m.is_or(term) || m.is_and(term)) { + bool is_or = m.is_or(term); + app *c = to_app(term); + bool t = is_or ? any_of(*c, is_true) : all_of(*c, is_true); + bool f = is_or ? all_of(*c, is_false) : all_of(*c, is_false); + if (t || f) { + mark_seen(term); + progress = true; + m_tg.add_eq(term, t ? m.mk_true() : m.mk_false()); + if (f) { + for (auto a : *c) { + if (is_false(a)) { + m_tg.add_lit(mk_not(m, a)); + if (!is_or) break; + } + } + } else { + for (auto a : *c) { + if (is_true(a)) { + m_tg.add_lit(a); + if (is_or) break; + } + } + } + } + } + if (m_use_mdl && m.is_distinct(term)) { + mark_seen(term); + progress = true; + bool eq = false; + app *c = to_app(term); + for (auto a1 : *c) { + for (auto a2 : *c) { + if (a1 == a2) continue; + if (m_mdl.are_equal(a1, a2)) { + m_tg.add_eq(a1, a2); + eq = true; + break; + } else + m_tg.add_deq(a1, a2); + } + } + if (eq) + m_tg.add_eq(term, m.mk_false()); + else + m_tg.add_eq(term, m.mk_true()); + } } return progress; } diff --git a/src/qe/mbp/mbp_dt_tg.cpp b/src/qe/mbp/mbp_dt_tg.cpp index b3b24617d..626e8a0e4 100644 --- a/src/qe/mbp/mbp_dt_tg.cpp +++ b/src/qe/mbp/mbp_dt_tg.cpp @@ -158,7 +158,6 @@ struct mbp_dt_tg::impl { m_tg.get_terms(terms, false); for (unsigned i = 0; i < terms.size(); i++) { term = terms.get(i); - SASSERT(!m.is_distinct(term)); if (is_seen(term)) continue; if (m_tg.is_cgr(term)) continue; if (is_app(term) && diff --git a/src/qe/mbp/mbp_qel.cpp b/src/qe/mbp/mbp_qel.cpp index d50a8c1f6..11b651268 100644 --- a/src/qe/mbp/mbp_qel.cpp +++ b/src/qe/mbp/mbp_qel.cpp @@ -178,7 +178,7 @@ class mbp_qel::impl { std::function non_core = [&](expr *e) { if (is_app(e) && is_partial_eq(to_app(e))) return true; - if (m.is_ite(e)) return true; + if (m.is_ite(e) || m.is_or(e) || m.is_implies(e) || m.is_and(e) || m.is_distinct(e)) return true; return red_vars.is_marked(e); };