feat(library/tactic): polish tactic API, and add new example showing how to implement tactics using Lua

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(util/luaref): warnings produced by valgrind

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/tactic): memory leaks

Proof/Cex builders and tactics implemented in Lua had a "strong reference" to script_state. If they are stored in the Lua state, then we get a cyclic reference.
That is, script_state points to these objects, and they point back to script_state.

To avoid this memory leak, this commit defines a weak reference for script_state objects. The Proof/Cex builders and tactics now store a weak reference to the Lua state.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/rewriter): unused variable warnings
feat(util/list): filter template

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(util/list): map_append template

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(util/name_set): add mk_unique (with respect to a name_set)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic): add focus tactical

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
doc(library/rewriter): add doxygen annotations for rewrite_* funcs
chore(.gitignore): update .gitignore
refactor(library/rewriter): move apply_rewriter_fn into rewriter.h
feat(library/rewriter): implement depth RW
refactor(library/rewriter): rename lc => ti
test(library/rewriter): add test for depth RW
feat(library/tactic): add disj_hyp_tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic): add absurd_tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/tactic): remove duplicate code, add add_proofs

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(util/list): bug in map template

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic): add unfold tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/hidden_defs): hidden definitions are just hints for tactics and solvers

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>