Module-level options

[zafer-esen]

(Detailed description to be added.)

This branch adds more module-level attributes (defaults are for 4.3):

• {:type_encoding "a" | "m" | "p") (default "a")
• {:prune "1" | "0"} (default "1")
• {:solver "cvc5" | "z3" | "yices2"} (default "z3")
• {:native_seq} use the native theory of sequences (default axiomatization)
• {:no_lit} completely turns off Lit functions for this module.
• {:isolate_assertions} same as {:vcs_split_on_every_assert} but at module level.
• {:prover_opt value} where value is any Z3 parameter (not tested with other solvers).
  • For instance: {:prover_opt smt.case_split:2}

Since the idea of this branch was to optionally enable/disable other changes, it includes work from other branches & PRs:

• Split prelude axiomatizations and native theory mode for sequences #4537 which in turn includes Monomorphize collection types #4535.
• Reduce Lit function usage where possible #4596 (not strictly necessary)
• Apply simplification to Imp and Iff connectives #4533 (not strictly necessary)

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.