Cvc5

==========

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

==========

New Features

- **API**
+ New API function `Solver::mkFloatingPoint(const Term& sign, const Term& exp, const Term& sig)`,
returns a floating-point value from the three IEEE-754 bit-vector value.
+ Added support for querying the values of real algebraic numbers in the API.
In particular, the methods
`Term::isRealAlgebraicNumber()`,
`Term::getRealAlgebraicNumberDefiningPolynomial()`,
`Term::getRealAlgebraicNumberLowerBound()`, and
`Term::getRealAlgebraicNumberUpperBound()` may now be used to query the
contents of terms corresponding to real algebraic numbers.

- Support for timeout cores
* **API**
+ New API function `Solver::getTimeoutCore()` when applicable returns a
subset of the current assertions that cause the solver to timeout without
a provided timeout (option `--timeout-core-timeout`).
* **SMT-LIB**
+ New command `(get-timeout-core)` which invokes the above method.

- Support for new interfaces to the SyGuS solver.
* **API**
+ New API function `Solver::findSynth` which takes an identifier specifying
a target term to synthesize and (optionally) a grammar. This method can
be used to directly enumerate terms in a provided grammar
(`FindSynthTarget::ENUM`), or as a way of finding other terms of interest,
e.g,. a rewrite rule that is applicable to the current set of assertions
(`FindSynthTarget::REWRITE_INPUT`).
+ New API function `Solver::findSynthNext` which gets the next term in the
enumeration.
* **SMT-LIB**
+ New commands `find-synth` and `find-synth-next` which invoke the above
methods.

Changes

- Removed support for the ANTLR parser and parsing for the TPTP language.
components.
- **API**
+ Simplified the `Solver::mkTuple` method. The sorts of the elements no longer
need to be provided.
+ Option `--print-unsat-cores-full` has been renamed to `--print-cores-full`.
Setting this option to true will print all assertions in the unsat core,
regardless of whether they are named. This option also impacts how timeout
cores are printed.
+ Removed API support for the deprecated SyGuS 2.0 command `Solver::synthInv`.
This method is equivalent to `Solver::synthFun` with a Boolean range sort.

==========

New Features

- A new (hand-written) parser is available and enabled by default.
* **Note**: the previous parser can be enabled using command line options
`--no-flex-parser --no-stdin-input-per-line`. These options will be
available until version 1.1 is released.

==========

New Features

- Support for the theory of (prime-order) **finite fields**:
* Sorts are created with
* C++: `Solver::makeFiniteFieldSort`
* SMT-LIB: `(_ FiniteField P)` for prime order `P`
* Constants are created with
* C++: `Solver::makeFiniteFieldElem`
* SMT-LIB: `(as ffN F)` for integer `N` and field sort `F`
* The operators are multiplication, addition and negation
* C++: kinds `FF_MUL`, `FF_ADD`, and `FF_NEG`
* SMT-LIB: operators `ff.mul`, `ff.add`, and `ff.neg`
* The only predicate is equality

==========

New Features

- **API**
* New API function `Solver::getVersion()`, returns a string representation
of the solver version.
- Support for **bit-vector overflow** detection operators:
* `BITVECTOR_UADDO` unsigned addition overflow detection
* `BITVECTOR_SADDO` signed addition overflow detection
* `BITVECTOR_UMULO` unsigned multiplication overflow detection
* `BITVECTOR_SMULO` signed multiplication overflow detection
* `BITVECTOR_USUBO` unsigned subtraction overflow detection
* `BITVECTOR_SSUBO` signed subtraction overflow detection
* `BITVECTOR_SDIVO` signed division overflow detection
- Support for **Web Assembly** compilation using Emscripten.

Changes

- The (non-standard) operators `BITVECTOR_TO_NAT` and `INT_TO_BITVECTOR` now
belong to the UF theory. A logic that includes UF is required to use them.
- The sort for (non-standard) bit-vector operators `BITVECTOR_REDAND` and
`BITVECTOR_REDOR` is now `(_ BitVec 1)` (was Boolean), following the
definition of reduction operators in Verilog (their origin).
- Reenable functionality that allows `(get-model)` commands after answering
`unknown` when `:produce-models` is set to `true`. Note that there is no
guarantee that building a model succeeds in this case.