mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

na

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-05-01 13:17:37 -07:00
parent 8dd522d805
commit c94a9e8ddd
2 changed files with 40 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

53
src/smt/smt_induction.cpp
View file

@ -105,33 +105,49 @@ literal_vector collect_induction_literals::operator()() {
// --------------------------------------
// create_induction_lemmas
bool create_induction_lemmas::is_induction_candidate(enode* n) {
app* e = n->get_owner();
if (m.is_value(e))
return false;
bool create_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 create_induction_lemmas::viable_induction_parent(enode* n) {
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 (o->get_family_id() == m.get_basic_family_id())
continue;
if (o->get_family_id() == m_rec.get_family_id()) {
in_good_context |= m_rec.is_defined(o);
continue;
}
if (o->get_family_id() == m_dt.get_family_id()) {
in_good_context |= m_dt.is_constructor(o);
continue;
}
}
if (!in_good_context)
return false;
return in_good_context;
}
// avoid recursively unfolding skolem terms.
if (e->get_num_args() > 0 && e->get_family_id() == null_family_id) {
bool create_induction_lemmas::viable_induction_term(enode* n) {
app* e = n->get_owner();
if (m.is_value(e))
return false;
}
sort* s = m.get_sort(e);
if (m_dt.is_datatype(s) && m_dt.is_recursive(s))
if (n->get_num_args() == 0)
return true;
// potentially also induction on integers, sequences
// m_arith.is_int(s)
// 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 create_induction_lemmas::viable_induction_position(enode* n) {
return
viable_induction_sort(m.get_sort(n->get_owner())) &&
viable_induction_parent(n) &&
viable_induction_term(n);
}
/**
* positions in n that can be used for induction
* the positions are distinct roots
@ -152,7 +168,7 @@ enode_vector create_induction_lemmas::induction_positions(enode* n) {
n = todo[i];
for (enode* a : smt::enode::args(n))
add_todo(a);
if (is_induction_candidate(n))
if (viable_induction_position(n))
result.push_back(n);
}
for (enode* n : todo)
@ -365,6 +381,7 @@ create_induction_lemmas::create_induction_lemmas(context& ctx, ast_manager& m, v
vs(vs),
m_dt(m),
m_a(m),
m_rec(m),
m_num_lemmas(0)
{}

6
src/smt/smt_induction.h
View file

@ -54,6 +54,7 @@ namespace smt {
value_sweep& vs;
datatype::util m_dt;
arith_util m_a;
recfun::util m_rec;
unsigned m_num_lemmas;
typedef svector<std::pair<expr*,expr*>> expr_pair_vector;
@ -82,7 +83,10 @@ namespace smt {
};
typedef vector<abstraction_arg> abstraction_args;
bool is_induction_candidate(enode* n);
bool viable_induction_sort(sort* s);
bool viable_induction_parent(enode* n);
bool viable_induction_term(enode* n);
bool viable_induction_position(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);