From 3985943eecb107ec89ca539ec3d7766552b67835 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 May 2020 09:51:28 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 2 +- src/smt/smt_induction.cpp | 173 ++++++++------------------------------ src/smt/smt_induction.h | 30 +------ 3 files changed, 38 insertions(+), 167 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index b0f72f0e7..5043f0df1 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1601,7 +1601,7 @@ namespace smt { if (inconsistent()) return false; } -#if 0 +#if 1 if (at_search_level() && induction::should_try(*this)) { get_induction()(); } diff --git a/src/smt/smt_induction.cpp b/src/smt/smt_induction.cpp index c38a7377c..5497c3fb0 100644 --- a/src/smt/smt_induction.cpp +++ b/src/smt/smt_induction.cpp @@ -158,7 +158,7 @@ enode_vector induction_lemmas::induction_positions(enode* n) { for (unsigned i = 0; i < todo.size(); ++i) { n = todo[i]; for (enode* a : smt::enode::args(n)) { - add_todo(a); + add_todo(a); if (!a->is_marked2() && viable_induction_term(n, a)) { result.push_back(a); a->set_mark2(); @@ -171,86 +171,7 @@ enode_vector induction_lemmas::induction_positions(enode* n) { n->unset_mark2(); return result; } - -void induction_lemmas::abstract1(enode* n, enode* t, expr* x, abstractions& result) { - expr_safe_replace rep(m); - rep.insert(t->get_owner(), x); - expr_ref e(n->get_owner(), m); - rep(e); - result.push_back(abstraction(e)); -} - -/** - * abstraction candidates for replacing different occurrence of t in n by x - * it returns all possible non-empty subsets of t replaced by x. - * - * TBD: add term sharing throttle. - * TDD: add depth throttle. - */ -void 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())); - return; - } - func_decl* f = n->get_owner()->get_decl(); - // check if n is a s - if (f->is_skolem()) { - expr_ref e(n->get_owner(), m); - result.push_back(abstraction(e)); - } - - 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) { - r2.push_back(v); - r2.back().push_back(a); - } - } - r1.swap(r2); - r2.reset(); - result.shrink(n); - } - for (auto const& a : r1) { - result.push_back(abstraction(m, m.mk_app(n->get_decl(), a.m_terms), a.m_eqs)); - } -}; -/** - * filter generalizations based on value_generator - * If all evaluations are counter-examples, include - * candidate generalization. - */ -void 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; - for (auto const& vec : values) { - if (vec[i] && (m.is_true(vec[i]) == sign)) - continue; - all_cex = false; - break; - } - if (all_cex) { - abs[j++] = abs.get(i); - } - } - std::cout << "resulting size: " << j << " down from " << abs.size() << "\n"; - abs.shrink(j); -} - /** extract substitutions for x into accessor values of the same sort. collect side-conditions for the accessors to be well defined. @@ -308,35 +229,21 @@ void induction_lemmas::mk_hypothesis_substs_rec(unsigned depth, sort* s, expr* y */ void induction_lemmas::mk_hypothesis_lemma(expr_ref_vector const& conds, expr_pair_vector const& subst, literal alpha) { - expr* alpha_e = ctx.bool_var2expr(alpha.var()); - expr_ref beta(alpha_e, m); + expr_ref beta(m); + ctx.literal2expr(alpha, beta); expr_safe_replace rep(m); for (auto const& p : subst) { rep.insert(p.first, p.second); } rep(beta); // set beta := alpha[sk/acc(acc2(sk))] - literal b_lit = mk_literal(beta); - if (alpha.sign()) b_lit.neg(); + // alpha & is-c(sk) => ~alpha[sk/acc(sk)] literal_vector lits; lits.push_back(~alpha); for (expr* c : conds) lits.push_back(~mk_literal(c)); - lits.push_back(b_lit); + lits.push_back(~mk_literal(beta)); add_th_lemma(lits); } -void induction_lemmas::create_hypotheses(unsigned depth, expr* sk, literal alpha) { - expr_ref_vector conds(m); - cond_substs_t subst; - expr* alpha_e = ctx.bool_var2expr(alpha.var()); - mk_hypothesis_substs(depth, sk, subst); - for (auto& p : subst) { - expr_pair_vector vec; - vec.push_back(std::make_pair(sk, p.second)); - mk_hypothesis_lemma(p.first, vec, alpha); - } -} - -#if 0 void induction_lemmas::create_hypotheses(unsigned depth, expr_ref_vector const& sks, literal alpha) { if (sks.empty()) return; @@ -350,55 +257,33 @@ void induction_lemmas::create_hypotheses(unsigned depth, expr_ref_vector const& // append the identity substitution: expr_ref_vector conds(m); subst.push_back(std::make_pair(conds, expr_ref(sk, m))); - substs.push_back(std::make_pair(sk, subst)); } // create cross-product of instantiations: vector> s1, s2; - si.push_back(std::make_pair(expr_ref_vector(m), expr_pair_vector())); + s1.push_back(std::make_pair(expr_ref_vector(m), expr_pair_vector())); for (auto const& x2cond_sub : substs) { + s2.reset(); for (auto const& cond_sub : x2cond_sub.second) { - s2.reset(); for (auto const& cond_subs : s1) { expr_pair_vector pairs(cond_subs.second); expr_ref_vector conds(cond_subs.first); - pairs.push_back(x2cond_sub.first, cond_sub.second); + pairs.push_back(std::make_pair(x2cond_sub.first, cond_sub.second)); conds.append(cond_sub.first); s2.push_back(std::make_pair(conds, pairs)); } - s1.swap(s2); } + s1.swap(s2); } - s1.pop_back(); // last substitution is the identity. + s1.pop_back(); // last substitution is the identity // extract lemmas from instantiations for (auto& p : s1) { - mk_hypothesis_lemam(p.first, p.second, alpha); + mk_hypothesis_lemma(p.first, p.second, alpha); } } -#endif -void induction_lemmas::create_lemmas(expr* sk, abstraction& a, literal lit) { - std::cout << "abstraction: " << a.m_term << "\n"; - sort* s = m.get_sort(sk); - if (!m_dt.is_datatype(s)) - return; - expr_ref alpha = a.m_term; - literal alpha_lit = mk_literal(alpha); - if (lit.sign()) alpha_lit.neg(); - - create_hypotheses(1, sk, alpha_lit); - - literal_vector lits; - // phi & eqs => alpha - lits.push_back(~lit); - for (auto const& p : a.m_eqs) { - lits.push_back(~mk_literal(m.mk_eq(p.first, p.second))); - } - lits.push_back(alpha_lit); - add_th_lemma(lits); -} void induction_lemmas::add_th_lemma(literal_vector const& lits) { IF_VERBOSE(0, ctx.display_literals_verbose(verbose_stream() << "lemma:\n", lits) << "\n"); @@ -420,21 +305,35 @@ literal induction_lemmas::mk_literal(expr* e) { bool induction_lemmas::operator()(literal lit) { unsigned num = m_num_lemmas; enode* r = ctx.bool_var2enode(lit.var()); - unsigned position = 0; + expr_ref_vector sks(m); + expr_safe_replace rep(m); + + // have to be non-overlapping: for (enode* n : induction_positions(r)) { expr* t = n->get_owner(); - sort* s = m.get_sort(t); - expr_ref sk(m.mk_fresh_const("sk", s), m); - std::cout << "abstract " << mk_pp(t, m) << " " << sk << "\n"; - abstractions abs; - abstract1(r, n, sk, abs); - if (abs.size() > 1) filter_abstractions(lit.sign(), abs); - for (abstraction& a : abs) { - create_lemmas(sk, a, lit); + if (is_uninterp_const(t)) { // for now, to avoid overlapping terms + sort* s = m.get_sort(t); + expr_ref sk(m.mk_fresh_const("sk", s), m); + sks.push_back(sk); + rep.insert(t, sk); } - ++position; } - return m_num_lemmas > num; + expr_ref alpha(m); + ctx.literal2expr(lit, alpha); + rep(alpha); + literal alpha_lit = mk_literal(alpha); + + // alpha is the minimal instance of induction_positions where lit holds + // alpha & is-c(sk) => ~alpha[sk/acc(sk)] + create_hypotheses(1, sks, alpha_lit); + if (m_num_lemmas == num) + return false; + // lit => alpha + literal_vector lits; + lits.push_back(~lit); + lits.push_back(alpha_lit); + add_th_lemma(lits); + return true; } induction_lemmas::induction_lemmas(context& ctx, ast_manager& m, value_sweep& vs): diff --git a/src/smt/smt_induction.h b/src/smt/smt_induction.h index 901e74569..27931ab7c 100644 --- a/src/smt/smt_induction.h +++ b/src/smt/smt_induction.h @@ -58,30 +58,6 @@ namespace smt { unsigned m_num_lemmas; typedef svector> expr_pair_vector; - - struct abstraction { - expr_ref m_term; - expr_pair_vector m_eqs; - abstraction(expr_ref& e): m_term(e) {} - abstraction(ast_manager& m, expr* e, expr* n1, expr* n2): m_term(e, m) { - if (n1 != n2) m_eqs.push_back(std::make_pair(n1, n2)); - } - abstraction(ast_manager& m, expr* e, expr_pair_vector const& eqs): - m_term(e, m), m_eqs(eqs) { - } - }; - typedef vector abstractions; - - struct abstraction_arg { - expr_ref_vector m_terms; - expr_pair_vector m_eqs; - abstraction_arg(ast_manager& m): m_terms(m) {} - void push_back(abstraction& a) { - m_terms.push_back(a.m_term); - m_eqs.append(a.m_eqs); - } - }; - typedef vector abstraction_args; typedef std::pair cond_subst_t; typedef vector cond_substs_t; @@ -90,14 +66,10 @@ namespace smt { bool viable_induction_children(enode* n); bool viable_induction_term(enode* p , enode* n); enode_vector induction_positions(enode* n); - void abstract(enode* n, enode* t, expr* x, abstractions& result); - void abstract1(enode* n, enode* t, expr* x, abstractions& result); - void filter_abstractions(bool sign, abstractions& abs); - void create_lemmas(expr* sk, abstraction& a, literal lit); void mk_hypothesis_substs(unsigned depth, expr* x, cond_substs_t& subst); void mk_hypothesis_substs_rec(unsigned depth, sort* s, expr* y, expr_ref_vector& conds, cond_substs_t& subst); void mk_hypothesis_lemma(expr_ref_vector const& conds, expr_pair_vector const& subst, literal alpha); - void create_hypotheses(unsigned depth, expr* sk, literal alpha); + void create_hypotheses(unsigned depth, expr_ref_vector const& sks, literal alpha); literal mk_literal(expr* e); void add_th_lemma(literal_vector const& lits);