Cvc5

==========

New Features

- New **C API**, implemented as a thin wrapper around the C++ API.
- Documentation: https://cvc5.github.io/docs-ci/docs-main/api/c/c.html
- Examples: https://github.com/cvc5/cvc5/tree/main/examples/api/c

- Exposed creation and maintenance of **Skolem functions** to the API. Skolem
functions are symbols that are internally introduced by cvc5 during solving.
They are formalized via an identifier (see
https://cvc5.github.io/docs-ci/docs-main/skolem-ids.html for details) as well
as a (possibly empty) set of indices.
+ The **API** methods `Term::isSkolem()`, `Term::getSkolemId()`, and
`Term::getSkolemIndices()`may now be used to identify terms corresponding
to skolems.

- We now export kinds `BITVECTOR_FROM_BOOLS`, `BITVECTOR_BIT`, `DIVISION_TOTAL`,
`INTS_DIVISION_TOTAL`, `INTS_MODULUS_TOTAL` which may appear in terms
resulting from simplification or terms appearing in proofs.

- Proof rules corresponding to rewrite rules are now exported in the API via
the enum `ProofRewriteRule`.

- A new `Plugin` class is available in our API. This class allows a user
to be notified when SAT clauses or theory lemmas are learned internally
by cvc5. The plugin class also contains a callback for the user to introduce
new learned clauses into the state of cvc5 during solving.

- Added a new strategy `--mbqi-fast-sygus` (disabled by default) for **quantifier
instantiation** which uses SyGuS enumeration to augment instantiations from
model-based quantifier instantiation.

Changes

- We now require CMake >= 3.16.

- **API**
All APIs have been refactored to expose a TermManager to the API. A term
manager manages creation and maintenance of all terms and sorts (across
potentially several solver instances within a thread).
Corresponding functions that were previously associated with a solver
instance and are now associated with a term manager are now deprecated
and will be removed in a future release.
* Python:
- Constructor `SymbolManager(Solver)` is now deprecated and replaced
by `SymbolManager(TermManager)`.
* Pythonic:
- Unsat cores and proofs are now available via the `Solver` methods
`unsat_core()` and `proof()`, respectively.

- The default proof format of cvc5 has been renamed to the
**Cooperating Proof Calculus (CPC) proof format**. This proof format coincides
with proof objects in our API.
* **API**
+ The option `--proof-format=cpc` prints proofs in the CPC format.
This option is now enabled by default.
* The **Ethos** proof checker is available, which can check proofs in this
format. In particular, the 0.1.0 release of Ethos can check proofs generated
by this version of cvc5. This checker is the second generation of the
AletheLF checker (`alfc`). Ethos inherits the code base of alfc and is based
on a logical framework called **Eunoia** (formerly called AletheLF).
See https://github.com/cvc5/ethos for more details. Note that the
development version of Ethos is available for download via the script
`./contrib/get-ethos-checker`, which will be kept in sync with further
development versions of cvc5.
* The rules of this format have been formalized in Eunoia and are available
in the cvc5 repository under the directory `./proofs/eo/cpc/`.

- The semantics of `SQRT` was changed to assume the result is positive.

- Fixed a bug involving how sequence terms are printed in model values.

==========

New Features

- Added support for **nullable** sorts and lift operator to the theory of
**datatypes**.

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

- Add support for the kind `BITVECTOR_NEGO` corresponding to bitvector
negation overflow detection.

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.
* Added 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**
+ Added 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).