From 799b6131f26668e1e0317aa8c86fc4b6e6bd05d8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 30 Apr 2020 13:24:26 -0700 Subject: [PATCH] avoid repeated internalization of lambda #4169 Signed-off-by: Nikolaj Bjorner --- src/smt/params/smt_params.cpp | 2 + src/smt/params/smt_params.h | 2 + src/smt/params/smt_params_helper.pyg | 1 + src/smt/smt_induction.cpp | 90 +++++++++++++++++++--------- src/smt/smt_induction.h | 2 + src/smt/smt_internalizer.cpp | 3 + src/smt/theory_recfun.cpp | 18 ++++-- src/smt/theory_recfun.h | 1 + 8 files changed, 88 insertions(+), 31 deletions(-) diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 650200bab..de09e42d0 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -26,6 +26,7 @@ void smt_params::updt_local_params(params_ref const & _p) { m_random_seed = p.random_seed(); m_relevancy_lvl = p.relevancy(); m_ematching = p.ematching(); + m_induction = p.induction(); m_clause_proof = p.clause_proof(); m_phase_selection = static_cast(p.phase_selection()); if (m_phase_selection > PS_THEORY) throw default_exception("illegal phase selection numeral"); @@ -111,6 +112,7 @@ void smt_params::display(std::ostream & out) const { DISPLAY_PARAM(m_display_features); DISPLAY_PARAM(m_new_core2th_eq); DISPLAY_PARAM(m_ematching); + DISPLAY_PARAM(m_induction); DISPLAY_PARAM(m_clause_proof); DISPLAY_PARAM(m_case_split_strategy); diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index bd5d07f1c..b79631d1a 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -110,6 +110,7 @@ struct smt_params : public preprocessor_params, bool m_display_features; bool m_new_core2th_eq; bool m_ematching; + bool m_induction; bool m_clause_proof; // ----------------------------------- @@ -262,6 +263,7 @@ struct smt_params : public preprocessor_params, m_display_features(false), m_new_core2th_eq(true), m_ematching(true), + m_induction(false), m_clause_proof(false), m_case_split_strategy(CS_ACTIVITY_DELAY_NEW), m_rel_case_split_order(0), diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 4fcfcfd5a..86db50e3c 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -37,6 +37,7 @@ def_module_params(module_name='smt', ('qi.cost', STRING, '(+ weight generation)', 'expression specifying what is the cost of a given quantifier instantiation'), ('qi.max_multi_patterns', UINT, 0, 'specify the number of extra multi patterns'), ('qi.quick_checker', UINT, 0, 'specify quick checker mode, 0 - no quick checker, 1 - using unsat instances, 2 - using both unsat and no-sat instances'), + ('induction', BOOL, False, 'enable generation of induction lemmas'), ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'), ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'), ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'), diff --git a/src/smt/smt_induction.cpp b/src/smt/smt_induction.cpp index 3793f4d9f..a1d1c7301 100644 --- a/src/smt/smt_induction.cpp +++ b/src/smt/smt_induction.cpp @@ -55,6 +55,8 @@ literal_vector collect_induction_literals::pre_select() { continue; result.push_back(lit); } + TRACE("induction", ctx.display(tout << "literal index: " << m_literal_index << "\n" << result << "\n");); + ctx.push_trail(value_trail(m_literal_index)); m_literal_index = ctx.assigned_literals().size(); return result; @@ -68,11 +70,6 @@ void collect_induction_literals::model_sweep_filter(literal_vector& candidates) vector values; vs(terms, values); unsigned j = 0; - IF_VERBOSE(1, - verbose_stream() << "terms: " << terms << "\n"; - for (auto const& vec : values) { - verbose_stream() << "assignment: " << vec << "\n"; - }); for (unsigned i = 0; i < terms.size(); ++i) { literal lit = candidates[i]; bool is_viable_candidate = true; @@ -109,14 +106,26 @@ literal_vector collect_induction_literals::operator()() { // create_induction_lemmas bool create_induction_lemmas::is_induction_candidate(enode* n) { - expr* e = n->get_owner(); + app* e = n->get_owner(); if (m.is_value(e)) return false; - // TBD: filter if n is equivalent to a value. + bool in_good_context = false; + for (enode* p : n->get_parents()) { + app* o = p->get_owner(); + if (o->get_family_id() != m.get_basic_family_id()) + in_good_context = true; + } + if (!in_good_context) + return false; + + // avoid recursively unfolding skolem terms. + if (e->get_num_args() > 0 && e->get_family_id() == null_family_id) { + return false; + } sort* s = m.get_sort(e); if (m_dt.is_datatype(s) && m_dt.is_recursive(s)) return true; - + // potentially also induction on integers, sequences // m_arith.is_int(s) // return true; @@ -160,14 +169,24 @@ enode_vector create_induction_lemmas::induction_positions(enode* n) { * TDD: add depth throttle. */ void create_induction_lemmas::abstract(enode* n, enode* t, expr* x, abstractions& result) { + std::cout << "abs: " << result.size() << ": " << mk_pp(n->get_owner(), m) << "\n"; if (n->get_root() == t->get_root()) { result.push_back(abstraction(m, x, n->get_owner(), t->get_owner())); } +#if 0 + // check if n is a s + if (is_skolem(n->get_owner())) { + result.push_back(abstraction(m, n->get_owner())); + return; + } +#endif + abstraction_args r1, r2; r1.push_back(abstraction_arg(m)); for (enode* arg : enode::args(n)) { unsigned n = result.size(); abstract(arg, t, x, result); + std::cout << result.size() << "\n"; for (unsigned i = n; i < result.size(); ++i) { abstraction& a = result[i]; for (auto const& v : r1) { @@ -193,7 +212,9 @@ void create_induction_lemmas::filter_abstractions(bool sign, abstractions& abs) vector values; expr_ref_vector fmls(m); for (auto & a : abs) fmls.push_back(a.m_term); + std::cout << "sweep\n"; vs(fmls, values); + std::cout << "done sweep\n"; unsigned j = 0; for (unsigned i = 0; i < fmls.size(); ++i) { bool all_cex = true; @@ -207,15 +228,17 @@ void create_induction_lemmas::filter_abstractions(bool sign, abstractions& abs) abs[j++] = abs.get(i); } } + std::cout << "resulting size: " << j << " down from " << abs.size() << "\n"; abs.shrink(j); } /* * Create simple induction lemmas of the form: * - * lit & a.eqs() & is-c(t) => is-c(sk); * lit & a.eqs() => alpha - * lit & a.eqs() & is-c(t) => ~beta + * alpha & is-c(sk) => ~beta + * + * alpha & is-c(t) => is-c(sk); * * where * lit = is a formula containing t @@ -242,6 +265,7 @@ void create_induction_lemmas::create_lemmas(expr* t, expr* sk, abstraction& a, l return; expr_ref alpha = a.m_term; auto const& eqs = a.m_eqs; + literal alpha_lit = null_literal; literal_vector common_literals; for (func_decl* c : *m_dt.get_datatype_constructors(s)) { func_decl* is_c = m_dt.get_constructor_recognizer(c); @@ -249,43 +273,51 @@ void create_induction_lemmas::create_lemmas(expr* t, expr* sk, abstraction& a, l for (func_decl* acc : *m_dt.get_constructor_accessors(c)) { if (acc->get_range() != s) continue; - if (common_literals.empty()) { - common_literals.push_back(~lit); - for (auto const& p : eqs) { - common_literals.push_back(~mk_literal(m.mk_eq(p.first, p.second))); - } + if (alpha_lit == null_literal) { + alpha_lit = mk_literal(alpha); + if (lit.sign()) alpha_lit.neg(); } has_1recursive = true; - literal_vector lits(common_literals); - lits.push_back(~mk_literal(m.mk_app(is_c, t))); expr_ref beta(alpha); expr_safe_replace rep(m); rep.insert(sk, m.mk_app(acc, sk)); rep(beta); literal b_lit = mk_literal(beta); if (lit.sign()) b_lit.neg(); + + // alpha & is_c(sk) => ~beta + literal_vector lits; + lits.push_back(~alpha_lit); + lits.push_back(~mk_literal(m.mk_app(is_c, sk))); lits.push_back(~b_lit); add_th_lemma(lits); } + + // alpha & is_c(t) => is_c(sk) if (has_1recursive) { - literal_vector lits(common_literals); + literal_vector lits; + lits.push_back(~alpha_lit); lits.push_back(~mk_literal(m.mk_app(is_c, t))); lits.push_back(mk_literal(m.mk_app(is_c, sk))); add_th_lemma(lits); } } - if (!common_literals.empty()) { - literal_vector lits(common_literals); - literal a_lit = mk_literal(alpha); - if (lit.sign()) a_lit.neg(); - lits.push_back(a_lit); + + // phi & eqs => alpha + if (alpha_lit != null_literal) { + literal_vector lits; + lits.push_back(~lit); + for (auto const& p : eqs) { + lits.push_back(~mk_literal(m.mk_eq(p.first, p.second))); + } + lits.push_back(alpha_lit); add_th_lemma(lits); } } void create_induction_lemmas::add_th_lemma(literal_vector const& lits) { IF_VERBOSE(1, ctx.display_literals_verbose(verbose_stream() << "lemma:\n", lits) << "\n"); - ctx.mk_clause(lits.size(), lits.c_ptr(), nullptr, smt::CLS_TH_LEMMA); + ctx.mk_clause(lits.size(), lits.c_ptr(), nullptr, smt::CLS_TH_AXIOM); // CLS_TH_LEMMA, but then should re-instance if GC'ed ++m_num_lemmas; } @@ -301,8 +333,8 @@ literal create_induction_lemmas::mk_literal(expr* e) { func_decl* create_induction_lemmas::mk_skolem(sort* s) { func_decl* f = nullptr; if (!m_sort2skolem.find(s, f)) { - sort* domain[2] = { s, m.mk_bool_sort() }; - f = m.mk_fresh_func_decl("sk", 2, domain, s); + sort* domain[3] = { m_a.mk_int(), s, m.mk_bool_sort() }; + f = m.mk_fresh_func_decl("sk", 3, domain, s); m_pinned.push_back(f); m_pinned.push_back(s); m_sort2skolem.insert(s, f); @@ -314,10 +346,11 @@ func_decl* create_induction_lemmas::mk_skolem(sort* s) { bool create_induction_lemmas::operator()(literal lit) { unsigned num = m_num_lemmas; enode* r = ctx.bool_var2enode(lit.var()); + unsigned position = 0; for (enode* n : induction_positions(r)) { expr* t = n->get_owner(); sort* s = m.get_sort(t); - expr_ref sk(m.mk_app(mk_skolem(s), t, r->get_owner()), m); + expr_ref sk(m.mk_app(mk_skolem(s), m_a.mk_int(position), t, r->get_owner()), m); std::cout << "abstract " << mk_pp(t, m) << " " << sk << "\n"; abstractions abs; abstract(r, n, sk, abs); @@ -326,6 +359,8 @@ bool create_induction_lemmas::operator()(literal lit) { for (abstraction& a : abs) { create_lemmas(t, sk, a, lit); } + std::cout << "lemmas created\n"; + ++position; } return m_num_lemmas > num; } @@ -335,6 +370,7 @@ create_induction_lemmas::create_induction_lemmas(context& ctx, ast_manager& m, v m(m), vs(vs), m_dt(m), + m_a(m), m_pinned(m), m_num_lemmas(0) {} diff --git a/src/smt/smt_induction.h b/src/smt/smt_induction.h index ca501dd2a..03c56b4a1 100644 --- a/src/smt/smt_induction.h +++ b/src/smt/smt_induction.h @@ -20,6 +20,7 @@ #include "smt/smt_types.h" #include "ast/rewriter/value_sweep.h" #include "ast/datatype_decl_plugin.h" +#include "ast/arith_decl_plugin.h" namespace smt { @@ -52,6 +53,7 @@ namespace smt { ast_manager& m; value_sweep& vs; datatype::util m_dt; + arith_util m_a; obj_map m_sort2skolem; ast_ref_vector m_pinned; unsigned m_num_lemmas; diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 1e75e4b15..5293dd888 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -558,6 +558,9 @@ namespace smt { void context::internalize_lambda(quantifier * q) { TRACE("internalize_quantifier", tout << mk_pp(q, m) << "\n";); SASSERT(is_lambda(q)); + if (e_internalized(q)) { + return; + } app_ref lam_name(m.mk_fresh_const("lambda", m.get_sort(q)), m); app_ref eq(m), lam_app(m); expr_ref_vector vars(m); diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index cfe4522de..4fa0db63e 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -21,7 +21,6 @@ Revision History: #include "ast/ast_util.h" #include "ast/for_each_expr.h" #include "smt/theory_recfun.h" -#include "smt/params/smt_params_helper.hpp" #define TRACEFN(x) TRACE("recfun", tout << x << '\n';) @@ -357,6 +356,7 @@ namespace smt { literal_vector preds; auto & vars = e.m_def->get_vars(); + unsigned max_depth = 0; for (recfun::case_def const & c : e.m_def->get_cases()) { // applied predicate to `args` app_ref pred_applied = c.apply_case_predicate(e.m_args); @@ -376,15 +376,25 @@ namespace smt { } else if (!is_enabled_guard(pred_applied)) { disable_guard(pred_applied, guards); + max_depth = std::max(depth, max_depth); continue; } activate_guard(pred_applied, guards); } // the disjunction of branches is asserted // to close the available cases. - std::function fn2 = [&]() { return preds; }; - scoped_trace_stream _tr2(*this, fn2); - ctx().mk_th_axiom(get_id(), preds); + { + scoped_trace_stream _tr2(*this, preds); + ctx().mk_th_axiom(get_id(), preds); + } + (void)max_depth; + // add_induction_lemmas(max_depth); + } + + void theory_recfun::add_induction_lemmas(unsigned depth) { + if (depth > 4 && ctx().get_fparams().m_induction && induction::should_try(ctx())) { + ctx().get_induction()(); + } } void theory_recfun::activate_guard(expr* pred_applied, expr_ref_vector const& guards) { diff --git a/src/smt/theory_recfun.h b/src/smt/theory_recfun.h index 62aa489b7..67e475aae 100644 --- a/src/smt/theory_recfun.h +++ b/src/smt/theory_recfun.h @@ -127,6 +127,7 @@ namespace smt { void assert_body_axiom(body_expansion & e); literal mk_literal(expr* e); + void add_induction_lemmas(unsigned depth); void disable_guard(expr* guard, expr_ref_vector const& guards); unsigned get_depth(expr* e); void set_depth(unsigned d, expr* e);