4484 Commits

Author SHA1 Message Date
Andrew Reynolds
b886b61030 Disable regression (#12302)
Gives "unknown" on one build on nightlies.
2025-12-10 20:11:53 +00:00
Andrew Reynolds
6dd08fb064 Move shadow elimination to post-rewrite, guard variable elimination (#12288)
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.
2025-12-09 20:31:32 +00:00
Andrew Reynolds
05a9433b25 Fix issue with substitution context in strings extended function inference (#12292)
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.
2025-12-09 20:15:32 +00:00
Andrew Reynolds
e622d77107 Ensure integer constants are converted to rationals in numerator of division terms (#12294)
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.
2025-12-09 19:29:22 +00:00
Andrew Reynolds
74554ef170 Fix subtype elimination for ARITH_MULT_SIGN (#12275)
Fixes https://github.com/cvc5/cvc5-projects/issues/774.
Fixes https://github.com/cvc5/cvc5-projects/issues/775.

The conversion wasn't correct for monomials with duplicated variables.
2025-12-03 20:26:36 +00:00
Andrew Reynolds
5ddd4f098e Fix double negation handling in NNF proofs (#12276)
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.
2025-12-03 19:18:21 +00:00
Andrew Reynolds
f825b36f13 Fix issue with subtypes in NL comparison proofs (#12277)
Fixes https://github.com/cvc5/cvc5-projects/issues/772.

Note the benchmark times out so we set a tlimit on the regression.

---------

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2025-12-03 18:03:32 +00:00
Andrew Reynolds
b19989f56a Fix issue with duplicate proof steps in theory rewrite reconstruction (#12278)
Fixes https://github.com/cvc5/cvc5-projects/issues/771.
2025-12-03 16:50:54 +00:00
Andrew Reynolds
911d9b4b6a Apply extensionality eagerly to functions with HO arguments (#12265)
Fixes https://github.com/cvc5/cvc5/issues/12256.
2025-12-01 15:23:59 +00:00
Thomas Hader
3410dd348b Remove test when libpoly is not present. (#12250)
Fixes #12244

Co-authored-by: Thomas Hader <tom@hader.email>
2025-11-25 22:46:04 +00:00
Haniel Barbosa
076d065ea4 [proofs] Fix cyclic proof issue in EqProof conversion (#12266)
Sometimes the equality engine proof is silly in that an equality is
derived having itself as an assumption. While silly, this is not wrong,
but when building the proof, given the overwrite policy of assumptions,
this would lead to a cyclic proof.

A thorough way to avoid this issue is to not override assumptions, since
in this module assumptions are never supposed to be generated during
proof conversion other than original assumptions given to the module. So
this commit makes the construction of the proof more careful.

An alternative solution would be to guard the conversion in different
points to short-circuit cases in which you are rederiving something. But
this is error-prone and can be done in post-processing anyway.

Fixes #12240
2025-11-25 20:21:44 +00:00
Andrew Reynolds
e0ee808eee Fix cyclic arithmetic proof (#12264)
Fixes https://github.com/cvc5/cvc5/issues/12255.
2025-11-25 19:19:11 +00:00
Andrew Reynolds
3da5981987 More fixes for proof subtype elimination (#12228)
Encountered while doing more thorough testing of SMT-LIB.

Fixes https://github.com/cvc5/cvc5-projects/issues/770.

---------

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2025-11-25 18:05:51 +00:00
Andrew Reynolds
ff09969f7f Fix proof reconstruction for nctn rewrite with str.from_code (#12263)
Fixes https://github.com/cvc5/cvc5-projects/issues/768.
2025-11-25 17:00:54 +00:00
Andrew Reynolds
2397a0e2b4 Fix proofs of nl comparison with arithmetic subtyping (#12261)
Fixes https://github.com/cvc5/cvc5-projects/issues/767
Fixes https://github.com/cvc5/cvc5-projects/issues/769

Also fixes a discrepancy between the internal reduction for `/_total`
and the Eunoia signature.

---------

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2025-11-25 16:46:11 +00:00
Andrew Reynolds
37609cb737 Eliminate shadowing at prerewrite (#12258)
Fixes #12252.

Since variable elimination is not sound for quantified formulas with
shadowing, this PR simplifies how variable shadowing is handled by
eagerly eliminating it at prerewrite.

Generalizes the proof reconstruction for lambda shadow elimination to
handle this case.

An assertion had to be deleted in this PR since now we may do shadow
elimination with `exists`.
2025-11-24 23:23:56 +00:00
Andrew Reynolds
8c4803232f Fix ARITH_MULT_SIGN for mixed arithmetic (#12243)
Fixes https://github.com/cvc5/cvc5/issues/12239.

---------

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2025-11-24 22:38:40 +00:00
Andrew Reynolds
90ea47f5e1 Fix proofs in arithmetic congruence manager (#12260)
Fixes #12254.

Handles a corner case where the congruence manager finds a conflict
between `(= f 0)` and `(not (= (to_real f) 0.0))`.
2025-11-24 21:17:59 +00:00
Andrew Reynolds
6980d6ac7f Fix issue with proofs of length intro on non-ACI normalized strings (#12242)
Fixes #12241.
2025-11-24 20:29:20 +00:00
Daniel Larraz
17f380674b java: Store JNI library by OS and CPU architecture (#12237)
This PR builds and stores the JNI library in a directory structured
according to the OS and CPU architecture. This allows a single JAR to
contain native JNI libraries for multiple OSes and CPU architectures
simultaneously, and prevents file collisions when multiple JARs
containing a native JNI library for the same OS but different
architectures are added to the classpath.
2025-11-17 16:17:04 +00:00
Andrew Reynolds
c07c580542 Allow MBQI by terms with constant arrays when arraysExp is enabled (#12205) 2025-11-12 16:00:36 +00:00
yoni206
310f487e6a Basic Support for Logarithm with Base 2 (#12224)
This PR externalizes the INTS_LOG2 operator so that it can be used via
the API and textual interface.
For solving, we eliminate it in expand-definitions using int.pow2.

The cpc signature is updated to match the current semantics in cvc5,
namely: log2 of a negative number is 0.

Tests and traces are added, as well as minor fixes to existing comments.

---------

Co-authored-by: Yoni Zohar <yonizohar@Yonis-MacBook-Pro.local>
2025-11-11 17:52:25 +00:00
Andrew Reynolds
f70c183c0f Fix proofs for linear arithmetic conflicts that involve non-linear (#12227)
Since https://github.com/cvc5/cvc5/pull/12178, we allow linear
arithmetic to reason about non-linear terms in the DIO solver.

This was leading to crashes during proof production since we traversed
non-linear multiplication terms. The proof failures occur in two places:
the dedicated proof reconstruction for DIO lemmas and in the arithmetic
congruence manager.

This PR fixes theses issues by not traversing multiplication terms in
these contexts and adds regressions for the two cases.

It also makes the traversal policy for arithmetic substitutions more
consistent by treating non-linear kinds like IAND more uniformly.
2025-11-11 16:54:21 +00:00
Andrew Reynolds
724682fa53 Enable proof subtype elimination by default (#12198)
This enables `--proof-elim-subtypes` by default.

To do so, we make two changes:
1. Assertions given to the solver engine are processed by the subtype
elimination node converter. This means that if a user assertion used
mixed arithmetic, the proof will be in terms of a different preprocessed
form of that assertion. This change is necessary to ensure that proofs
do not contain mixed arithmetic (which cannot be avoided if the overall
assumptions have mixed arithmetic).

2. The subtype elimination node converter is relaxed so that real
division is overloaded (but not mixed). This change is motivated by the
fact that SMT-LIB rational constants are parsed as the real division of
integer constants and should not be considered as needing to be
processed by the subtype elimination node converter.

Also makes an optimization to the proof node converter to not update
proofs when it is unecessary to do so.
2025-11-07 14:44:25 +00:00
Andrew Reynolds
536a6a5c18 Do not split on infinite datatypes based on fmf option (#12218)
Previously our behavior was somewhat inconsistent: we would not split on
datatypes that had a possible constructor that was "interpreted finite"
(i.e. finite only when uninterpreted sorts are finite), even when finite
model finding is disabled (i.e. uninterpreted sorts are considered
infinite).

This updates the behavior to be more consistent: we do not need to split
on datatype terms that have a constructor that has infinite cardinality
based on the option.

This change leads to noticeably better performance on the verus set
(4.7% faster, +32-7 over a 60 second timeout).
2025-11-06 22:49:58 +00:00