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.
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.
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
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`.
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.
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>
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.
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.
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).