Support for Offset Equalities - #156
Open
jhoenicke wants to merge 75 commits into
Open
Conversation
Add the data-structure foundation for offset (affine) equality classes in congruence closure, where a class member t satisfies t == rep + offset rather than t == rep. This is increment 1 of the offset-equality plan: it threads the offset through the union-find but creates no non-zero offsets yet, so behavior is preserved (every offset is ZERO and the structure degenerates to plain congruence closure). - CCTerm: add mOffsetToRep; thread the offset delta through mergeInternal and undoMerge, add the same-class offset-consistency check in merge (the x = x+1 conflict case, explanation stubbed until the proofs increment), a reasonDiff helper, and a rep-offset-is-zero invariant. - CCEquality: add mOffset (lhs == rhs + offset) with accessor/setter/toString. - CCAppTerm: add the nullable mArgOffsets array and getArgOffset. - doc/offset-equality-plan.md: design and increment plan. Full test suite passes unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Make SignatureTrigger key on each argument's effective offset (the term's offset to its representative plus the structural argument offset) in addition to the representative, so two function applications are congruent only when their arguments have the same representative and the same offset. Thread the offset delta through recomputeHashCode/rehash/rehashSignatures and the merge/undoMerge callers. CongruenceTrigger picks up the structural offsets from its app term; FindTriggerTrigger (no terms) and ReverseTriggerTrigger (no structural offset) are unaffected. This is increment 2a of the offset-equality plan. No creation site emits non-zero offsets yet, so every effective offset is ZERO and the change is a no-op; the full test suite passes unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Make CCTermPairHash.Info carry an offset so that several infos with the same endpoints but different offsets can coexist (e.g. for a == b and a == b + 5). The offset enters the cuckoo-hash key via an offset hash that is invariant under negation, so (A, B, off) and its mirror (B, A, -off) still hash and compare equal; equals() and getInfo() take the offset into account. To keep the change minimal and behavior-preserving, zero-defaulting overloads Info(l, r) and getInfo(l, r) are provided, so every existing call site continues to query offset zero unchanged. Threading the context-derived offsets through the individual call sites (insertEqualityEntry, isDiseqSet, separate, the merge-time propagation, etc.) is deferred to the creation increment, where it is exercised end-to-end. At zero offset the offset hash contribution is zero, so the hash values are identical to before. This is increment 2b of the offset-equality plan. Full test suite passes unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The offset hash was made invariant under negation, which also made (a, b, off) and (a, b, -off) — i.e. a = b + off and a = b - off — collide. That is a structured collision cuckoo hashing handles badly. Instead express the offset in a canonical endpoint orientation before hashing, so the mirror (b, a, -off) still matches but off and -off are distinguished. The orientation uses CCTerm.hashCode() (deterministic) rather than System.identityHashCode(), to keep the solver reproducible. On the rare event that the two endpoints have equal hash codes, the orientation is ambiguous, so we fall back to the negation-invariant offset.abs() hash. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This is increment 3 of the offset-equality plan: the feature is now active and exercised end-to-end (the full test suite runs with it enabled, since it is on for non-proof runs). - Flag createOffsetEqualities() on CClosure (= !isProofGenerationEnabled()). - Clausifier/CCTermBuilder: build offset-free CCTerms for numeric terms, keyed on the offset-free affine, carrying the constant as an offset; LASharedTerm becomes offset-free (offset zero) and is shared with linear arithmetic only once (the share() guard prevents re-sharing a CCTerm several offset terms map to). createAppTerm records per-argument offsets (mArgOffsets). - EqualityProxy: derive the CCEquality offset from the difference of the two terms' constants. - CClosure/CCTerm: thread the context-derived offset through insertEqualityEntry (chain walk), createCCEquality, isDiseqSet, separate/undoSep, backtrackComplete, removeCCEquality, and the mergeInternal/undoMerge pair-hash re-keying and propagation (propagate equalities at the matching offset). setLiteral detects the same-class offset conflict (x == x + 1). - Shared-term equality propagation (mergeInternal, propagateSharedEquality) now carries the offset: createEquality encodes value(t1) == value(t2) + offset by building the rhs term t2+offset, so the CCEquality carries the offset and the linked LAEquality the matching constant. - ModelBuilder: a class member's model value adds its offset to the representative, the representative's value subtracts the shared term's offset, and function-application keys/values include the argument and term offsets. - Debugging aids: M/U merge logs and dumpModel print offsets. Proof generation stays on the offset-free path (flag off under proofs) until the next increment. Full test suite passes with offsets enabled. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…cture The shared-term equality propagation built the right-hand term as a nested (+ t2 offset). When t2 is itself a normalized sum (e.g. k - 256*(div k 256)), Polynomial re-parses that inner sum as a single opaque monomial, so the derived LAEquality dropped the summands (turning k mod 256 = 1 into a bogus k = 1) and produced spurious unsat (e.g. bv/test04.smt2). Build the right-hand term as a single flattened polynomial term via the new Clausifier.addConstantToTerm (unifyPolynomial(Polynomial(t2) + offset)) so the equality re-parses with all summands intact. Also print argument offsets in CCAppTerm.toString to make offset terms legible in debug output. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
E-matching binds quantifier variables to offset-free CCTerms (GetArgCode reads the offset-free argument), losing the constant offset: matching a(x) against the ground term a(l+1) instantiates x := l instead of x := l+1, so the conflict instance is never produced and an unsat problem is reported sat (quantified/quanttest001.smt2). Gate createOffsetEqualities() on mQuantTheory == null, mirroring the existing quantifier check in isBasicStablyInfinite. Quantifier-free problems keep offsets; quantified problems use the offset-free-less path. Offset-aware e-matching is future work for when the quantifier theory is reworked. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ashing Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Introduce CCParameter, an interface for "a value up to a constant" used wherever a function-application argument, array index or congruence argument is handled once offsets exist. A bare CCTerm is a CCParameter with offset zero (no wrapper allocated in the common case); OffsettedCCTerm carries a non-zero offset. CCParameter.of canonicalizes (offset zero -> bare CCTerm). Value identity is (getRepresentative(), getOffsetToRep()); use sameValueAs for comparison. Purely additive; no behavior change yet. Consumers (CClosure lookups, DataTypeTheory, ArrayTheory) will be migrated to use it. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The congruence sanity check compared application arguments by representative only; with offsets two applications are congruent only when their arguments have the same value (representative AND offset). Compare via CCParameter.sameValueAs. (getCCTermRep and getAllFuncApps need no change: getCCTermRep is only called from the quantifier theory, where offsets are disabled, and getAllFuncApps keys solely on the function symbol so it is offset-agnostic.) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…p keys getValueKey() builds a canonical value-identity key from the representative, so a plain HashMap keyed on it distinguishes values by (representative, offsetToRep): a bare representative CCTerm for offset zero, an OffsettedCCTerm(rep, offset) otherwise (whose structural equals/hashCode then coincide with value identity). Intended for the array theory's index maps, rebuilt per merge. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Array indices are now values up to a constant. Every index is read as a CCParameter (getIndexParamFromSelect/getIndexParamFromStore = argument 1 plus its structural offset), and all index-keyed maps/sets key on the value identity getValueKey() (representative + offset-to-rep) instead of the bare representative: ArrayNode.mSelects, the makeWeakRepresentative/mergeWith working maps, merge's seenIndices, the Cursor store-index sets, computeWeakeqExt's nodeMapping and the weakeq-ext inverse map, and mArrayModels. Index comparisons use sameValueAs / .equals(valueKey). This is sound because the array theory rebuilds its weak-equivalence structures from scratch on every index merge, so the value keys are a stable snapshot for the duration of a buildWeakEq/computeWeakeqExt pass. Index disequality literals in array lemmas are offset-aware: createIndexEquality (ArrayTheory) and computeIndexDiseq (WeakCongruencePath) build the literal via createEquality(t1, t2, offset, ...) with offset = storeIdx.offset - readIdx.offset, and drop the always-false disjunct when the two indices share a CCTerm but differ by a constant. Store indices for the lemma are collected as full parameters (raw term + structural offset), not value keys, so the generated literal coincides with the asserted atom rather than one on the index representative. WeakCongruencePath navigates by value key; its computePath calls only collect reason atoms along the union-find walk (matched indices always share a representative), so the clause is sound. The net path offset matters only for the proof object, which is disabled while offsets are on; WeakSubPath.mIdx stays a bare CCTerm for that (offset-disabled) annotation. ModelBuilder gains getModelValue(CCParameter) so array models store at the true index value (representative value + offset), not the representative's value. This fixes a wrong model on array/difftest004 (the @diff index offset was dropped) and the array/weakeq-ext crashes (nia/divaxiom2, abv/ext02). System-benchmark failures drop from 6 to 5 with no new failures; the remaining unsat->unknown cases stem from the still-open LA->CC offset propagation gap. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Record completion of gap 1 (the array index migration, incl. WeakCongruencePath and ModelBuilder.getModelValue) and update the resume point and remaining-gap list. System failures are now bv/test01 and abv/indexInRange01 (both unsat->sat, pre-existing, from the LA->CC offset propagation gap), which is the next target. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…rg view Consolidate the hand-rolled CCParameter.of(getArgument(i), getArgOffset(i)) into a single CCAppTerm.getArgParam(i) accessor, giving the uniform "an argument is a value up to a constant" view at the API boundary. ArrayTheory's index helpers and CClosure.checkCongruence now route through it. This keeps the internal storage as parallel CCTerm[]/Rational[] arrays (null in the offset-free case): the argument array is shared between CCAppTerm and its CongruenceTrigger, getArguments() returns a CCTerm[] consumed by the proof, path and model code, and Java array covariance would force a fresh allocation in the offset case for a CCParameter[] field. The parallel-array form is the right internal representation for the flat congruence engine; CCParameter is the right abstraction only at the consumer boundary. Behavior-preserving. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Record the gap-2 investigation: the LA side (non-constant fingerprint bucketing + offset equality propagation via EqualityProxy) is small and fixes bv/test01 and abv/ext02, but it exposes that CC's offset-conflict explanation is incomplete - computeAntiCycle's same-class assertion fires, and CongruencePath is offset-blind so the reconstructed conflict path is inconsistent (plus gap 3, eager same-class propagation). Gap 2 must therefore be done together with increment 4 (offset-aware CongruencePath / conflict explanation) and gap 3, not as a standalone change. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…handling
Implements gap 2 (LA->CC offset-equality propagation) together with the offset-
aware congruence-closure disequality handling it requires (gaps 3 + the conflict
explanation).
LinArSolve.propagateSharedEqualities now keys the shared-term fingerprint on its
non-constant part when offset equalities are enabled, and on a collision propagates
value(a) == value(b) + k as an offset CCEquality via a generalized
propagateSharedEquality (building rhs + k through EqualityProxy, which already
derives the CCEquality offset and links the LAEquality). A true-proxy guard skips
the tautology between two distinct constant terms. When offsets are off the
constant stays in the key, so the classic equal-value bucketing is unchanged.
On the CC side, a merge now propagates the disequality for eqlits whose offset
differs from the merge offset (CCTerm.mergeInternal), mirroring the existing
matching-offset true propagation. The conflict/explanation machinery is made
offset-aware:
- CClosure.computeAntiCycle and CongruencePath.computeAntiCycle explain an offset
disequality whose two sides are in the same class at a different offset via the
path between them ({not eq, not path}), instead of the offset-0 temporary-merge
trick which cannot work once the classes are already merged;
- setLiteral's same-class "assert eq while offset differs" conflict uses the same
{not eq, not path} form (computeCycle would emit a satisfied clause);
- getPropagatedLiteral computes a propagated disequality's explanation eagerly
(only when offsets are enabled), while the congruence graph still matches the
trail, and stores it on the atom so DPLLEngine does not recompute it later from a
state where a subsequent offset merge has joined the two sides (the merge is only
undone at decision-level backtrack);
- checkPending and separate allow the new same-class / decided-false offset cases.
Fixes bv/test01 and abv/ext02; abv/ext01 no longer crashes. SystemTest drops from
5 to 4 failures with no new failures and all other unit tests green. The two
remaining array cases (abv/indexInRange01, ufbv/ufbv01) need the LA-propagated
index equality to re-trigger array congruence, which is a separate gap.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Record that LA->CC offset-equality propagation, eager offset (dis)equality propagation at merge time, and the offset-aware conflict explanation are implemented (commit 858013d): bv/test01 fixed, abv/ext01 no longer crashes, SystemTest 5 -> 4 failures with all other unit tests green. Capture Jochen's insight that the old mDiseqReason anti-cycle (not the offset-differs propagation) was the obstacle, resolved by computing the disequality explanation eagerly at propagation time. Next: the two remaining array cases need an index-merge to re-trigger array congruence. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The benchmark calls (get-proof) but never enables proof production, so it errors whenever the runner does not turn proofs on for it. Add (set-option :produce-proofs true) to the benchmark itself. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…e per value Redesign the CC<->LA sharing for offset equalities, replacing the fragile non-constant fingerprint bucketing. The root problem: with offsets the LASharedTerm was made offset-free (value of the offset-free affine), so a term like (a+255) mod 256 was handed to LA with value -255 instead of 0, and mbtc - which groups shared terms by value - never matched it against 0. The fingerprint bucketing recovered this but over-collided on every fixed value and starved the useful propagation (ufbv01, indexInRange01 stayed sat-masked-as-unknown). Now the LASharedTerm carries the term's full value (its constant included). This is sound because the offset-free CCTerm and the full LASharedTerm share the same LinVars - the constant only lands in the LAEquality bound - and the CC-level offset equality is still derived from the term constants in EqualityProxy. mbtc then groups by true value and propagates the offset equality the ordinary way, so the non-constant bucketing is removed. share() is decoupled: several full terms (2x+4y, 2x+4y+1) collapse to one offset-free CCTerm, so each distinct full-value LASharedTerm is registered with LA (mbtc must see every value) while the offset-free CCTerm is shared with CC once. The offset-aware CC disequality machinery from the previous commit (merge-time disequality propagation, computeAntiCycle, eager explanation) is unchanged and still needed - offset CCEqualities are still created, just via the value-based path now. Fixes abv/indexInRange01 and ufbv/ufbv01. SystemTest now has a single remaining failure, model/buggy001, a pre-existing array-model assertion unrelated to offsets. All other unit tests pass. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Record the full-value LASharedTerm redesign (commit 0c94d30): mbtc now groups by true value, the non-constant fingerprint bucketing is gone, and indexInRange01 + ufbv01 are fixed. Only model/buggy001 remains (pre-existing array-model assertion, unrelated to offsets). Capture the next items: share all numeric CCAppTerm arguments (completeness), simplify the vestigial offset propagateSharedEquality, the proof object, and the optional CCEquality<->LAEquality unlinking. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Make the shared-term fingerprint ignore the constant part when offset equalities are enabled, so two shared terms collide when their non-constant parts agree (provably equal up to a constant). propagateSharedEqualities recovers the exact offset from the model-independent value difference and propagates an offset CCEquality to CC -- the LA->CC dual of CCTerm.mSharedTerm -- instead of only zero-offset equalities. The early-out guard in propagateSharedEquality is offset-aware: same affine class and matching offset is already known and skipped; otherwise the propagated hash dedups, so the same-class/different-offset conflict (self-pair (rep, rep)) lets CC raise the offset conflict exactly once. The shared-var loops iterate a snapshot because propagating an offset equality synthesizes and shares a (rhs + offset) term (appends to mSharedVars); it is offset-free-equivalent to an existing term and the guard recognizes it as known on the next call. No-op when offset equalities are disabled (proofs/quantifiers): the full-value fingerprint is kept and every offset is zero. SystemTest unchanged at 1 failure (model/buggy001, pre-existing). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…er[] Replace the parallel (CCTerm[], Rational[] offsets) representation with a single CCParameter[] in CCAppTerm, SignatureTrigger (and CongruenceTrigger / FindTriggerTrigger / ReverseTriggerTrigger), and CCTermBuilder. Offset-free arguments stay bare CCTerms via CCParameter.of, so there is no allocation regression and the two parallel-array invariants are gone. - createAppTerm takes CCParameter[] (the argOffsets overload is dropped); SignatureTrigger drops its 3-arg constructor; effectiveOffset is just getOffsetToRep() and equals() uses sameValueAs(). - ReverseTrigger.getArgument() now returns CCParameter, and ReverseTriggerTrigger keys its signature on the argument *value* (getArgParam) rather than the offset-free term. - Full break: CCAppTerm.getArgument(i)/getArguments() are removed. Callers use getArgParam(i) for the value or getArgParam(i).getCCTerm() for the structural term (ArrayTheory, DataTypeTheory, DTReverseTrigger, EMReverseTrigger, GetArgCode, QuantClause, ModelBuilder). Offset-aware proof generation is left for later: CongruencePath.computeCCPath and CCProofGenerator carry TODOs noting the annotation should pair on CCParameter; clause extraction is already correct (<=1 offset edge per arg). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…e check) At argument sites that are structurally offset-free -- datatype selector/tester arguments, array arguments of select/store, and the two array arguments of diff -- replace `getArgParam(i).getCCTerm()` with `(CCTerm) getArgParam(i)`. The cast asserts the no-offset assumption at runtime (ClassCastException on an OffsettedCCTerm) instead of silently dropping an unexpected offset. Array index/value accessors keep getCCTerm() (they intentionally take the offset-free part of a possibly-offset argument), as do the constructor-argument sites, which still need offset-aware handling (injectivity, selector projection, model building). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
DataTypeTheory.ConstrTerm now stores its arguments as CCParameter[] instead of CCTerm[], so a numeric constructor field keeps its offset (e.g. cons(x+5)) and the field's model value is computed offset-aware via ModelBuilder.getModelValue(CCParameter). The model-assembly loop reads the value through the parameter and only recurses on the offset-free representative for still-unresolved datatype-typed fields (numeric fields are resolved in an earlier SCC). Previously the field's offset was dropped, giving e.g. (fst p) = y instead of y + 5. Selector-sourced arguments are offset-free already, so they are unaffected. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
getSMTFormula returned (= lhs rhs) and dropped mOffset, so an offset equality lhs == rhs + k was translated as lhs == rhs. With model-check-mode this made the checker evaluate e.g. 0 == y instead of 0 == y + (-3) and report a spurious "Literal not satisfied" FATAL (the printed model values were already correct). Emit (= lhs (+ rhs offset)) when the offset is non-zero. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Two QF model benchmarks (model-check-mode, :status sat) exercising the offset paths: offset_lia (congruence offset equality f(y+5)) and offset_datatype (an offset equality inside a datatype constructor, (mk (+ y 5) 0)). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… lemmas Per the proof rules (doc/proof/datatypes.tex), the only datatype operands that can be numeric are constructor arguments, so offsets only enter the propagated equality of dt-project (s_ij(u) ~ v_j) and dt-injective (a_k ~ b_k); every reason and the mainEq of the other rules stay offset-free. DataTypeLemma.mMainEquality becomes a SymmetricPair<CCParameter>, and the lemma producers read the constructor field via CCAppTerm.getArgParam(i) (keeping its offset) and compare values with sameValueAs instead of comparing offset-free representatives. processPendingLemmas encodes the offset into the propagated equality via createEquality(t1, t2, offset, ...) and treats a same-term / different-offset main equality as a trivial conflict. Reasons remain SymmetricPair<CCTerm> (offset-free) and computePath already collects offset edges for clause extraction, so the conflict/propagation clauses are correct without proof generation. Proof annotation still pairs on the offset-free terms (offset-aware datatype proofs are deferred, see the CongruencePath TODO). Adds test/datatype/offset_lemmas.smt2 exercising both rules over a numeric field. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Rework SubPath rendering and fix a lingering cross-class offset bug in the congruence-merge conflict path. SubPath.getParams now takes the anchor (a CCParameter in the path's class) at render time instead of storing mStart/mStartOffset; the relative offsets are intrinsic (getOffsetToRep differences). It asserts the anchor shares the representative of every numeric node — a path spanning two classes mixes reference frames and yields garbage offsets, the root of the earlier offset conflicts. Non-numeric terms never carry an offset, so weak-array paths (which cross strong classes) are exempt. The no-arg getParams() self-anchors at the first node. This guard exposed that computeCycle(diseq) from CCTerm.mergeInternal (a disequality forbids a merge at the matching offset) walks a single path across the freshly added, not-yet-united merge bridge — the eager-conflict twin of the lazy computeAntiCycle/computeAntiCycleDiffClass path, never converted, silently wrong in the proof object when the bridge offset is non-zero. Fix: generalize computeSharedConflictCycle into computeMergeConflictCycle taking an optional concrete diseq literal (shared-term clash -> null; merge conflict -> the disequality as the cycle's positive literal); both build the two single-class halves separately and stitch them. CClosure.computeMergeDiseqCycle wraps it; mergeInternal orients the diseq sides into source/destination class and calls it. abv/ext01 (bridgeOff=-1) exercises it and proof-checks unsat. The destination-half pre-shift now rides on getParams(rhsTerm@shift), so the main path is a plain concatenation (computeAntiCycleDiffClass and computeMergeConflictCycle). Removed dead code orphaned by the shared-term-clash change: SubPath.getTerms(), the CCTerm[] prepend overload and unused terms/mainTerms locals in CCAnnotation, and the two-arg computeCycle(CCParameter,CCParameter). test/proof 97/98, abv 4/4, bv 35/35, regression 53/55, uflira 5/5, lia 32/32 (only the two documented pre-existing failures); BitvectorTest 89/89, ProofSimplifierTest 14/14, ProofUtilsTest 4/4, CongruentAddTest 5/5, PairHashTest 1/1. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
mVisited keys congruence subpaths by an undirected SymmetricPair, so a retrieved SubPath's stored term list may run either way. The cross-class stitch builders (computeMergeConflictCycle, computeAntiCycleDiffClass, computeCongruenceAntiCycle) assumed [start..end] and produced a mis-stitched main path when the subpath was stored backwards. getParams(anchor) now treats the anchor as the intended start: the anchor must be a path endpoint, and the term list is rendered in reverse when the anchor is the stored last node, so callers always get [anchor..other]. The stitch sites anchor explicitly at their start endpoint (segSrc.getParams(srcEnd), segB.getParams(right@shift), existing.getParams(second@0)) instead of self-anchoring, and assert the main path runs srcEnd..destEnd by comparing getCCTerm() (not the offsetted parameter, which carries a non-zero offset for a real offset diseq). Validated by temporarily reversing the build order of both halves: abv/ext01 still proof-checks unsat. test/proof 97/98, abv 4/4, bv 35/35, regression 53/55, uflira 5/5, lia 32/32 (only the two pre-existing failures); BitvectorTest 89/89, ProofSimplifier/ ProofUtils/CongruentAdd/PairHash green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The three anti-cycle builders are special cases of computeMergeConflictCycle. The same-class ones are the degenerate case where the two endpoints coincide (srcEnd == destEnd == lhs): the source half is empty and the destination half is the existing class path from rhsTerm back to lhs, so the trivial diseq (lhs@0, lhs@(bridgeOff - pathOffset)) falls out of the same two-half stitch. Three knobs span every case: srcEnd==destEnd (same vs cross class), reason==null (congruence vs equality bridge), diseqLit==null (trivial/shared vs concrete disequality). Delete CongruencePath.computeAntiCycle, computeAntiCycleDiffClass and computeCongruenceAntiCycle; route CClosure.computeAntiCycle (both branches, orienting the separating diseq via eq.mDiseqOrientation at the call site) and computeCongruenceAntiCycle through computeMergeConflictCycle. setLiteral's same-class assert-true conflict uses a new computeSameClassAntiCycle helper (must force the same-class shape since eq may carry a stale mDiseqReason). Five conflict explainers collapse to one (plus computeCycle, the bridgeless positive-eq cycle). The unified same-class anti-cycle anchors its trivial diseq on lhs instead of the old rhs; both are valid EQ-discharged trivial diseqs, so proof-check is unaffected. test/proof 97/98, abv 4/4, bv 35/35, regression 54/55, uflira 5/5, lia 32/32, datatype non-quantified clean (only the documented pre-existing failures); BitvectorTest 89/89, ProofSimplifierTest 14/14, ProofUtilsTest 4/4, CongruentAddTest 5/5, PairHashTest 1/1. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The conflict explainers build each half within its own class and never walk the merge bridge, so a merge conflict no longer needs the equal edge. CCTerm.mergeInternal now detects the conflict (a disequality forbidding the merge, or a shared-term clash) and returns it before invertEqualEdges / mEqualEdge / mOldRep / mReasonLiteral are set, dropping the old add-the-edge-then-undo-it dance. The conflict path now mutates nothing and the diseq orientation reads a pristine union-find. Guard fix: a CCTermPairHash.Info also holds equality literals and compare triggers, so diseqInfo.mDiseq can be null when diseqInfo != null. Only a non-null mDiseq is a merge conflict (else diseq.getLhs() NPEs); fall through to the shared-term check / normal merge otherwise. test/proof 97/98, abv 4/4, bv 35/35, uflira 5/5, lia 32/32, datatype non-quantified clean (only the documented pre-existing failures); BitvectorTest 89/89, ProofSimplifierTest 14/14, ProofUtilsTest 4/4, CongruentAddTest 5/5, PairHashTest 1/1. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…computePathNonRecursive mAllPaths was overloaded as both the topologically-ordered annotation output and a return channel (WeakCongruencePath read mAllPaths.removeFirst() to grab the strong path it had just built so it could inline it into a weak path). That coupling caused two problems: drainTodo's dedup set was per-call, so a subpath shared across drains was re-appended (duplicate); and the removeFirst graft relied on mAllPaths's front being the just-built path, which only held because the broken per-call dedup kept re-adding already-built paths. - Promote drainTodo's local `added` set to the field mCollected, so each subpath enters mAllPaths at most once across all drains of a lemma. - Inline grafts (collectPathOnePrimary, collectPathPrimary) call computePathNonRecursive directly: it returns the SubPath without adding it to mAllPaths and enqueues its congruence dependencies for the enclosing drain. Removes the removeFirst call and its ordering assumption. - computeMergeConflictCycle builds its two halves the same way, dropping the mVisited lookup and the filter-out-of-mAllPaths loop; mAllPaths is now exactly the other-paths list and is passed straight to CCAnnotation. - computeConstOverWeakEQ gains the explicit drainTodo() the removed internal graft-drains used to provide. Validated (-ea): test/proof 97/98 (only pre-existing trivialdiseqarray); array + interpolation proof-check pass/fail set identical to baseline; uflira/abv/lia clean; BitvectorTest/ProofSimplifierTest/ProofUtilsTest/RPITest/CongruentAddTest green (117 tests). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…vialdiseqarray) trivialdiseqarray (a = (store (const ((select a j)+1)) i 1), i != j) returned sat for an unsat problem. With i != j, a and the const array agree at j, so select(a,j) = (select a j)+1, i.e. x = x+1, a same-class/different-offset conflict. Two array-side spots dropped the offset and suppressed it: - ArrayTheory: four weak-eq propagation guards (READ_OVER_WEAKEQ / READ_CONST_WEAKEQ, primary-merge and secondary-edge paths) skipped propagation on getRepresentative() equality. Two terms in the same class at different offsets are not already equal -- that is the conflict -- so the lemma was thrown away. Use the offset-aware !select.sameValueAs(other) (matching the existing CONST_WEAKEQ guard). With offsets off sameValueAs reduces to a representative comparison, so classic behaviour is unchanged. - WeakCongruencePath.generateClause built the lemma equality from bare CCTerms (getCCTerm()), dropping the offset into the degenerate select(a,j)=select(a,j) (which trips the createEquality assertion once the guard fires). Pass the CCParameters to the offset-aware overload; it yields the false proxy (eq == null, already handled) so the lemma becomes the conflict clause. trivialdiseqarray is now unsat with a proof-checking low-level proof. Validated (-ea): test/proof 98/98 (was 97/98, no regressions); array sweep (93 benchmarks, proof-check) 0 status mismatches, only pre-existing errors; 117 JUnit tests green (Bitvector/ProofSimplifier/ProofUtils/RPI/CongruentAdd). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… model values An audit of ArrayTheory for offset correctness turned up two value spots that still dropped the offset (indices were already offset-aware throughout): - computeWeakeqExt fingerprint (SOUNDNESS): the per-array nodeMapping that drives weakeq-ext stored element values as bare representatives, so two arrays whose elements agree only up to a constant offset got the same fingerprint and a spurious a = b was propagated. Witness (genuinely sat): (not (= (store c i y) (store c i (+ y 1)))) was reported unsat. Store value identities (getValueKey) and compare with equals() instead of == (offset value-keys are fresh OffsettedCCTerm objects); constRep/defaultValue become CCParameter. Precision only improves: arrays still match iff they agree at every index including offsets, so no valid extensionality is lost. - fillInModel element values (wrong models): the const value, per-index select values, finite-elem default, and secondary-edge select all fed a bare representative to getModelValue, dropping offsetToRep. getModelValue(CCTerm) returns only the representative value while getModelValue(CCParameter) shifts by the offset, and Java picks the CCTerm overload for a CCAppTerm argument, so pass CCParameters (getValueFromConst directly, or getValueKey for selects). Validated (-ea): test/proof 98/98; the witness is now sat (was unsat pre-fix, confirming the soundness bug); model-check-mode on a const/store offset instance yields a consistent model; array sweep (93 benchmarks, proof-check) 0 status mismatches, only pre-existing errors; 117 JUnit tests green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…odelBuilder getModelValue(CCTerm) returned mModelValues.get(term.getRepresentative()) -- the representative's value with the member's offsetToRep silently dropped, which is surprising and a source of wrong models for numeric members (the bug just fixed in fillInModel). Remove it in favour of the single offset-aware getModelValue(CCParameter): a bare CCTerm is an offset-free parameter, so all former callers (array/datatype/boolean terms -- all non-numeric or representatives) rebind to it with identical behaviour, while any numeric member now necessarily goes through the offset-shifting path. Removing an overload is binary-incompatible: callers in other files (e.g. DataTypeTheory) must be recompiled, so a clean build is required (an incremental rebuild leaves a stale .class referencing the deleted method and throws NoSuchMethodError). Validated (clean build, -ea): test/proof 98/98; datatype+model dirs 30/30 (incl. model/offset_datatype); array sweep 0 status mismatches; trivialdiseqarray unsat, extensionality witness sat, model-check on a const/store offset instance consistent; 117 JUnit tests green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ue(CCParameter) getModelValueWithOffset(CCTerm, Rational) was a private helper called only from getModelValue(CCParameter) and two sites that reconstructed a CCParameter's (term, offset) by hand. Inline its body into getModelValue(CCParameter) (using param.getRepresentative()/getOffsetToRep() directly) and route the two callers through getModelValue: - fillInFunctions: getModelValueWithOffset(term, ZERO) -> getModelValue(term) - addApp: getModelValueWithOffset(argParam.getCCTerm(), argParam.getOffset()) -> getModelValue(argParam) Pure refactor, behaviour unchanged. Validated (-ea): test/proof 98/98, datatype+model 30/30, array sweep 0 status mismatches, 117 JUnit tests green; trivialdiseqarray unsat, extensionality witness sat, model-check consistent. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Terms with a constant offset (e.g. x+5) map to a CCParameter (base CCTerm + offset) at build time; offset-free terms map to a plain CCTerm. createCCTerm()/convert() returns the CCParameter, while getCCTerm() returns the offset-free CCTerm from the offset-free-keyed map. EqualityProxy stores the offset-free sides plus the offset. A term that is just an offseted CCTerm is no longer shared with LA. The addTermAxioms must now only be called for offset-free terms. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
drainTodo keeps mAllPaths in the order the proof generator needs (a path precedes the paths explaining its congruences) via a re-enqueue discipline: a freshly seen pair takes the path==null branch, which re-enqueues it behind the dependencies that computePathNonRecursive pushes to the front, so the dependencies are collected first. The only way to bypass that branch is to find the path already cached in mVisited on its first pop. That is exactly what happened for inline grafts. computePathNonRecursive cached every path it built in mVisited, including the strong paths built directly (outside the drain) for splicing into a weak/store path (WeakCongruencePath.collectPathOnePrimary/collectPathPrimary, computeMergeConflictCycle). When such an edge was later requested as a standalone subpath, drainTodo found it already cached and collected it immediately -- ahead of its still-pending dependencies, which addFirst then placed before it. The symptom was an array read-over-weakeq lemma whose (as const) congruence path appeared before the select-congruence path that explains it. Fix: make computePathNonRecursive a pure builder and move the mVisited caching into drainTodo, which already does the lookup. Inline grafts are then not cached, so a standalone request for the same edge rebuilds it through the drain and is collected after its dependencies. The graft's dependencies are enqueued either way, so the inlined congruences are still explained. (A full switch to CCParameter path nodes, to handle cross-class offsets uniformly, is left as a follow-up.) Validated: test/proof 98/98, array/abv proof-check clean, ProofSimplifier/ProofUtils/RPI/CongruentAdd/PairHash green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Hash them by OffsetEqKey instead of symmetric pair. The resolveEqualities still checks for the simple identity or symm case and only uses the farkas lemma when needed.
Record the select/const edge of each weak-i path explicitly in the lemma
annotation instead of re-deriving it by searching the clause equalities.
With offset equalities the justifying select equality is offset-rendered
(the constant may sit on the select side), so the old search is ambiguous;
delivering the edge from the producer removes that ambiguity for all three
consumers (CCProofGenerator, ProofSimplifier, ArrayInterpolator).
- WeakSubPath stores the edge (select1/select2, ordered path[0]->path[last]),
set in computeWeakCongruencePath; null for plain weak paths.
- CCAnnotation carries mSelectEdges parallel to the paths.
- The :weakpath term becomes {index, subs} or {index, subs, {left, right}};
ArrayInterpolator ignores the extra element (backward tolerant).
- CCProofGenerator.collectWeakPath reads the annotated edge (orientSelectEdge),
findSelectPath only as fallback.
- ProofSimplifier threads the edge through proveSelectOverPath and feeds its
flat terms (bare select / full const value) to proveSelectConst, bridging the
offset-rendered clause equality via resolveNeededEqualities; match is decided
by proveSelectConst, not by proveSelectPathTrans (which may return null).
Validated with offsets off: array + interpolation proof-check sweep unchanged
vs baseline; on constarr014 the annotated edge covers every select step and the
search fallback is never hit. Preparation for offsets under proofs (the
proveSelectConst offset-value handling is still open). See
doc/offset-equality-plan.md.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Remove old code to determine the select/const edges
TermCompiler.unifyPolynomial now unifies only the constant-free part of a polynomial and re-attaches the constant with CCParameter.addConstant, so every canonic sum is the canonic offset-free term with the constant as last summand, byte-identical to the flat terms that annotations build via addConstant. A constant base folds into a plain constant (5, not (+ 0 5)), a zero offset returns the term unchanged, and Clausifier.addConstantToTerm is just CCParameter.addConstant now. This lets ProofSimplifier.OffsetEqKey drop the Polynomial summand hashmaps: the new OffsetTerm splits a side purely syntactically into offset-free part (a Term, compared by identity; the 0 term for pure constants) and constant offset. BvToIntUtils was the one producer bypassing the unifier with direct Polynomial.toTerm calls (e.g. normalizeMod emitted the constant mid-sum, breaking the syntactic key on abv/indexInRange01 and ufbv/ufbv01); its polynomial-term exits now go through the unifier. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
An offset equality x = y + k can justify a path step x+k1 = y+(k+k1). The mixed variable of the literal names the shared value of its own two sides, so at path level it stands for mixedVar + k1, and an EQ placeholder equating it with a path-level shared term s must use EQ(mixedVar, s - k1). The new OffsetLitInfo wraps a LitInfo with the shift and orientation of a literal instance relative to the literal (one shift suffices: a key match forces both sides to shift equally). It provides getMixedBoundary() (mixedVar + shift), buildEQ() (normalized via Polynomial), and isLeftALocal/isLeftBLocal, which also fix the orientation hazard that OffsetEqKey matches flipped pairs. OffsetEqKey now retains the absolute side offsets and computes shift/orientation between two equal keys. CCInterpolator routes all lookups through getEqualityInfo(), reorients the clause disequality against the path endpoints (it can itself be shifted), and closeAPathMixed takes the OffsetLitInfo to emit the shifted EQ. interpolateInstantiation needs no change since it uses the atom's own parameters. The new test dt_project_offset001 exercises a mixed dt-project equality used at a non-zero shift in a congruence. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
In a dt-injective lemma both constructor arguments can carry offsets, so the canonicalized clause literal (e.g. b = a-2) differs from the annotation's main equality (b+7 = a+5) by a constant shift and possibly swapped sides. The new getAnnotationLitInfo() reorients the literal info to the annotation equality via OffsetLitInfo. interpolateDTInjective works at annotation level in the mixed branches: shared terms come from the annotation's diseq parameters selected by isLeftALocal (removing the assumption that the clause atom order matches the annotation), and the mixed disequality emits buildEQ, which subtracts the shift from the shared selector term. interpolateDTProject gets the same treatment for its disequality against the goal equality; the shift is currently always zero there since the propagated atom is created at exactly the annotation offset, but this is safer against future lemma changes. Also fix the missing-disequality branch, which read the equality info from the (empty) disequality map. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The unifier for master reverse triggers was a static JVM-global cache keyed only on (function symbol, argument position). A second solver sharing the theory -- the interpolant checking solver is a clone of the main solver -- got the first solver's master trigger back and never registered its own find trigger, so it had no selector/tester reverse triggers at all: no dt-project/dt-tester propagation (the "Unpropagated selector/is of constructor" recovery fired at every final check) and missed dt-cycle conflicts, making the checking solver claim SAT on unsat datatype queries. The unifier is now a per-engine field of CClosure. MasterReverseTrigger.activate wraps each new application in a ReverseTriggerTrigger, but removeTerm only removed mCongTrigger and mFindTrigger, so the application entry survived a pop and later trigger merges activated reverse triggers on the removed CCAppTerm. The application term now remembers these signatures (mReverseTriggers) and removeTerm removes them. This is sound because pop asserts an empty undo stack: all signature merges, including the insert-time merges that addSignatureHash also records, are already undone at that point, so each application entry is back in its own signature object. This fixes the interpolation tests dt_constructor001/002 and dt_cycle001/2/3/5/7/8, whose interpolants were correct but rejected because the checking solver missed the datatype cycle conflict. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
CClosure.createEquality and EqualityProxy.createCCEquality passed a null SourceAnnotation, which addTermAxioms dereferences when the equality's term is new to the solver. This was unreachable in practice because the terms of theory-propagated equalities always existed already; in the interpolant checking solver with working datatype triggers, a propagated tester equality can reference a term the clone never clausified. Use SourceAnnotation.EMPTY_SOURCE_ANNOT like other theory-internal term creation does. Also assert that the createCCEquality fall-through in createEquality is only taken for numeric equalities: it creates an LAEquality, and a non-numeric equality always matches the cached literal above unless that literal is a stale atom referencing removed CCTerms. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Key the lemma's equality/disequality maps by OffsetEqKey, so a path-level
fact like (+ i 1) != (+ j 2) finds the canonicalized clause literal
(= i (+ j 1)). The lookups return the atom together with an OffsetLitInfo
reoriented to the query. A found atom denotes exactly the queried fact,
so it can be used as a formula unchanged; the constant shift only matters
in three places:
- Projections: index (dis)equalities collected on a weak path are stored
as ProjectedIndexLit holding the path-level term of the non-weakpath
side. buildFPiTerm uses it instead of picking the atom parameter that
is not the weakpath index (silently wrong under a shift), buildEQ for
mixed disequalities and getMixedBoundary for mixed equalities.
- findSharedTerms matches the offset-free parts and returns the other
side (or the mixed variable) plus the constant difference.
- The select structure of the main disequality and the read-const select
are taken from the lemma annotation, as the clause atom may be
offset-canonicalized.
The select/const edge of a weakeq-ext weak path is now read from the
lemma annotation (:weakpath {index, subs, {left, right}}) instead of
searching the clause equalities; findSelectEquality and isGoodSelect are
removed. Note that an edge term that is a select can still be the value
of a const array node, so the const-value attachment is checked first,
regardless of the edge term's shape. A mixed select edge whose literal
is value-shifted against the annotation is not supported yet and asserts.
The addStoreEdgeStep branch for a missing index disequality now asserts
that the indices are trivially distinct (same offset-free part, different
constant), so a missed lookup can no longer be silently misread.
The new tests arrayoffset001-009 cover shifted store/select indices in
read-over-weakeq (001/002/007), offset const values (003/009), the
annotated select edge (008), offset stores resolved by congruence
(004/005), and an LA-derived offset index through a mixed CC equality
(006); 001 and 007-009 fail without this commit.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The e-matching register becomes CCParameter[] end to end, so candidate values keep their constant offsets: GetArgCode passes the full argument value (binding x := a+3 when matching f(x) against f(a+3)), YieldCode records CCParameter substitutions, and the dawg keys render the value terms. Compare triggers are offset-aware: insert/removeCompareTrigger mirror the insertEqualityEntry offset walk (including parking a trigger at the merge boundary when the two values are already in one class at a different offset); merge-time activation was already offset-selective. isEqSet/isDiseqSet take CCParameters with value semantics; isDiseqSet also detects same-class values at different offsets as provably distinct. getCCTermRep becomes getCCParamRep (constant split, value-keyed signature lookup, returns rep plus offset), and the new Clausifier.getCCParameter looks up the value of a possibly offsetted term. getRepresentativeTerm canonicalizes to the representative value term so a and a+1 in one class stay distinct substitutions; QuantClause keeps argument offsets in the interesting instantiation terms. MBTC clash slots gain the reverse-trigger source: the watched value of an installed reverse trigger joins its (symbol, position) slot. Offset-free behavior is unchanged; offsets stay disabled under quantifiers until the following commit. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Drops the quantifier condition from Clausifier.createOffsetEqualities; with the proof gate already open this enables offsets for all problems, including quantifiers with proofs and interpolation. It also makes the Clausifier and CClosure offset predicates coincide, eliminating the raw-vs-effective flag divergence. New regression tests pin the e-matching value semantics: the offset binding x := a+3, the dedup distinctness of a and a+1 within one congruence class, and a guard against the spurious unsat that dropping the offset used to cause. Validated by the full test suite (726/726) with lowlevel proof checking, model checking and interpolant checking enabled in the system tests. The remaining quantified/*match* failures are a pre-existing limitation (quantified datatype match terms), unrelated to offsets. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The model builder chooses fresh values for numeric classes that never entered the linear arithmetic solver, avoiding all values registered so far. But only representative values were registered: a use site of a class (a member or a function application argument, a CCParameter) has value repValue + offsetToRep, which was never marked as used. A fresh value could thus coincide with such a use-site value, evaluating a function at the same point twice with different results. Fix: compute per numeric representative the minimal and maximal offset at which any use site references the class (all members and all numeric CCAppTerm argument parameters, scanned globally since use sites of a class can sit in applications of other sorts). setModelValue additionally registers value + maxOffset as used, and a fresh class value is chosen as extendFresh() - minOffset so that even the smallest use-site value is fresh. Add regression tests test/model/offset_fresh001..003.smt2 covering the offset on the shared side, a Bool predicate variant, and a negative offset on the CC-local side. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.