Upgrade Ibex/CAPD to Codac - #4
Open
kunalsheth wants to merge 79 commits into
Open
Conversation
…nch for direct lemma additions without matching.
…time_t is a constant/real-const.
…..)`, `alpha_hash_set(..)`)
- Move trie implementation to own subfolder. - Move stats struct to independent header file.
….cc for unit tests.
…ot work on ASTs.
…a-bijection checking.
…ed_map to flat vector for better cache performance.
…unit test. (Fixed alpha-hashing bug that was previously causing it to fail.)
…a/Expressions optional— to avoid unnecessary copying in production.
…atal error to warning.
…ctionality from context_impl.cc.
…dpoint contraction
The previous implementation used LohnerAlgorithm (Codac's simple first-order
method with contractions=1) in a single direction, accumulating a hull of
enclosures that intersected X_t. This gave weak contraction because:
- contractions=1 produces loose per-step global enclosures
- The hull over all n_steps=200 time steps grows wide for long trajectories
- Each contractor call only narrowed one endpoint (X_0 or X_t)
Replace with CtcLohner::contract(tube, FWD_BWD):
- FWD pass propagates X_0 forward, narrowing X_t
- BWD pass propagates X_t backward, narrowing X_0
- Both endpoints are contracted in a single contractor call
- contractions=5 gives tighter per-step enclosures (Codac default)
- n_steps=20 (down from 200) keeps per-call cost low; Lohner is nearly
exact for smooth ODEs with this step size
Add vars_0_narrowed to CodacOdeResult so Prune() can narrow m_vars_0
from the backward pass in the same call, eliminating the need for the
separate BWD contractor to provide X_0 contraction.
Benchmark: bouncing_ball_with_drag_10_0.smt2
before (n_steps=200, contractions=1, LohnerAlgorithm): >>30s
after (n_steps=20, contractions=5, CtcLohner FWD_BWD): 13s
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Seven files covering architecture, contractors, ODE integration, pattern matching (CAV26), C++ API, QF_NRA_ODE semantics, and SMT2 syntax reference. ODE semantics doc is grounded in parser.yy, scanner.ll, symbolic_odes.cc, and contractor_odes.cc, including negated-invariant ignore behavior and all edge cases. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Adds benchmark/ scripts for rapid regression detection during development: - select.py: picks 8 random + all anomaly benchmarks, outputs TSV - run_batch.sh: parallel runner with gtime -v -o and timeout 300 - parse_results.py: parses gtime + solver output into summary.csv - aggregate.py: compares vs frozen DRPM_0L baseline, flags regressions (>1.5x) and exceptional speedups (<0.6x), updates state.json - baseline.csv: frozen reference from prior CAV26/TACAS26 experiments - state.json: persistent anomaly tracker (initially empty) Also adds .claude/skills/benchmark.md (/benchmark) and benchmark-baseline.md (/benchmark-baseline) for one-command invocation from Claude Code. The /benchmark skill delegates result interpretation to a Haiku subagent to keep the main context clean. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…alies benchmark.md: run_batch.sh now launched with run_in_background so the ~5-minute batch doesn't block; wait for task notification instead of polling. state.json: records first real benchmark run (bfcef46) results — 5 anomalies added (3 solve→timeout, 1 ERR, 1 correctness flip) and 3 exceptional wins (tacas benchmarks now solving where baseline timed out). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
- benchmark/select.py: anomaly names in state.json lack .smt2 suffix but baseline.csv names include it; normalize with removesuffix before comparing so tracked anomalies are always guaranteed to run - .claude/skills/benchmark.md, benchmark-baseline.md: replace run_in_background on run_batch.sh with foreground execution (420s/1200s timeout); the background mode killed grandchild solver processes on task cleanup, leaving empty gtime files - benchmark/state.json: updated anomaly list from completed test run Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…e skill - Fix SAR-ADC benchmark resolution: point SARADC_DIRS to the complete AMS-verification-bundle-of-sticks/saradc/rolled/ directory (all 21 baseline entries now resolve); update CLAUDE.md accordingly - Eliminate permission prompts in /benchmark-baseline: extract the inline python3 heredoc from do_baseline.sh into set_local_baseline.py, and pre-compute per-family frozen vs local averages inside aggregate.py (--frozen-baseline flag) so the Haiku subagent only needs one Read call - Migrate skills from flat .md files to subdirectory format (skill.md) - Add do_benchmark.sh / do_baseline.sh shell drivers; select_baseline.py for stratified 3-family sampling; set_local_baseline.py for state updates - Record accumulated run history and anomaly state in state.json Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Prevents resource contention on a 16-core machine that was causing false timing regressions when all benchmarks ran simultaneously. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Two-pass optimization to close the post-migration regressions in both ODE and non-ODE solving while staying inside Codac v2 + lebarsfa/ibex-lib. ODE contractor (contractor_odes_codac.cc, contractor_odes.cc): - CodacOdeCache reuses the per-flow AnalyticFunction and CtcLohner across every Prune call; keyed by OdeFlow* with a static dedup map so hybrid systems with N_modes copies of one flow translate the symbolic RHS just once instead of N_modes x 2 times. - contractions=2 (was 5): empirical speed/tightness sweet spot. - BWD contractor skips CtcLohner (Step 4): the constructor's m_vars_0 <-> m_vars_t swap turns CtcLohner FWD_BWD into the wrong question for non-time-symmetric dynamics. FWD's FWD_BWD already narrows both endpoints jointly, so skipping BWD's Step 4 loses no contraction. See CODAC_MIGRATION.md for the correctness analysis. - Trivial-flow short-circuit: flows where every RHS is the literal 0 bypass CtcLohner entirely and just intersect X_0 ∩ X_t. - Adaptive n_steps: clamp(max(n_steps_hint, ceil(t_ub * 2)), n_steps_hint, 60). Keeps the historical 20-step floor for short horizons (bouncing ball unchanged at ~2.8 s) and only adds steps when t_ub > ~10 so cardiac (t_ub up to 30) gets h <= 0.5 instead of h = 1.5. Cardiac k4 went from 29 s baseline (TIM on a noisy day) to ~5 s consistently. IBEX fwdbwd contractor (contractor_ibex_fwdbwd.cc): - Replaced the full-box IntervalVector iv_before = iv snapshot + std::set <int> changed_vec with a thread_local std::vector<(int, ibex::Interval)> saving only the input bits' intervals before contraction. Cost per Prune goes from O(|box|) to O(|free_vars(f)|) (typically 50-500 vs 2-10), and the std::set node allocations disappear entirely. thread_local keeps the buffer's capacity across calls so steady-state Prune does zero alloc. Headline timings vs baseline: - cardiac_new_cardiac k4: 29 s -> ~5 s (6x) - tacas c2e2 k10 NOR__sigmoid SAT: 142 s -> 0.8 s (170x) - tacas c2e2 k17 NOR__sigmoid UNS: TIM -> 13.6 s (resolved) - tacas c2e2 k21 NOR__sigmoid SAT: 234 s -> 7.7 s (30x) - bouncing_ball_with_drag_10_0: unchanged at ~2.8 s (n_steps floor) Hard TIMs that remain (quad k128, planning k1280/k1536, crazyflie k16, prostate k2 variants, cardiac k64) are at Codac v2's order-2 Taylor ceiling — not fixable without library changes. Full writeup in CODAC_MIGRATION.md under "ODE Contractor Optimization Pass" and "Second Optimization Pass". Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…ic tests The BWD ODE contractor's Step 4 (previously an early-return no-op) is re-enabled via Codac LohnerAlgorithm(forward=false). The FWD path's CtcLohner FWD_BWD is unchanged — this is purely additive. Adds ~50% per BWD Prune; bouncing_ball_with_drag_10_0 goes from ~2.8s to ~4.2s. Soundness is verified by a new semantic test suite — closed-form fixtures for trivial, decay, and rational-coupled (mock-prostate) flows. All 7 soundness gates pass on both HEAD and the experiment, including the load-bearing MockProstateTest cases whose rational coupling mirrors the prostate_h2 benchmark's dynamics. The prior "any SAT↔UNSAT flip aborts" criterion conflated soundness regressions with completeness improvements. The new aggregate.py classifier distinguishes SOUNDNESS REGRESSION (flip away from annotated ground truth) from CORRECTNESS IMPROVEMENT (flip toward it) from UNDETERMINED FLIP (no annotation). Ground truth is populated only from filename conventions (VNAMSCwI _SAT/_UNS, SARADC -1e/5000e); dReal3 is not propagated because it has the same δ-completeness limitations as dReal4. A frozen-baseline fallback makes flips on anomaly-list rows missing from baseline_local.csv visible to the classifier. Re-classifying the prior experiment batch: 0 soundness regressions, 5 UNDETERMINED FLIPS (4 prostate variants + 1 water-double-network-sat, all SAT→UNSAT — likely δ-witness refutations). CLAUDE.md, CODAC_MIGRATION.md, and DEPENDENCIES.md are updated to reflect the BWD restoration and the new performance baseline. The new CODAC_MIGRATION.md "Third Pass" section records the verification audit, documents the cache-key bug in make_codac_ode_cache (raw OdeFlow* pointers, vulnerable to pointer reuse — worked around in the test file via inline static fixtures), and lists the natural next steps. codac_docs/ collects the Codac v1/v2 reference material and analysis notes (including alternatives_to_ctclohner.md, which gated this experiment) that informed the work. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
make_codac_ode_cache used a raw OdeFlow* as the cache-map key. If an
OdeFlow was destroyed and a new one was later allocated at the same
address, the lookup returned a stale cache built for the previous flow.
Hit reproducibly when test fixtures created and destroyed OdeFlows
between TEST_F instances.
The cache map now stores a CacheSlot { shared_ptr<const OdeFlow> flow,
shared_ptr<CodacOdeCache> cache } keyed by raw pointer. The held
shared_ptr keeps the OdeFlow alive for the cache's lifetime, so the
address cannot be reused while the entry is live. make_codac_ode_cache's
signature changes from (const OdeFlow& flow, ...) to
(shared_ptr<const OdeFlow> flow, ...) — the single call site in
contractor_odes.cc now passes icc->get_flow() directly instead of
dereferencing it.
The semantic test fixtures keep their inline-static OdeFlow members for
tidiness (one cache entry per fixture class instead of per TEST_F
instance), but the comment is updated to note the fix.
Note: TimePropag::FWD-only on the FWD contractor (item 5) was
attempted and reverted in this session — it caused
github_oct5_0hz_k4_cardiac_new_cardiac to flip UNSAT → delta-SAT
(soundness-direction). The deferred-item recommendation in
CODAC_MIGRATION.md ("re-lock the regression baseline before measuring")
stands.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
CODAC_MIGRATION.md collapses from a multi-phase planning doc into a finished migration summary (-711 lines). CLAUDE.md, DEPENDENCIES.md, and docs/ode-integration.md trim their Codac sections to point at the consolidated doc instead of repeating it. examples/README.md replaces stale Bazel build instructions with a current manual-compile recipe against the CMake build. codac_docs/analysis/alternatives_to_ctclohner.md gains a "Why #6 is not justified" section spelling out the soundness, wrapping-effect, and maintenance arguments against rolling a custom higher-order Taylor integrator, so the existing "not justified for CAV26" verdict isn't re-litigated without that context. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
The cache-key pointer-reuse bug previously listed under "Known issues" was fixed in commit fed8a02 (CacheSlot holds a shared_ptr<const OdeFlow> alongside the cache). Update the four spots that still described it as unfixed: - "Current implementation": describe the new CacheSlot layout and the shared_ptr-based liveness guarantee. - "Open lines of attack" item 2 (eviction): clarify that the slot now pins each flow in memory until process exit, so eviction is the remaining cache-lifetime concern. - "Open lines of attack" item 7 (Fix the cache-key bug): removed — done. - "Known issues": rewritten as a "Resolved" entry pointing at the fix commit. Record the item-5 attempt under "What we tried but reverted": the TimePropag::FWD-only change on the FWD contractor caused github_oct5_0hz_k4_cardiac_new_cardiac to flip UNSAT → δ-SAT (soundness-direction). The new ground-truth-aware classifier caught it. Reverted before commit. Lesson noted for any future re-attempt (BWD contractions=1 doesn't replace FWD_BWD's BWD pass on cardiac). Refresh benchmark/state.json with the post-cache-fix run's anomalies and exceptional speedups (water-triple, water-double, thermostat- triple, tacas_c2e2 k30 — likely real wins from the cache fix landing properly). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
CAPD master now exposes CAPD_INTERVAL_TYPE=NATIVE, which makes capdExt
skip add_subdirectory(filibsrc) entirely and uses CAPD's own ARM64-capable
DoubleRounding. The previously-abandoned FILIB-bypass patch is no longer
needed. CAPD runs alongside Codac's order-2 CtcLohner via a gate on
(t_ub, n_state_vars); CAPD divergence falls back to Lohner so no narrowing
is ever lost.
* CMakeLists.txt: ExternalProject_Add(capd_external) pinning master SHA
b353e170 (2026-05-18) + INTERFACE_COMPILE_DEFINITIONS=__USE_NATIVE__.
* src/dreal/contractor/odes/contractor_odes_capd.{h,cc}: per-flow IMap
cache (forward + -f(x) for backward integration), per-call IOdeSolver +
ITimeMap. Soundness identical to Pass 3's backward-image argument.
* src/dreal/contractor/odes/to_capd_string.h: forward-ported Expression ->
CAPD-IMap string builder.
* --capd-t-gate (default 5.0) and --capd-ndim-gate (default 6) CLI flags.
* 38 new unit tests: 26 to_capd_string direct tests + 12 contractor
semantic tests (gate dispatch / long-horizon CAPD / backend consistency
/ 6D ndim-gate / trivial-flow precedence). All 550 tests pass.
* Benchmark sweep (30 stratified): 0 regressions, 2 SARADC anomalies
resolved, tacas family 0.44x vs CAV26 frozen baseline.
* Docs: CODAC_MIGRATION.md, codac_docs/analysis/*.md, CLAUDE.md updated.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
DEPENDENCIES.md: add CAPD section (CAPDGroup/CAPD@b353e170, CAPD_INTERVAL_TYPE=NATIVE, ExternalProject); correct IBEX version (ibex-2.8.9.1 → ibex-2.8.9.20250626) and build method (ExternalProject → configure-time zip download) for both IBEX and Codac; update ODE Contractor Status to describe the Codac-default / CAPD-gated hybrid. CLAUDE.md: update Prerequisites line, Auto-downloaded Dependencies list (IBEX/Codac as prebuilt zips; CAPD as ExternalProject), and upgrade-ibex branch summary (remove stale "CAPD abandoned" sentence; describe working gated hybrid). docs/ode-integration.md: fix CtcLohner configuration (contractions 5→2, steps 50→20 adaptive); update Performance section; replace "CAPD not taken" section with "CAPD gated hybrid" section; correct IBEX version in "What was replaced". docs/contractors.md, docs/architecture.md: update ODE contractor description to mention the CAPD gate dispatch. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
TIM/OOM/ERR results are now penalized at 2× the solver timeout (600 s) instead of being excluded from family averages. This fixes a misleading analysis in CODAC_MIGRATION.md where benchmarks transitioning from TIM to solved appeared to "raise" the average — under PAR2 they correctly lower it. Changes: - aggregate.py: add par2_time() helper; unify solve→TIM, TIM→solve, and plain timing regression/exceptional into a single PAR2-ratio check; compute_family_comparison now includes all benchmarks (formerly TIM rows excluded); output keys renamed frozen_avg_par2/local_avg_par2 - CLAUDE.md: update threshold documentation to reference PAR2 time - CODAC_MIGRATION.md: replace old raw-average table with corrected PAR2 numbers from a fresh baseline run; tacas was not "2.3× faster" — it is 2.61× slower once timed-out benchmarks are counted - Skill files: reference PAR2 scores and updated JSON key names - baseline_local.csv, state.json: refreshed from new baseline run Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
The CODAC_MIGRATION.md trade-off table claimed the loss of ncsys-lab's `_grad = nullptr` hack was "minor memory overhead." It is not. `sample` profiling on `1mhz_k20_saradc_2b_box_4a_-1e` puts ~65% of total wall time inside `ibex::Function::init` building `_grad` (Gradient ctor + ExprLinearity walk) — work `Function::backward` (the only IBEX entry point fwdbwd uses) never reads. End-of-run `--verbose info` stats confirm: 0.022 s in Pruning, 77 s in Theory CheckSat, 877 unique-formula cache misses × ~88 ms/each = the missing 77 s. The big fix — restore the gradient-suppression hack on the upstream lebarsfa IBEX — is documented as "Open lines of attack" item 7 (switch `ibex_external` from prebuilt-zip to source `ExternalProject_Add` with a small `PATCH_COMMAND`) and deferred to a follow-on session because it needs source-IBEX build wiring. Expected impact: saradc family PAR2 from 567 s toward ~190 s. What landed in this commit: - `contractor_ibex_polytope.cc::Prune` switches to the Pass-2 input-restricted thread_local snapshot recipe. Quiet win for `--polytope` users; no effect on default-config saradc, which never hits polytope. - Temporary `ContractorIbexPolytopeStat` block added alongside, mirroring the fwdbwd one — useful for future debug under `--polytope --verbose info`. - `CODAC_MIGRATION.md`: trade-off row rewritten to flag actual magnitude; new "Re-investigation 2026-06-07" section with the profile evidence; "Open lines of attack" item 7 added; stale `1mhz_k28_saradc_3b_box_4a_-1e` "TIMs at HEAD" claim corrected (it now solves in 279 s). - `DEPENDENCIES.md`: "performance impact is acceptable" claim corrected with link to the re-investigation section. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…Codac Benchmarking on 2026-06-07 confirmed native ARM64 CAPD order-20 is at least as fast as Codac CtcLohner order-2 on all tested integral-based ODE benchmarks, and 23% faster on the canonical bouncing_ball reference case (3391 ms vs 4410 ms). No verdict differences were observed. This eliminates the performance argument for keeping Codac. CODAC_MIGRATION.md: - Add "Strategic reassessment 2026-06-07" conclusion section with the two-option analysis, full benchmark table, and Option B decision rationale. - Update open-lines-of-attack item 7 to target ibex-team/ibex-lib (not lebarsfa) and fold in Codac removal as part of the same work item. - Fix CLI flag documentation: --capd-t-gate/--capd-ndim-gate validators reject 0; correct invocation is --capd-t-gate 1e-300 --capd-ndim-gate 1. CLAUDE.md: - Note the 2026-06-07 strategic direction in the upgrade-ibex branch desc. - Update ODE performance baseline with measured numbers (4.4 s Codac, 3.4 s CAPD forced) and remove the stale "needs a benchmark sweep" caveat. - Fix the wrong --capd-t-gate 0 force-CAPD invocation in two places. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
This bundles two related changes: 1. **IBEX URL switch.** The ExternalProject source-build for IBEX now defaults to https://github.com/ncsys-lab/ibex-lib.git instead of the sibling file://../ibex-fork path. The IBEX_GIT_REPOSITORY cache variable remains overridable for local-dev iteration against an unpushed checkout. Updates the Dockerfile (drops the COPY ibex-fork step), DEPENDENCIES.md, and CLAUDE.md to match. 2. **Soundness regression tests** (`ibex_log_pow_edge_cases_test.cc`). Header rewritten to document the patched-and-shipped state of ibex commit 33eb6676 ("gaol: fix Interval::log and Interval::pow soundness gaps"). Adds two new tests: - PowSubnormalUnderflow: confirms `pow([0.5,0.5], 1075.0)` returns the rigorous overapproximation [0, DBL_TRUE_MIN] (not [0, 0]). - DISABLED_PowSubnormalUnderflowEndToEnd: documents the remaining ibex HC4-backward unsoundness in pow-of-degenerate-constant chains (the deeper layer of dreal/dreal4#321, beyond what the gaol wrapper fix addresses). DISABLED_ so CI stays green; the diagnostic stays in tree. Note: this commit also picks up some pre-existing upgrade-ibex WIP that was already in the working tree (Codac removal narrative in CLAUDE.md / DEPENDENCIES.md, eigen apt-get removal in the Dockerfile). They're conceptually part of the same "fork-aware build" arc, so bundling them keeps the working tree clean. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Removes the Codac CtcLohner contractor and the CAPD/Codac gated-hybrid
dispatch. CAPD order-20 Taylor now handles every ODE Prune call.
- Delete contractor_odes_codac.{cc,h} and Codac includes from contractor_odes.
- Add run_capd_trace in contractor_odes_capd.{cc,h} to replace
run_lohner_trace for the --visualize flag (one IVector slice per step).
- Drop --capd-t-gate / --capd-ndim-gate CLI flags and the matching
Config::kDefaultCapdTGate / kDefaultCapdNdimGate constants.
- Update CODAC_MIGRATION.md with a resolved-status banner.
- Strip CAPD-forced test variants and gate-boundary tests from
contractor_odes_semantic_test; reframe long-horizon tests as plain
soundness gates against the single CAPD backend.
- contractor_capd_test: drop the Lohner-pinning code; update the BWD
expectations to match CAPD's one-way backward image (no p0 narrowing,
no constraints recorded).
The dreal-perf-patches branch adds an optional callback to ibex::Function::backward (commit 4d61b841) that fires once per narrowed variable. Use it from contractor_ibex_fwdbwd::Prune to populate the output bitset directly, avoiding the per-call snapshot of input intervals. On boxes with 50-500 variables and a fwdbwd constraint touching only 2-10, this skips an O(|free_vars(f)|) copy and the post-hoc comparison loop. Add three companion regression tests for the patch series: - ibex_backward_callback_test: scalar callback fires for each narrowed var, receives correct old/new intervals, skips unchanged vars. - ibex_backward_callback_vector_matrix_test: covers the f04f5db5 audit fix in read_arg_domains so vector/matrix-typed symbols also get per-component notifications (forward-compat for upstream PR). - ibex_function_backward_compat_test: defaulted-arg overload still compiles for the two-arg call site dReal uses today.
Covers ncsys-lab/ibex-lib commit edbd8159 which nulls out the Gradient and ExprLinearity allocations in Function::init. dReal only calls Function::backward, which never touches _grad / _lin, so the lazy initialization is sound for our call path. Profiling on the saradc family attributed ~65% of wall time to those allocations pre-patch. The test exercises a Function pipeline that would page-fault if either field were dereferenced, providing observational evidence the patch holds.
Add two smoke tests calibrated against ncsys-lab/ibex-lib commits fc986657, 4f845aa3 (FPU management on Apple Silicon / x86) and 059d1fe7 (gaol::init wrapper). None of these are part of the current dreal-perf-patches minimal fork — mainline's 971f8eb0 gaol-rounding fix covers the arm64 path without the wholesale FPU rewrite, and the gaol-init cleanup didn't clear the upstream-PR bar. The tests are retained as DOCUMENTATION of where mainline ibex differs from the cav26-era FPU-clean baseline. Goldens can be updated to mainline if the behavior is acceptable, or the patches re-added to flip them to PASS.
The aggregate initializer was passing the second field positionally after a designated .filtered, which some compilers warn on / reject. Add the explicit .changed = ... designator.
…overrun)
Two distinct crash modes were surfacing as ERR exits in the benchmark suite.
Mode A — SIGABRT in CaDiCaL (saradc + several tacas). With factor/BVA
inprocessing on, cadical->vars() includes solver-internal extension
variables; the model-reading loops call val() on them, which aborts
("extension variable ... defined by the solver internally"). Disable factor
in the SatSolver ctor. The model-reading loops are correct only while factor
is off, so each is annotated with a BRITTLE hazard comment pointing at the
(cadical_next_var - 1) bound that would be required if factor is re-enabled.
Mode B — heap buffer overrun in the CAPD ODE integrator (car/automaton
models). The cached IMap was built over every flow variable while the
C0Rect2Set was built from only the evolving state vars, so CAPD wrote an
n x n Jacobian into undersized buffers (confirmed via guard malloc: a write
in Map::operator() during run_capd_fwd -> moveSet). Flow variables with
d/dt == 0 are parameters: emit them in CAPD's par: section and bind them
per-call via setParameter on a private map copy (copying keeps the cached
map immutable, which is required because it is shared across parallel ICP
workers), instead of as integration variables. Mirrors cav26's
build_capd_string. Adds ContractorCapdParamTest exercising the var/par
dimension split that previously corrupted the heap.
Both fixes are satisfiability-preserving. They do NOT address a separate,
pre-existing false-UNSAT on some param-bearing ODE instances (GT=SAT) that
the crashes were masking; that is tracked separately.
Note: contractor_odes_capd.cc also carries a pre-existing, uncommitted
simplification of run_capd_fwd (removal of the in-FWD backward sweep) that
was already in the working tree; it is interleaved with the Mode B edit and
included here.
569/569 tests pass against gcc_build at this tree.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
gaol (ibex's interval backend) is sound only with the FPU in round-upward mode; under any other mode its directed rounding inverts (lo>hi), so an inexactly-FP-representable subexpression collapses to an empty interval and wrongly empties the box. ContractorIbexFwdbwd::Prune historically relied on ambient FE_UPWARD, but linking CAPD (the ODE backend) leaves the process FPU in FE_TONEAREST via its DoubleRounding static init, so the ambient mode can no longer be assumed. The result was a silent false-UNSAT on formulas with inexact constant arithmetic inline in inequalities (e.g. (* 3.3 x), (* C (pow 10 -N))) -- the GT=SAT false-UNSATs on the 1mhz_*_saradc_*_box_* benchmarks. Exactly-representable values (0.5, *1.0) need no rounding and so hid the bug. Establish FE_UPWARD explicitly per Prune (cheap; runs on every ICP worker thread, where FPU mode is thread-local). Also guard FE_TONEAREST in contractor_ode_lohner::generate_trace (the --visualize path), the only CAPD entry point that lacked it -- the solve-critical Prune/cache paths were already guarded. Adds an end-to-end regression test and documents the gaol<->CAPD rounding-mode invariant (plus the known flaky-test trio) in CLAUDE.md. Verified: the three saradc benchmarks now return delta-sat; full suite green except the pre-existing flaky trio (ITE-eliminator counter, Timer.Test1); benchmark batch shows 0 regressions, 0 correctness flips. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…pty) Regression tests for two dreal-perf-patches fork fixes, authored during the fork patch audit: - 1836b569 (function: copy old-value in backward callback to avoid aliasing box storage) - d2b978b9 (HC4Revise: report partial narrowings on EmptyBoxException) Both pass against the current fork build. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 <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.