TODO.txt

TODO:

- document :sorry in user manual.
- Add options --include=X --reference=X
  - remove reference command?
- `let` is never builtin, use alf.let
- A language can decide if its library is automatically included or not? Or done via include command.
  - Maybe for consistency we always include.
- weaker type system for program bodies?
- warn unused parameters
- don't always use mkExprInternal in evaluate (@lazyHash)
- fix printing decimals?
- define-fun-rec parsing
- set-option?
- quote function type
- RARE rules (@alfRare)


CVC5-TODO:

- define-fun-rec
- fine grained inclusion of signatures to avoid overloading
- set.insert
- ambiguous datatype constructors
- rewrite as a ALF proof rule
- minimize rewrite proofs? A = A' ^ B = true => (or A B) = true -----> B = true => (or A B) = true
- substitute as an ALF proof rule
- convert as an ALF proof rule


COMPLETED:

- datatypes
- literal ops to compiler
- auto-evaluate literal ops
- change syntax for nil, for eval.
- :restrict
- bitvectors
- datatype testers
- howto: bitvector literal type rule
- strings
- alf.ite smart evaluation, not just literals
- alf.is_eq not just literals
- change @ to _
- :requires for implicit is dropped, maybe simplify
- failures in side conditions?
- generalize CLI
- show compiled files via --show-config
- proper compilation of alf.ite / alf.is_eq
- alf.cons for list variables at non-tail locations
- ensure assumption scope level is preserved per include file
- X remove custom nil construction policy?
- separate symbol table for proof rules?
- type field separate from Expr? (to save memory)
- Temporary memory allocation of Expr within calls to evaluation?
- memory safe
- Literal inherits from ExprValue
- n-ary literal ops
- arity overloading?

- sorts introduced internally to proof (fmf-fun)
- INDEXED_ROOT_PREDICATE