Vehicle-lang

* Added functions `min` and `max` over rationals.

* Removed `Explicit` as a command line compilation target option as it never worked.

* Fixed bug where generated Agda files sometimes incorrectly said `Unable to read the verification cache from file`.

* Fixed spurious "Unnecessary resources provided" warning when exporting to ITPs.

* Drastically reduced memory consumption when compiling verification queries.

* Removed `Int` from the VCL language as not currently needed.

* Allow `parameter`s to be used as network sizes.

* More powerful index solver: `i` is now a valid index for vectors of size `n + 1 + i`.

* Fixed compilation bugs when using network outputs as inputs to higher order functions.

* More accurate error messages when the verifier is killed during verification.

* If during verification the verifier throws an error, Vehicle will now create a reproducer
automatically.

* Added new command-line option `--verifier-args` to `verify` mode that allows extra
arguments to be passed directly to the verifier.

* Fixed bug when reconstructing witnesses using Fourier-Motzkin elimination.

* Fixed bug properties involving the comparison of abstract `Index` values would throw
a `Something went wrong in query compilation` error.

* Added warnings to `compile` command when you hit Marabou bug
https://github.com/NeuralNetworkVerification/Marabou/issues/670

* Added warnings to `compile` command when not all input variables are well-constrained.

* In order to better follow the kebab-case conventions for command line arguments
the following command-line arguments have been renamed as follows:
- `outputFile` -> `output`
- `moduleName` -> `module-name`
- `verifierLocation` -> `verifier-location`

* Fixed bug where using `forall ... in` and `exists ... in` would sometimes throw
`unification of lambdas not implemented` error.

* When compiling a non-linear specification to verify queries, fixed the following bugs
with the non-linearity analysis:
- The presence of type-synonyms would cause the analysis to error.
- Using a linear quantity as the denominator of a division would sometimes cause the analysis to error.
- Using a linear quantity as the denominator of a division would sometimes display an erroneous error referencing a non-existent multiplication.

* Added warnings to `compile` command when unneeded resources are passed.

* Added warnings to `verify` command when properties are found to be trivial
(i.e. there was no need to call a verifier).

* Added warnings to `verify` command when properties require the mildly unsound
conversion of strict to non-strict inequalities.