Choosing which formulas and terms to encode

[Vtec234]

@abdoo8080 and I discussed recently when terms should be encoded with their definition, and when just declared. Here is a proposal for how the tactic could behave. It is almost what it does now, except that I suggest we do encode all assumptions in default mode and move the current behavior to smt only.

• With smt, we encode every assumption and declare-fun/declare-const every constant appearing in the assumptions and goal.
• With smt [thm1, def1], we proceed as above but also encode thm1, and instead of just declaring occurrences of def1 we define them.
• With smt only [h1, thm1, def1], we proceed as the tactic currently does by only declaring the minimal set of terms and skipping assumptions other than h1.

What are your thoughts?

[abdoo8080]

Your proposal looks reasonable to me. However, at its current state, the tactic will most likely crash on any reasonable proof context 😅. Properly handling all of those crashes is not a priority for us right now. So, let's keep the current behavior for now and come back to this issue when we have a more robust tactic.