Roadmap (Summer 2024 and beyond)

[elsoroka]

Development Roadmap for Summer 2024 and beyond

Minor features:

• Add support for unicode #44
• Automatically download Z3 if not already installed #43

Expanding capabilities:

• Support for quantifiers #31. probably less difficult than Improvements to @uninterpreted functions #11.
• Improvements to @uninterpreted functions #11. This will probably involve work with metaprogramming to get right and need good unit testing.
• Completing the following three will take us to a milestone: all SMT-LIB theories supported. For each of these issues, a separate ticket should be created with a checklist for developing, testing, and documenting this feature.
  • Add SMT-LIB theory of floating point numbers https://smt-lib.org/theories.shtml
  • Add SMT-LIB theory of arrays https://smt-lib.org/theories.shtml
  • Add SMT-LIB theory of strings https://smt-lib.org/theories.shtml
• [ ]

New features:

• Infer logic type from expression #24. This should be straightforward to implement but requires understanding the logic types. Type promotion rules could be useful to encode the (https://smt-lib.org/logics.shtml)[hierarchy of logic types].