Cvc5

==========

New Features

- Added support for **nullable** sorts and lift operator to the theory of **datatypes**.
- Adds a new strategy `--sub-cbqi` (disabled by default) for **quantifier
instantiation** which uses subsolvers to compute unsat cores of instantiations
that are used in proofs of unsatisfiability.

Changes

- SAT clauses are no longer marked as removable in MiniSat. This change
**improves performance** overall on quantifier-free logics with arithmetic and
strings.
- **API**
* Functions `kindToString(Kind)` and `sortKindToString(SortKind)` are now
deprecated and replaced by `std::to_string(Kind)` and
`std::to_string(SortKind)`. They will be removed in the next minor release.
- Minor changes to the output format for proofs. Proofs in the AletheLF
proof format generated by cvc5 now correspond directly to their representation
in proof objects obtained in via the API (the `Proof` class). Moreover,
proofs now use SMT-LIB compliant syntax for quantified formulas and unary
arithmetic negation.
- The option `--safe-options` now disallows cases where more than one regular
option is used.
- Fixes the parsing of `define-fun-rec` and `define-funs-rec` in interactive
mode.
- Renamed `bag.duplicate_removal` to `bag.setof`.
- Improvements to handling of constant production rules (`Constant`) in SyGuS
grammars.

==========

New Features

- Added support for **forward declarations** (feature `:fwd-decls`) in **SyGuS**
inputs. This allows functions-to-synthesize to include previous
functions-to-synthesize in their grammars. This feature is enabled by default
for all SyGuS inputs.

Changes

- Fixed a bug when piping input from stdin, which caused cvc5 to have degraded
performance. This bug could also cause cvc5 to throw spurious parser errors.

==========

New Features

- **API**
* The **signature** of functions `Solver::mkFiniteFieldSort(const std::string&)`
and `Solver::mkFiniteFieldElem(const std::string&, const Sort&)` is now
extended with an additional (optional) parameter to
`Solver::mkFiniteFieldSort(const std::string& size, uint32_t base)` and
`Solver::mkFiniteFieldElem(const string& value, const Sort& sort, uint32_t base)`
to configure the base of the string representation of the given string
parameters.
* A **new API for proofs** is available. The new `Proof` class represents a node
of the proof tree. Function
`Solver::getProof(modes::ProofComponent c = modes::ProofComponent::FULL)`
returns the root proof nodes of a proof component as a vector. Function
`Solver::proofToString(std::vector<Proof> proof, modes::ProofFormat format, modes::ProofComponent component)`
can be used to print proof components to a string with a specified proof
format.
* Added support for **parsing** inputs from file, string, or input stream. We
provide an `InputParser`, `SymbolManager`, and `Command` class for reading
inputs (see `include/cvc5_parser.h`). Example use cases of these classes
are available at https://cvc5.github.io/docs/cvc5-1.1.1/examples/parser.html
and https://cvc5.github.io/docs/cvc5-1.1.1/examples/parser_sym_manager.html.
These interfaces are also available in the Java and Python APIs.
* Added a variant of **timeout cores** that accepts a set of assumptions. This
is available via the API method `Solver::getTimeoutCoreAssuming` or the
SMT-LIB command `get-timeout-core-assuming`, which accept a list of
formulas to assume, while all current assertions are implicitly included
in the core.
* Add new method `Solver::getUnsatCoreLemmas` which returns the set of theory
lemmas that were relevant to showing the last query was unsatisfiable. This
is also avialable via the SMT-LIB command `get-unsat-core-lemmas`.

- Support for the **AletheLF (ALF) proof format**. This format combines the
strengths of the Alethe and LFSC proof formats, namely it borrows much of the
syntax of Alethe, while being based on a logical framework like LFSC.
* **API**
+ The option `--proof-format=alf` prints proofs in the AletheLF format.
This option is enabled by default.
* The ALF proof checker (alfc) is available for download via the script
`./contrib/get-alf-checker`.

- **CaDiCaL** is now integrated via the IPASIR-UP interface as **CDCL(T) SAT
solver**. The CDCL(T) SAT solver can be configured via option `--sat-solver`.
Currently, MiniSat is still default. Note that CaDiCaL cannot be used as the
CDCL(T) SAT engine when proof production is enabled. In that case, option
`--sat-solver` will default back to MiniSat.

Changes

- Various bug fixes.

==========

Note: This is a pre-release version for the upcoming version 1.1.0.

New Features

- **API**
+ Add the ability to query the logic that has been set in the solver via
`Solver::isLogicSet` and `Solver::getLogic`.

Changes

- **SMT-LIB**
* The syntax for 0-ary tuples has been changed for the purposes of
disambiguation. The new syntax for 0-ary tuple sort is `UnitTuple` whose
0-ary constructor is `tuple.unit` (the previous syntax had overloaded
`Tuple` and `tuple`, with no arguments).

==========

Note: This is a pre-release version for the upcoming version 1.1.0.

Changes

- **API**
+ C++ enums are now enum classes
+ Added argument `fresh` to `Solver::declareFun` which distinguishes whether
the solver should construct a new term or (when applicable) return a
term constructed with the same name and sort. An analogous flag is added
to `Solver::declareSort`. The option `--fresh-declarations` determines
whether the parser constructs fresh terms and sorts for each declaration
(true by default, which matches the previous behavior).

==========

Changes

- Various bug fixes