diff --git a/src/smt/smt_induction.cpp b/src/smt/smt_induction.cpp
new file mode 100644
index 000000000..c2eccdb02
--- /dev/null
+++ b/src/smt/smt_induction.cpp
@@ -0,0 +1,368 @@
+/*++
+ Copyright (c) 2020 Microsoft Corporation
+
+ Module Name:
+
+ smt_induction.cpp
+
+ Abstract:
+
+ Add induction lemmas to context.
+
+ Author:
+
+ Nikolaj Bjorner 2020-04-25
+
+ Notes:
+
+ - work in absence of recursive functions but instead presence of quantifiers
+ - relax current requirement of model sweeping when terms don't have value simplifications
+ - k-induction
+ - also to deal with mutually recursive datatypes
+ - beyond literal induction lemmas
+ - refine initialization of values when term is equal to constructor application,
+
+--*/
+
+#include "ast/ast_pp.h"
+#include "ast/ast_util.h"
+#include "ast/recfun_decl_plugin.h"
+#include "ast/datatype_decl_plugin.h"
+#include "ast/arith_decl_plugin.h"
+#include "ast/rewriter/value_sweep.h"
+#include "ast/rewriter/expr_safe_replace.h"
+#include "smt/smt_context.h"
+#include "smt/smt_induction.h"
+
+using namespace smt;
+
+/**
+ * collect literals that are assigned to true,
+ * but evaluate to false under all extensions of
+ * the congruence closure.
+ */
+
+literal_vector collect_induction_literals::pre_select() {
+ literal_vector result;
+ for (unsigned i = m_literal_index; i < ctx.assigned_literals().size(); ++i) {
+ literal lit = ctx.assigned_literals()[i];
+ smt::bool_var v = lit.var();
+ if (!ctx.has_enode(v)) {
+ continue;
+ }
+ expr* e = ctx.bool_var2expr(v);
+ if (!lit.sign() && m.is_eq(e))
+ continue;
+ result.push_back(lit);
+ }
+ ctx.push_trail(value_trail<context, unsigned>(m_literal_index));
+ m_literal_index = ctx.assigned_literals().size();
+ return result;
+}
+
+void collect_induction_literals::model_sweep_filter(literal_vector& candidates) {
+ expr_ref_vector terms(m);
+ for (literal lit : candidates) {
+ terms.push_back(ctx.bool_var2expr(lit.var()));
+ }
+ vector<expr_ref_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;
+ for (auto const& vec : values) {
+ if (vec[i] && lit.sign() && m.is_true(vec[i]))
+ continue;
+ if (vec[i] && !lit.sign() && m.is_false(vec[i]))
+ continue;
+ is_viable_candidate = false;
+ break;
+ }
+ if (is_viable_candidate)
+ candidates[j++] = lit;
+ }
+ candidates.shrink(j);
+}
+
+
+collect_induction_literals::collect_induction_literals(context& ctx, ast_manager& m, value_sweep& vs):
+ ctx(ctx),
+ m(m),
+ vs(vs),
+ m_literal_index(0)
+{}
+
+literal_vector collect_induction_literals::operator()() {
+ literal_vector candidates = pre_select();
+ model_sweep_filter(candidates);
+ return candidates;
+}
+
+
+// --------------------------------------
+// create_induction_lemmas
+
+bool create_induction_lemmas::is_induction_candidate(enode* n) {
+ expr* e = n->get_owner();
+ if (m.is_value(e))
+ return false;
+ // TBD: filter if n is equivalent to a value.
+ 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;
+ return false;
+}
+
+/**
+ * positions in n that can be used for induction
+ * the positions are distinct roots
+ * and none of the roots are equivalent to a value in the current
+ * congruence closure.
+ */
+enode_vector create_induction_lemmas::induction_positions(enode* n) {
+ enode_vector result;
+ enode_vector todo;
+ auto add_todo = [&](enode* n) {
+ if (!n->is_marked()) {
+ n->set_mark();
+ todo.push_back(n);
+ }
+ };
+ add_todo(n);
+ for (unsigned i = 0; i < todo.size(); ++i) {
+ n = todo[i];
+ for (enode* a : smt::enode::args(n))
+ add_todo(a);
+ if (is_induction_candidate(n))
+ result.push_back(n);
+ }
+ for (enode* n : todo)
+ n->unset_mark();
+ return result;
+}
+
+
+/**
+ * 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 create_induction_lemmas::abstract(enode* n, enode* t, expr* x, abstractions& result) {
+ if (n->get_root() == t->get_root()) {
+ result.push_back(abstraction(m, x, n->get_owner(), t->get_owner()));
+ }
+ 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);
+ 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 create_induction_lemmas::filter_abstractions(bool sign, abstractions& abs) {
+ vector<expr_ref_vector> values;
+ expr_ref_vector fmls(m);
+ for (auto & a : abs) fmls.push_back(a.m_term);
+ vs(fmls, values);
+ 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);
+ }
+ }
+ 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
+ *
+ * where alpha = a.term()
+ * beta = alpha[sk/access_k(sk)]
+ * for each constructor c, that is recursive
+ * and contains argument of datatype sort s
+ *
+ * TBD: consider k-inductive lemmas.
+ */
+void create_induction_lemmas::create_lemmas(expr* t, 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;
+ family_id fid = s->get_family_id();
+ expr_ref alpha = a.m_term;
+ auto const& eqs = a.m_eqs;
+ literal_vector common_literals;
+ for (func_decl* c : *m_dt.get_datatype_constructors(s)) {
+ func_decl* is_c = m_dt.get_constructor_recognizer(c);
+ bool has_1recursive = false;
+ 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)));
+ }
+ }
+ 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();
+ lits.push_back(~b_lit);
+ add_th_lemma(lits);
+ }
+ if (has_1recursive) {
+ literal_vector lits(common_literals);
+ 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);
+ 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);
+ ++m_num_lemmas;
+}
+
+literal create_induction_lemmas::mk_literal(expr* e) {
+ if (!ctx.e_internalized(e)) {
+ ctx.internalize(e, false);
+ }
+ enode* n = ctx.get_enode(e);
+ ctx.mark_as_relevant(n);
+ return ctx.get_literal(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);
+ m_pinned.push_back(f);
+ m_pinned.push_back(s);
+ m_sort2skolem.insert(s, f);
+ }
+ return f;
+}
+
+
+bool create_induction_lemmas::operator()(literal lit) {
+ unsigned num = m_num_lemmas;
+ enode* r = ctx.bool_var2enode(lit.var());
+ 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);
+ std::cout << "abstract " << mk_pp(t, m) << " " << sk << "\n";
+ abstractions abs;
+ abstract(r, n, sk, abs);
+ abs.pop_back(); // last position has no generalizations
+ filter_abstractions(lit.sign(), abs);
+ for (abstraction& a : abs) {
+ create_lemmas(t, sk, a, lit);
+ }
+ }
+ return m_num_lemmas > num;
+}
+
+create_induction_lemmas::create_induction_lemmas(context& ctx, ast_manager& m, value_sweep& vs):
+ ctx(ctx),
+ m(m),
+ vs(vs),
+ m_dt(m),
+ m_pinned(m),
+ m_num_lemmas(0)
+{}
+
+induction::induction(context& ctx, ast_manager& m):
+ ctx(ctx),
+ m(m),
+ vs(m),
+ m_collect_literals(ctx, m, vs),
+ m_create_lemmas(ctx, m, vs)
+{}
+
+// TBD: use smt_arith_value to also include state from arithmetic solver
+void induction::init_values() {
+ for (enode* n : ctx.enodes())
+ if (m.is_value(n->get_owner()))
+ for (enode* r : *n)
+ vs.set_value(r->get_owner(), n->get_owner());
+}
+
+bool induction::operator()() {
+ bool added_lemma = false;
+ vs.reset_values();
+ literal_vector candidates = m_collect_literals();
+ for (literal lit : candidates) {
+ if (m_create_lemmas(lit))
+ added_lemma = true;
+ }
+ return added_lemma;
+}
+
+// state contains datatypes + recursive functions
+// more comprehensive:
+// state contains integers / datatypes / sequences + recursive function / quantifiers
+
+bool induction::should_try(context& ctx) {
+ recfun::util u(ctx.get_manager());
+ datatype::util dt(ctx.get_manager());
+ theory* adt = ctx.get_theory(dt.get_family_id());
+ return adt && adt->get_num_vars() > 0 && !u.get_rec_funs().empty();
+}
diff --git a/src/smt/smt_induction.h b/src/smt/smt_induction.h
new file mode 100644
index 000000000..ca501dd2a
--- /dev/null
+++ b/src/smt/smt_induction.h
@@ -0,0 +1,123 @@
+/*++
+ Copyright (c) 2020 Microsoft Corporation
+
+ Module Name:
+
+ smt_induction.h
+
+ Abstract:
+
+ Add induction lemmas to context.
+
+ Author:
+
+ Nikolaj Bjorner 2020-04-25
+
+--*/
+
+#pragma once
+
+#include "smt/smt_types.h"
+#include "ast/rewriter/value_sweep.h"
+#include "ast/datatype_decl_plugin.h"
+
+namespace smt {
+
+ class context;
+
+ /**
+ * Collect literals that are potentially useful for induction lemmas.
+ */
+ class collect_induction_literals {
+ context& ctx;
+ ast_manager& m;
+ value_sweep& vs;
+ unsigned m_literal_index;
+
+ literal_vector pre_select();
+
+ void model_sweep_filter(literal_vector& candidates);
+
+ public:
+ collect_induction_literals(context& ctx, ast_manager& m, value_sweep& vs);
+
+ literal_vector operator()();
+ };
+
+ /**
+ * Synthesize induction lemmas from induction candidates
+ */
+ class create_induction_lemmas {
+ context& ctx;
+ ast_manager& m;
+ value_sweep& vs;
+ datatype::util m_dt;
+ obj_map<sort, func_decl*> m_sort2skolem;
+ ast_ref_vector m_pinned;
+ unsigned m_num_lemmas;
+
+ typedef svector<std::pair<expr*,expr*>> expr_pair_vector;
+
+ func_decl* mk_skolem(sort* s);
+
+ 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<abstraction> 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_arg> abstraction_args;
+
+ bool is_induction_candidate(enode* n);
+ enode_vector induction_positions(enode* n);
+ void abstract(enode* n, enode* t, expr* x, abstractions& result);
+ void filter_abstractions(bool sign, abstractions& abs);
+ void create_lemmas(expr* t, expr* sk, abstraction& a, literal lit);
+ literal mk_literal(expr* e);
+ void add_th_lemma(literal_vector const& lits);
+
+ public:
+ create_induction_lemmas(context& ctx, ast_manager& m, value_sweep& vs);
+
+ bool operator()(literal lit);
+ };
+
+ /**
+ * Establish induction clauses.
+ */
+
+ class induction {
+ context& ctx;
+ ast_manager& m;
+ value_sweep vs;
+ collect_induction_literals m_collect_literals;
+ create_induction_lemmas m_create_lemmas;
+
+ void init_values();
+
+ public:
+ induction(context& ctx, ast_manager& m);
+
+ bool operator()();
+
+ static bool should_try(context& ctx);
+ };
+
+}