Vehicle-lang

* 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.

* Fixed bug in display of progress bar when verification counter-example found.

* Fixed bug where `forall ... in` and `exists ... in` didn't evaluate properly during verification
(introduced in v0.9.0).

* Improved precision of constants in the verifier queries generated.

* Removed the notion of a distinct notion of a "proof cache".
Instead, the folder of verification queries generated by Vehicle serves as the proof cache.
As part of this, the `--proofCache` argument for the command-line modes `export` and `verify`
has been renamed `--cache`.

* After performing verification, Vehicle now writes out the witnesses and counter-examples found
by the verifier to `.idx` format files within the verification cache.

* Exposed `verify` mode functionality in Python via the `verify` function in the `vehicle_lang`
module (however, counter-examples are not yet provided.)

* Loss functions no longer generated via the `to_python` function from `vehicle_lang.compile`
module, but instead can be created via the `load_loss_function` function from the
`vehicle_lang` file.

* Fixed bug where Vehicle would run out of memory when compiling a specification with many
individual sub-properties (e.g. robustness).

* Fixed bug in `verify` mode where disjunctions in properties without top-level quantifiers
were being incorrectly translated.

* Fixed bug in `verify` mode where incorrect equations were generated if quantified variables
had non-unit coefficients when expressed in terms of network inputs.

* Fix various bugs in the loss function backend.

* Expose `LOSS_VEHICLE` logic in the tensorflow loss function bindings.

* When calling loss functions, no longer need to have individual `()` call
for each argument. Instead can use named arguments, e.g. for mnist spec:
python
lossFn(
n=1,
classifier=classifier,
epsilon=0.001,
trainingImages=(ZEROES_28X28,),
trainingLabels=(0,),
)