latest

Latest builds

5a7a3d2

cmake: Update versioning scheme (#12116)

The current versioning scheme follows the format:
```
<version-in-last-tag>-dev.<number-of-commits-since-last-tag>.<commit-sha>[-modified]
```
This leads to two main practical issues:

1. To retrieve `<number-of-commits-since-last-tag>`, a clone of the
repository with access to the full Git history is required. This is not
always desirable, since it introduces unnecessary overhead. For example,
the GitHub `checkout` action retrieves only the latest commit by
default. When this information is not available, the build system does
not include other useful details such as the branch name or commit SHA
in the `CVC5_GIT_INFO` constant.

2. Even when the full history is available, the list of tags may not be.
This is common when a user or developer works on their own fork of the
repository.

This PR changes the format to:
```
<latest-release-version>-dev.<branch-name>@<commit-sha>[-modified]
```
This makes the version scheme more robust when the Git history or list
of tags is not available.

In addition, this PR preserves the old behavior of incrementing the
patch version by one when a development version is detected.

ae2d768

Minor improvements to higher-order solver from mbqi enum choice branc…

f7db8fa

Do not introduce mixed arithmetic in transcendental proof rules (#12101)

Also adds a regression for `ARITH_TRANS_SINE_APPROX_BELOW_NEG`, which
was missing.

---------

Co-authored-by: Haniel Barbosa <[email protected]>

8aeaa19

Fix issue with ee-mode central with arrays (#11898)

The array theory requires explicitly being notified about disequalities
between arrays.

When ee-mode=central, we did not configure arrays to request these
notifications.

Fixes https://github.com/cvc5/cvc5/issues/11889.

e852a84

Introduced non-closed converter, more robust guard for non-closed ter…

802460d

Add proof elaboration for MACRO_BOOL_BV_INVERT_SOLVE (#11701)

8cfac8f

Generalize elaboration for quant prenex to handle nested cases (#11450)

The elaboration for MACRO_QUANT_PRENEX was incomplete since it did not
handle cases where prenexing was done in nested cases, e.g. `(forall x
(or (and (forall y P) Q) R) ---> (forall xy (or (and P Q) R))`.

This makes the elaboration take this into account, making use of the new
miniscoping rules.

cvc5

v0.0.1

Add missing internal-to-external mapping for BITVECTOR_BIT. (#10960)