feat: implement all "main" features from the solver API, related tests, document missing features in README

README.md

@@ -7,10 +7,6 @@ cvc5 solver in Lean. It was designed to support the needs of the
 [lean-smt] tactic. The FFI allows Lean programs to interact
 with cvc5 by calling its functions and accessing its API.
 
-## Limitations
-
-- Minimal interface to the cvc5 solver (contributions are welcome!)
-
 ## Getting Started
 
 To use `lean-smt` in your project, add the following lines to your list of
@@ -38,6 +34,24 @@ your system. If you are using Windows, you need to have `clang` and `libc++`
 (version 19) installed on your `MSYS2` environment. Build this library by running
 `lake build` in the root directory of the project.
 
+## Missing features
+
+Term API:
+
+- [`getStringValue`](https://github.com/cvc5/cvc5/blob/cf59add20e053647145edb5f8151a2785c1d703e/include/cvc5/cvc5.h#L1600-L1607)
+
+Solver API:
+
+- [statistics](https://github.com/cvc5/cvc5/blob/cf59add20e053647145edb5f8151a2785c1d703e/include/cvc5/cvc5.h#L3410-L3425)
+- [option info](https://github.com/cvc5/cvc5/blob/cf59add20e053647145edb5f8151a2785c1d703e/include/cvc5/cvc5.h#L3240-L3279)
+- [driver options](https://github.com/cvc5/cvc5/blob/cf59add20e053647145edb5f8151a2785c1d703e/include/cvc5/cvc5.h#L3211-L3223)
+- [plugins](https://github.com/cvc5/cvc5/blob/cf59add20e053647145edb5f8151a2785c1d703e/include/cvc5/cvc5.h#L3616-L3619)
+
+Input parser:
+
+- [`setStreamInput`](https://github.com/cvc5/cvc5/blob/cf59add20e053647145edb5f8151a2785c1d703e/include/cvc5/cvc5_parser.h#L251-L259)
+- [dedicated parser errors](https://github.com/cvc5/cvc5/blob/cf59add20e053647145edb5f8151a2785c1d703e/include/cvc5/cvc5_parser.h#L348-L352)
+
 ## Contributing
 
 Contributions to the Lean cvc5 FFI project are welcome! If you would like to contribute, please