/*++
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/for_each_expr.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);
}
TRACE(induction, ctx.display(tout << "literal index: " << m_literal_index << "\n" << result << "\n"););
ctx.push_trail(value_trail<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;
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;
}
// --------------------------------------
// induction_lemmas
bool induction_lemmas::viable_induction_sort(sort* s) {
// potentially also induction on integers, sequences
return m_dt.is_datatype(s) && m_dt.is_recursive(s);
}
bool induction_lemmas::viable_induction_parent(enode* p, enode* n) {
app* o = p->get_expr();
return
m_rec.is_defined(o) ||
m_dt.is_constructor(o);
}
bool induction_lemmas::viable_induction_children(enode* n) {
app* e = n->get_expr();
if (m.is_value(e))
return false;
if (e->get_decl()->is_skolem())
return false;
if (n->get_num_args() == 0)
return true;
if (e->get_family_id() == m_rec.get_family_id())
return m_rec.is_defined(e);
if (e->get_family_id() == m_dt.get_family_id())
return m_dt.is_constructor(e);
return false;
}
bool induction_lemmas::viable_induction_term(enode* p, enode* n) {
return
viable_induction_sort(n->get_expr()->get_sort()) &&
viable_induction_parent(p, n) &&
viable_induction_children(n);
}
/**
* 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 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 (!a->is_marked2() && viable_induction_term(n, a)) {
result.push_back(a);
a->set_mark2();
}
}
}
for (enode* n : todo)
n->unset_mark();
for (enode* n : result)
n->unset_mark2();
return result;
}
// Collecting induction positions relative to parent.
induction_lemmas::induction_positions_t induction_lemmas::induction_positions2(enode* n) {
induction_positions_t result;
enode_vector todo;
todo.push_back(n);
n->set_mark();
for (unsigned i = 0; i < todo.size(); ++i) {
enode* n = todo[i];
unsigned idx = 0;
for (enode* a : smt::enode::args(n)) {
if (viable_induction_term(n, a)) {
result.push_back(induction_position_t(n, idx));
}
if (!a->is_marked()) {
a->set_mark();
todo.push_back(a);
}
++idx;
}
}
for (enode* n : todo)
n->unset_mark();
return result;
}
void induction_lemmas::initialize_levels(enode* n) {
expr_ref tmp(n->get_expr(), m);
m_depth2terms.reset();
m_depth2terms.resize(get_depth(tmp) + 1);
m_ts++;
for (expr* t : subterms(tmp)) {
if (is_app(t)) {
m_depth2terms[get_depth(t)].push_back(to_app(t));
m_marks.reserve(t->get_id()+1, 0);
}
}
}
induction_lemmas::induction_combinations_t induction_lemmas::induction_combinations(enode* n) {
initialize_levels(n);
induction_combinations_t result;
auto pos = induction_positions2(n);
if (pos.size() > 6) {
induction_positions_t r;
for (auto const& p : pos) {
if (is_uninterp_const(p.first->get_expr()))
r.push_back(p);
}
result.push_back(r);
return result;
}
for (unsigned i = 0; i < (1ull << pos.size()); ++i) {
induction_positions_t r;
for (unsigned j = 0; j < pos.size(); ++j) {
if (0 != (i & (1 << j)))
r.push_back(pos[j]);
}
if (positions_dont_overlap(r))
result.push_back(r);
}
for (auto const& pos : result) {
std::cout << "position\n";
for (auto const& p : pos) {
std::cout << mk_pp(p.first->get_expr(), m) << ":" << p.second << "\n";
}
}
return result;
}
bool induction_lemmas::positions_dont_overlap(induction_positions_t const& positions) {
if (positions.empty())
return false;
m_ts++;
auto mark = [&](expr* n) { m_marks[n->get_id()] = m_ts; };
auto is_marked = [&](expr* n) { return m_marks[n->get_id()] == m_ts; };
for (auto p : positions)
mark(p.first->get_expr());
// no term used for induction contains a subterm also used for induction.
for (auto const& terms : m_depth2terms) {
for (app* t : terms) {
bool has_mark = false;
for (expr* arg : *t)
has_mark |= is_marked(arg);
if (is_marked(t) && has_mark)
return false;
if (has_mark)
mark(t);
}
}
return true;
}
/**
extract substitutions for x into accessor values of the same sort.
collect side-conditions for the accessors to be well defined.
apply a depth-bounded unfolding of datatype constructors to collect
accessor values beyond a first level and for nested (mutually recursive)
datatypes.
*/
void induction_lemmas::mk_hypothesis_substs(unsigned depth, expr* x, cond_substs_t& subst) {
expr_ref_vector conds(m);
mk_hypothesis_substs_rec(depth, x->get_sort(), x, conds, subst);
}
void induction_lemmas::mk_hypothesis_substs_rec(unsigned depth, sort* s, expr* y, expr_ref_vector& conds, cond_substs_t& subst) {
sort* ys = y->get_sort();
for (func_decl* c : *m_dt.get_datatype_constructors(ys)) {
func_decl* is_c = m_dt.get_constructor_recognizer(c);
conds.push_back(m.mk_app(is_c, y));
for (func_decl* acc : *m_dt.get_constructor_accessors(c)) {
sort* rs = acc->get_range();
if (!m_dt.is_datatype(rs) || !m_dt.is_recursive(rs))
continue;
expr_ref acc_y(m.mk_app(acc, y), m);
if (rs == s) {
subst.push_back(std::make_pair(conds, acc_y));
}
if (depth > 1) {
mk_hypothesis_substs_rec(depth - 1, s, acc_y, conds, subst);
}
}
conds.pop_back();
}
}
/*
* Create simple induction lemmas of the form:
*
* lit & a.eqs() => alpha
* alpha & is-c(sk) => ~beta
*
* where
* lit = is a formula containing t
* alpha = a.term(), a variant of lit
* with some occurrences of t replaced by sk
* beta = alpha[sk/access_k(sk)]
* for each constructor c, that is recursive
* and contains argument of datatype sort s
*
* The main claim is that the lemmas are valid and that
* they approximate induction reasoning.
*
* alpha approximates minimal instance of the datatype s where
* the instance of s is true. In the limit one can
* set beta to all instantiations of smaller values than sk.
*
*/
void induction_lemmas::mk_hypothesis_lemma(expr_ref_vector const& conds, expr_pair_vector const& subst, literal alpha) {
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))]
// 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(~mk_literal(beta));
add_th_lemma(lits);
}
void induction_lemmas::create_hypotheses(unsigned depth, expr_ref_vector const& sks, literal alpha) {
if (sks.empty())
return;
// extract hypothesis substitutions
vector<std::pair<expr*, cond_substs_t>> substs;
for (expr* sk : sks) {
cond_substs_t subst;
mk_hypothesis_substs(depth, sk, subst);
// 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<std::pair<expr_ref_vector, expr_pair_vector>> s1, s2;
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) {
for (auto const& cond_subs : s1) {
expr_pair_vector pairs(cond_subs.second);
expr_ref_vector conds(cond_subs.first);
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.pop_back(); // last substitution is the identity
// extract lemmas from instantiations
for (auto& p : s1) {
mk_hypothesis_lemma(p.first, p.second, alpha);
}
}
void induction_lemmas::add_th_lemma(literal_vector const& lits) {
IF_VERBOSE(0, ctx.display_literals_verbose(verbose_stream() << "lemma:\n", lits) << "\n");
ctx.mk_clause(lits.size(), lits.data(), nullptr, smt::CLS_TH_AXIOM);
// CLS_TH_LEMMA, but then should re-instance if GC'ed
++m_num_lemmas;
}
literal induction_lemmas::mk_literal(expr* e) {
expr_ref _e(e, m);
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);
}
bool induction_lemmas::operator()(literal lit) {
enode* r = ctx.bool_var2enode(lit.var());
#if 1
auto combinations = induction_combinations(r);
for (auto const& positions : combinations) {
apply_induction(lit, positions);
}
return !combinations.empty();
#else
unsigned num = m_num_lemmas;
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();
if (is_uninterp_const(t)) { // for now, to avoid overlapping terms
sort* s = t->get_sort();
expr_ref sk(m.mk_fresh_const("sk", s), m);
sks.push_back(sk);
rep.insert(t, sk);
}
}
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;
#endif
}
void induction_lemmas::apply_induction(literal lit, induction_positions_t const & positions) {
unsigned num = m_num_lemmas;
obj_map<expr, expr*> term2skolem;
expr_ref alpha(m), sk(m);
expr_ref_vector sks(m);
ctx.literal2expr(lit, alpha);
induction_term_and_position_t itp(alpha, positions);
bool found = m_skolems.find(itp, itp);
if (found) {
sks.append(itp.m_skolems.size(), itp.m_skolems.data());
}
unsigned i = 0;
for (auto const& p : positions) {
expr* t = p.first->get_expr()->get_arg(p.second);
if (term2skolem.contains(t))
continue;
if (i == sks.size()) {
sk = m.mk_fresh_const("sk", t->get_sort());
sks.push_back(sk);
}
else {
sk = sks.get(i);
}
term2skolem.insert(t, sk);
++i;
}
if (!found) {
itp.m_skolems.append(sks.size(), sks.data());
m_trail.push_back(alpha);
m_trail.append(sks);
m_skolems.insert(itp);
}
ptr_vector<expr> todo;
obj_map<expr, expr*> sub;
expr_ref_vector trail(m), args(m);
todo.push_back(alpha);
// replace occurrences of induction arguments.
#if 0
std::cout << "positions\n";
for (auto const& p : positions)
std::cout << mk_pp(p.first->get_owner(), m) << " " << p.second << "\n";
#endif
while (!todo.empty()) {
expr* t = todo.back();
if (sub.contains(t)) {
todo.pop_back();
continue;
}
SASSERT(is_app(t));
args.reset();
unsigned sz = todo.size();
expr* s = nullptr;
for (unsigned i = 0; i < to_app(t)->get_num_args(); ++i) {
expr* arg = to_app(t)->get_arg(i);
found = false;
for (auto const& p : positions) {
if (p.first->get_expr() == t && p.second == i) {
args.push_back(term2skolem[arg]);
found = true;
break;
}
}
if (found)
continue;
if (sub.find(arg, s)) {
args.push_back(s);
continue;
}
todo.push_back(arg);
}
if (todo.size() == sz) {
s = m.mk_app(to_app(t)->get_decl(), args);
trail.push_back(s);
sub.insert(t, s);
todo.pop_back();
}
}
alpha = sub[alpha];
std::cout << "alpha:" << alpha << "\n";
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) {
// lit => alpha
literal_vector lits;
lits.push_back(~lit);
lits.push_back(alpha_lit);
add_th_lemma(lits);
}
}
induction_lemmas::induction_lemmas(context& ctx, ast_manager& m):
ctx(ctx),
m(m),
m_dt(m),
m_a(m),
m_rec(m),
m_num_lemmas(0),
m_trail(m)
{}
induction::induction(context& ctx, ast_manager& m):
ctx(ctx),
m(m),
vs(m),
m_collect_literals(ctx, m, vs),
m_create_lemmas(ctx, m)
{}
// 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_expr()))
for (enode* r : *n)
if (r != n) {
vs.set_value(r->get_expr(), n->get_expr());
}
}
bool induction::operator()() {
bool added_lemma = false;
vs.reset_values();
init_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();
}