This job seems redundant now, since we already have three jobs compiling
with Clang ("ubuntu:production-libc++",
"ubuntu:production-arm64-libc++", and "ubuntu:production-dbg-clang") and
one job that implicitly compiles without libpoly ("ubuntu:safe-mode").
This ensures compatibility for statically linking cvc5 with Lean
binaries on Windows for Lean versions 4.20 and above, as required by the
lean-cvc5 project.
This fixes a proof hole on SMT-LIB.
The PR https://github.com/cvc5/cvc5/pull/12258 recently applied shadow
elimination at prewrite. The motivation was to preemptively avoid
illegal variable eliminations. However, this is less efficient (includes
spurious alpha equivalence reasoning) and makes proof reconstruction
very difficult in rare cases, since we now must reason about more cases
in shadow elimination, including shadowing with duplicate variables.
We now move shadow elimination to post-rewrite, which avoids several
complications that are resolved bottom-up.
This furthermore properly guards variable eliminations to ensure that
substitutions are safe.
In the end this has the benefit that variable elimination is now safe
when taken as a standalone utility.
3 variants of the delta debugged regression are added.
Fixes https://github.com/cvc5/cvc5-projects/issues/776.
This updates the explanation mechanism for context dependent
simplification, to ensure substitutions whose LHS are concatention terms
are avoided.
Would otherwise lead to cyclic proofs, which cause the conversion proof
generator to fail.
The regression added required 2 RARE rewrites which were missing.
Fixes https://github.com/cvc5/cvc5-projects/issues/778.
The issue was caused by two rewritten literals (one with `(/ 2 a)` and
one with `(/ 2.0 a)`) being mapped to the same literal after subtype
elimination, which leads to a chain resolution step that failed due to
proving a stronger result than what was specified.
In general this indicates we need to ensure that subtype elimination is
a bijection over rewritten literals. This PR adds a rewrite to ensure
this is the case.
This PR moves the cross-compilation CI jobs out of the main workflow and
into a nightly scheduled one. Since native builds now cover all
supported platforms, cross-compilation testing is less critical. This
change streamlines CI and reduces cache contention.
The new artifacts simplify integrating the cvc5 library into
[lean-cvc5](https://github.com/abdoo8080/lean-cvc5), which requires cvc5
to be compiled with libc++.
This PR replaces the MSYS2 MINGW64 environment with the CLANG64
environment for compiling cvc5 natively on Windows x86_64. The main
difference between the two is that MINGW64 uses GCC and links against
libstdc++ and the MSVCRT runtime, whereas CLANG64 uses Clang and links
against libc++ and the UCRT runtime (see the MSYS2 [environment
documentation](https://www.msys2.org/docs/environments/) for details).
This ensures compatibility for statically linking cvc5 with Lean
binaries that use libc++ on Windows x86_64, thus facilitating the
integration of cvc5 into
[lean-cvc5](https://github.com/abdoo8080/lean-cvc5).
---------
Co-authored-by: Abdalrhman Mohamed <abdoo8080@outlook.com>
This PR is the sequel of https://github.com/cvc5/cvc5/pull/12245
It adds more implementations in the Piand solver.
The next PR will provide additional implementations of lemmas in the
Piand solver.
---------
Co-authored-by: Zvika Berger <zvbe@example.com>
This is the reason why #12285 was failing. `visit` is a vector of
`TNode`, however, `impl` are nodes created while traversing and pushed
on the `visit` stack, which can go out of scope while `visit` not
holding a reference due to `TNode`.
The new version of the `cibuildwheel` action uses the final CPython
3.14.0 release to build wheels for that version, rather than a release
candidate, although using the candidate release should still produce
ABI-compatible wheels.
Fixes https://github.com/cvc5/cvc5-projects/issues/773.
Double negation was handled lazily in NNF by deferring further rewriting
to another call to NNF.
This policy could lead to inconsistent proofs if there were further NNF
steps that were processed in the current rewrite and within the formula
that was deferred.
This ensures we process NNF on the doubly negated formula in the same
rewrite step, thus correcting the inconsistency in proof reconstruction.
This modifies the TheoryModel class so that models for functions are
computed on demand.
It also modifies the FMF module to compute function values when it is
invoked.
The motivation for this change is efficiency, as it function values are
not essentially in most cases during solving (apart from HO logics, and
when using mbqi or fmf), and moreover take significantly long time to
generate for large benchmarks. The performance overhead is particularly
in combination with lazy distinct handling (which requires models).
Using lazy function models reduces the overhead on a verification set of
interest from ~20% to ~4% with this PR.
This PR removes now obsolete methods that have been moved/updated in
TheoryModel.
---------
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
Reported by Jibiana Jakpor.
The rule `str-indexof-contains-concat-pre` was introduced recently in
https://github.com/cvc5/cvc5/pull/12174, which had a typo.
The other rule `str-indexof-contains-pre` is only sound if the string to
find is non-empty.
