Generate named SMT database when defining inductive predicates

[fdupress]

The database for an inductive indpred would include the indpred_ind principle, and the per-constructor lemmas, and could be used as smt(@indpred_smt) (for example).

This is to make rapid exploration possible when defining complex invariants as inductive predicates.

[strub]

By constructor lemmas, you mean injectivity/non-confusion?

[fdupress]

No. I mean, given

inductive popo x =
| Foo of (P x).

The lemma that says forall x, P x => popo x.

[strub]

In fact, inductive predicates are sent as abstract predicates to SMT solvers. Does not seem optimal to me.