Rounding mode fixes - #5
Open
kunalsheth wants to merge 52 commits into
Open
Conversation
Phase A of the rounding-mode-discipline work. Two sites ran gaol interval arithmetic without establishing the FE_UPWARD rounding mode that gaol's directed rounding requires for soundness, relying instead on an ambient mode that — once CAPD is linked — is FE_TONEAREST: - ContractorIbexPolytope::Prune: CtcPolytopeHull runs gaol arithmetic to build its linear relaxation, with no guard (unlike ContractorIbexFwdbwd::Prune). This guard is currently *defensive*: IBEX is built with LP_LIB=none, so contract() is a no-op and the hazard cannot fire today — hence no regression test (it would be vacuous). It documents the invariant and makes Prune correct-by-construction if an LP backend is ever enabled. - Tighten (delta-sat post-processing): runs interval.diam()/mid() and a gaol `&=` from Context::Impl::CheckSat(), whose ambient mode is undefined (whatever CheckSatCore left). Establish FE_UPWARD for the pass. Phase E will replace the hand-rolled endpoint arithmetic with interval ops. A third candidate (the unguarded .diam() in DefaultTerminationCondition) is deferred to Phase C: it is masked today by the per-contractor guards and a standalone fix would add per-iteration fesetround cost to the fixpoint loop — exactly the cost Phase C's phase-hoisting removes. Full suite green (570/571; only the known-flaky Timer.Test1 failed). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…cy + Debug gate Phase B of the rounding-mode-discipline work — make the FPU-mode invariant checkable in Debug at zero release cost. - DREAL_ASSERT_ROUNDING(x) now compiles to ((void)0) under NDEBUG instead of unused(fegetround() == x), so it no longer executes a fegetround() read in release builds and is free to sprinkle densely (incl. hot paths). - RoundingModeGuard maintains a debug-only thread_local shadow of the mode the guard stack expects. DREAL_ASSERT_ROUNDING_CONSISTENT() asserts the live FPU register still matches that shadow, catching an fesetround/CAPD clobber that bypasses a guard — drift a plain guard cannot detect. Placed at the gaol->CAPD boundary (contractor_ode_lohner::Prune). - Dense DREAL_ASSERT_ROUNDING at the gaol-world leaves (ContractorIbexFwdbwd, ContractorIbexPolytope, Box::MaxDiam) and the CAPD boundary. Forward-looking: these become the safety net once Phase C hoists the per-Prune guards. - rounding_debug_gate.sh: builds the Debug test target and runs the suite, failing on any rounding-assertion abort (the known-flaky EXPECT trio does not fail it). The automated form of "Debug build + any benchmark reveals leaky rounding modes". No CI provider exists in-repo, so this is a script to wire in. Verification: Debug gate passes (no rounding assertion fired across the suite; the shadow consistency check did not false-positive at the CAPD boundary). Release suite 570/571 (only the known-flaky Timer.Test1). CLAUDE.md updated. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
… hot loop Phase C of the rounding-mode-discipline work. Replaces the per-Prune FE_UPWARD RoundingModeGuard (an fesetround on every contractor invocation in the ICP hot loop — pipeline-serializing, the ~65% cost) with a once-per-phase scope plus a compile-time capability token. - New UpwardRounding (zero-size capability) + UpwardRoundingScope (RAII, sole minter) in rounding_mode_guard.h. The scope establishes FE_UPWARD once; its token() witnesses it. - Contractor::Prune and the whole virtual interface / every override now take const UpwardRounding&. The token threads from the phase entry down to every gaol contractor. A contractor cannot be pruned without a caller-supplied token, and only UpwardRoundingScope mints one, so the FE_UPWARD invariant is compile-time-enforced (direct callers, incl. tests, must open a scope). - Phase entries mint the scope once: IcpSeq::CheckSat (before the loop) and each IcpParallel worker (FPU mode is thread-local). Pure-gaol leaves (ContractorIbexFwdbwd/Polytope::Prune) drop their guards and instead DREAL_ASSERT_ROUNDING(FE_UPWARD) to verify the inherited phase mode in Debug. - CAPD reentrancy: contractor_ode_lohner::Prune keeps its internal FE_TONEAREST guard, and re-establishes a nested UpwardRoundingScope before calling its ibex invariant sub-contractors — the token makes that mandatory rather than easy-to-forget. - Ported the direct-call contractor tests to mint a scope (preserved, not deleted). Verification: Release suite 571/571. Debug gate passes — no rounding assertion fired across the suite, confirming the phase mode is correctly established on every path that reaches the now-unguarded gaol contractors (incl. CAPD reentrancy), and the shadow consistency check still does not trip. CLAUDE.md updated to describe the phase-hoist + token design. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…+ safe_ accessors Phase E of the rounding-mode-discipline work — the scalar-FP class the token cannot reach (intra-expression mode-mixing). - New util/rounded_double.h: Exact / RoundedDown / RoundedUp typed doubles + make_sound_interval(RoundedDown lo, RoundedUp hi) (compiler-checked outward rounding) + directed arithmetic (sub_down/sub_up/add_down/add_up) that computes the round-down direction via roundDown(x) = -roundUp(-x) under FE_UPWARD (no per-op fesetround) and requires the UpwardRounding token. - Tighten (context_impl.cc): the CONTINUOUS delta-box was built as Box::Interval(mid - half, mid + half) — mis-rounded under every single mode (lower endpoint pulled inward -> too-narrow box, can drop a true solution). Rebuilt with make_sound_interval(sub_down(...), add_up(...)) so gaol rounds outward. (static_cast<int> in the INTEGER case truncates toward zero independent of mode; only the safe_mid is FE_UPWARD-sensitive.) - safe_mid()/safe_diam() FE_UPWARD-guarded accessors centralize the gaol getters. Routed the solve-time call sites through them: theory_solver termination condition (closing the Phase A deferral — now under Phase C's phase scope, no per-call fesetround), Box::MaxDiam, brancher, icp eval, counterexample_refiner, forall_formula_evaluator, the forall counterexample mid. Parser (parse time) and model printing (FE_TONEAREST) stay raw and will be allow-listed by the Phase D lint. - rounded_double_test.cc: verifies the directed rounding matches gaol's own interval enclosure exactly, the Tighten construction rounds outward, and Exact::half is mode-invariant. Verification: Release suite 574/575 (only flaky Timer.Test1) + 4 new tests. Debug gate passes — every routed safe_ site genuinely runs under FE_UPWARD (no false positives). CLAUDE.md updated. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…rce routing Phase D + the C4 wrapper-funneling of the rounding-mode-discipline work. C4 (arithmetic-level token enforcement): - New util/ibex_guarded.h: ibex_hc4_backward(f, rhs, box, cb, UpwardRounding) wraps ibex's HC4 backward and requires the token. ContractorIbexFwdbwd::Prune now calls the wrapper instead of num_ctr_->f.backward directly, so `ur` is genuinely consumed and the raw call is gone. This closes the gap the Prune-level token left: the gaol arithmetic itself now requires proof of FE_UPWARD, not just entry to Prune. Phase D (routing lint): - rounding_lint.py: dependency-free static check (the syntactic intent of the planned clang-tidy check — a real custom check must be compiled into clang-tidy, and clang-query against the compile DB hits a toolchain header mismatch, so a scoped regex lint is the robust, build-free realization). It forbids in src/dreal: raw ibex backward, raw .mid()/.diam(), and intervals built from hand scalar +/- arithmetic. Comment text is stripped before matching; legitimate sites carry `// rounding-lint: allow <reason>` markers (model printing under FE_TONEAREST; integer bisection on exact bounds); the parser and the wrapper-definition files are skipped. - rounding_debug_gate.sh runs the lint first, then the Debug assertion gate. Verification: lint is clean and a self-test confirms it flags an injected raw .backward / .diam (it enforces, not decorates). Release suite 574/575 (only flaky Timer.Test1). Full gate (lint + Debug suite) passes. CLAUDE.md updated. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Onboard the high-priority ode_expressivity benchmarks (43 self-contained
.smt2, content-addressed via manifest.json) as a weighted 4th family
`odeexpr`, alongside saradc/github/tacas. No solver code changes.
Family infra (benchmark/odeexpr.py): ODEEXPR_ROOT, FAMILY_WEIGHTS
{odeexpr:6, saradc:3, github:2, tacas:2} (encodes 1 odeexpr = 3 github =
2 saradc = 3 tacas), family_of, and manifest-based name<->path resolution
that tracks each bench_id's current revision (robust to regeneration).
Selection/aggregation:
- select.py / select_baseline.py: union the odeexpr corpus from the
manifest and draw it with weighted-without-replacement sampling
(~3x per-item) so the high-priority family is over-sampled.
- aggregate.py: merge baseline_odeexpr.csv as the authoritative odeexpr
timing reference, add a weighted_overall PAR2, and tag odeexpr
regressions with elevated ODEEXPR/ODEEXPR-HIGH priority. Fix a
divide-by-zero (sub-10 ms CPU rounds to 0.00) with a documented
measurement floor that still flags genuine instant->seconds jumps.
Methodology: global 600 s timeout; primary metric is CPU time (user+sys),
not wall clock (multi-tenant machine), with the solver under nice -n 1.
Cross-solver comparison:
- run_batch.sh honors a DREAL_BINARY override for alternate native builds.
- run_dreal3.sh runs the set through dReal v3.16.12 (Docker) with a
semantics-preserving input adaptation; enforces the timeout INSIDE the
container (a host timeout around docker run leaves VM zombies on macOS)
and measures in-container CPU.
- compare_solvers.py joins per-solver summaries; baseline_odeexpr_cav26.csv
/ baseline_odeexpr_dreal3.csv + odeexpr_solver_comparison.txt are the
frozen results. HEAD (arm64, upgraded IBEX/CAPD) vs cav26: identical
solve-set + verdicts, ~2-3x faster; vs dReal3: ~6-20x faster and solves
2 more. No SAT/UNSAT disagreements among the three.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
contractors.md: the Prune signature now carries the UpwardRounding capability token; add prose on why (gaol sound only under FE_UPWARD, phase-hoisted scope as sole minter) and update the Adding-a-Contractor steps with token forwarding + ibex_hc4_backward routing + lint. CLAUDE.md: note rounding_debug_gate.sh (Debug assertion gate) and rounding_lint.py in Running Tests; refresh the clean-run count to 573/576 (rounded_double_test added 4 tests). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The docs/ tree still described Codac (CtcLohner order-2, the --capd-t-gate/--capd-ndim-gate gated hybrid, contractor_odes_codac.cc, codac2::GlobalEnclosureError) as the live ODE backend, contradicting CLAUDE.md. Rewrite every such site to the current reality: CAPD is the sole backend, order-10 IOdeSolver+ITimeMap, via run_capd_fwd / run_capd_bwd / run_capd_trace over a per-flow CapdOdeCache (forward f(x) + negated -f(x) IMap), with trivial-flow and T=0 short-circuits. Substantive (not rename-only) corrections in qf_nra_ode_semantics.md: translation failure RAISES (does not silently skip); to_capd_string covers nearly the full QF_NRA operator set; divergence is caught inside run_capd_fwd (found==false) rather than via a codac2 exception. Also ode-integration.md (largest rewrite), architecture.md, api-guide.md, syntax-reference.md, README.md, and the contractors.md ODE section. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Comment-only, no behavior change. The CAPD ODE headers still said the integrator was Taylor order-20 (the tuned value is kCapdTaylorOrder=10) and that make_capd_ode_cache 'Returns nullptr if translation fails' — it returns nullptr only when flow is null and RAISES (std::runtime_error, contractor_odes_capd.cc:318/338) on an untranslatable RHS. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…model Consolidate the four overlapping rounding constructs (RoundingModeGuard, UpwardRoundingScope, the UpwardRounding token, rounded_double.h) into one symmetric design with two parallel regimes, each: a named RAII Scope that establishes the mode and mints a zero-size capability token, the token threaded as compile-time proof into every mode-sensitive operation, a DREAL_ASSERT_ROUNDING backstop, and a routing-lint rule. - Interval regime (FE_UPWARD): UpwardRoundingScope -> UpwardRounding, consumed by safe_mid/safe_diam (now token-gated, matching sub_*/add_*/ibex_hc4_backward). - Nearest regime (FE_TONEAREST): new NearestRoundingScope -> new NearestRounding, consumed by new format_double / dump_json and run_capd_*. Decimal formatting is equally correctness-critical: a model value formatted under FE_UPWARD prints the wrong number. RoundingModeGuard is now a sealed rounding_detail primitive (private ctor; only the two scopes friend it), so no call site outside rounding.h ever names a rounding-mode constant. UpwardRounding is threaded through the whole eval/branch path (FormulaEvaluator/ExpressionEvaluator operator(), EvaluateBox, Brancher/TerminationCondition std::functions, CounterexampleRefiner::Refine); ExpressionEvaluator drops its per-eval fesetround in favor of the inherited phase mode. Headers reshaped for symmetry (1 infra + 1 consumer header per regime): rounding_mode_guard.h -> rounding.h (infra: scopes, tokens, macros) rounded_double.h + ibex_guarded.h -> rounded_interval.h (interval consumers) + rounded_format.h, json_guarded.h (nearest consumers) rounding_lint.py gains a 4th rule (raw json .dump( -> dump_json) and documents that there is no real clang-tidy (it is a dependency-free regex substitute). New rounded_format_test.cc locks in the nearest-regime correctness case. Verified: release suite 575/575, Debug rounding gate PASS, routing lint clean, benchmark 0 regressions/0 exceptional (the one flagged SAT->UNSAT flip is a pre-existing baseline-staleness artifact, UNSAT on this arch since 2026-06-05). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Adds the verifier for the two upcoming gaol ARM64 rounding-cost levers
(inline aarch64 fpcr fast-path; batched nearest-region). Both levers must
change only when/how the FPU rounding mode is switched, never the values
computed, so every gaol interval function must stay BIT-IDENTICAL.
Two layers over a wide adversarial grid (132 cases: sin/cos/tan/exp/log/
asin/acos/atan/sinh/cosh/tanh/sqrt/pow + the four basic ops, hitting
extrema, poles, domain edges, full periods, huge magnitudes, subnormals,
point intervals, and overflow/underflow):
(A) Bit-identical golden -- the exact, unforgeable lever gate. The golden
table (gaol_transcendental_golden.inc) is captured from the baseline
build by the DISABLED_Generate test, committed and inspectable; the
check recomputes every case and asserts the output endpoint bits
reproduce bit-for-bit (memcpy bits, never ==).
(B) Independent enclosure (+ coarse catastrophic-width floor) -- validates
the frozen baseline golden is itself sound, not enshrining a bug.
Asserts the gaol interval encloses the libm reference at sampled
endpoints/extrema/interior, with a few-ulp reference-error tolerance.
A tight independent width bound is not achievable across all regimes
(argument reduction near sin/cos zeros is absolute-limited; ulp-distance
explodes across zero; finite sampling underestimates wide images) --
exact width is layer (A)'s job.
All test code lives in dReal; nothing is added to the ibex-fork.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Add a runtime tripwire to RoundingModeGuard's dtor: it reads the live FPCR and
abort()s in *every* build if the mode the scope established did not survive to
scope exit. An out-of-band fesetround is a soundness hazard — gaol under the
wrong mode silently empties a box, yielding a false `unsat`. The dtor reuses
that read for a live-based restore that heals any in-scope mode change while
preserving the check-before-set write-skip; the old changed_-gated restore is
gone.
The tripwire surfaced two real, previously-masked clobberers, both now contained
with a new ExpectClobber scope tag (suppress the tripwire for that scope, rely on
the live-based restore to heal the mode):
- CAPD's DoubleRounding leaves the FPU in a directed mode (FE_UPWARD) on return
rather than restoring nearest -- contained tightly in the run_capd_* /
make_capd_ode_cache adapters (contractor_odes_capd.cc).
- ibex's interval operator<< likewise leaves a directed mode -- contained at
the two model-print sites, Box::operator<< (util/box.cc) and the
smtlib2-compliant PrintModel (smt2/driver.cc). This was the cause of an
abort() after printing an interval-valued (e.g. ODE) model.
Also folds in the earlier fesetround work on this branch: remove the spurious,
mode-independent NearestRoundingScope from is_integer / convert_int64_to_double
(util/math.cc) -- is_integer is called per pow in the hot FE_UPWARD VisitPow
loop, so the scope forced a needless mode flip per call.
Tests: BoxTest.IntervalPrintDoesNotClobberRounding (verified it catches the bug
by reverting box.cc), plus ContractorCapdFullTest.GenerateTrace{DoesNotClobber-
Rounding,TrajectoryShape} -- first coverage of generate_trace / --visualize.
Debug rounding gate green (578/578), routing lint clean, release --visualize
end-to-end output byte-identical to baseline.
Docs: CLAUDE.md FPU-rounding section and OPTIMIZATION_LOG.md updated.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The bare `smt2` line matched any path component named smt2 at any depth, so it silently ignored the source tree src/dreal/smt2/ (17 tracked files) and the test fixtures under test/dreal/test/smt2/ (519 tracked files) in addition to the intended top-level smt2/ examples/scratch dir. Tracked files survived, but new files in those source/test dirs would have been dropped silently (and `git add` of src/dreal/smt2/ warned). Anchor it to `/smt2/` so only the top-level dir is ignored. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ExpectClobber
The always-on RoundingModeGuard tripwire and the ExpectClobber tag were only
covered indirectly (via CAPD adapters and model printing). Add util/test/
rounding_test.cc to exercise the mechanism directly:
- CleanScopeEstablishesAndRestores: the live-based restore returns the FPU to
the caller's mode (no abort).
- {Nearest,Upward}ExpectClobberContainsAndHeals: ExpectClobber suppresses the
tripwire for a body that leaves the mode changed AND heals back to the
caller's mode, in both regimes.
- RoundingModeGuardDeathTest.{Nearest,Upward}UncontainedClobberAborts:
EXPECT_DEATH cases proving an out-of-band fesetround inside a
non-ExpectClobber scope aborts at scope exit ("clobbered out-of-band").
threadsafe death-test style since the test binary links the full solver.
Note: a new GLOB'd test file needs a CMake reconfigure to be picked up; the
reconfigure also brought cmake-build-debug current with f55d480's test file.
Debug gate green (588/588, 0 rounding aborts); the contained child abort does
not trip the gate (it keys on the parent exit code).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
DREAL_TESTS is a file(GLOB_RECURSE) with no CONFIGURE_DEPENDS, so the test-file list is cached at configure time. A brand-new test .cc is only picked up after `cmake <build-dir>` (or FULL_BUILD.sh); BUILD.sh, bare `cmake --build`, and rounding_debug_gate.sh just run ninja and silently skip it, reporting green while never running the new test. Document this verification trap in the Running Tests section. (Hit during this branch's work — a new rounding_test.cc appeared to be gate-validated when it had never been compiled.) Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…fork #9/#10) The odeexpr fesetround section left the gaol-internal directed-rounding slice as "untouched / off-limits". It was addressed in the ibex-fork by two bit-identical levers (inline aarch64 FPCR write; batched nearest-region), gated by the dReal-side gaol_transcendental bit-identity test. Records the measured 3-way result: L1 ~2%, L1+L2 ~8% on transcendental-dense odeexpr. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ding levers) Bumps the patch count 7->10 across CLAUDE.md / DEPENDENCIES.md / CODAC_MIGRATION.md / CMakeLists.txt (the docs were stale at 7; #8 gaol log/pow + #9/#10 gaol ARM64 rounding-cost levers were missing) and pins IBEX_GIT_TAG to the fork HEAD sha e6d2403d (reproducible) instead of the moving dreal-perf-patches branch ref, so standard github builds pull the new surgical patches. Refreshes the odeexpr fesetround note (gaol-internal slice now cut ~8% in the fork) and the Dockerfile comment. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ty-propagation soundness net
Bumps the IBEX pin e6d2403d -> cf3928c7 (ncsys-lab/ibex-lib@dreal-perf-patches),
which adds fork patch #11: HC4Revise/InHC4Revise/Gradient backward methods (and
the shared CompiledFunction::backward<V> driver) signal an emptied domain via a
bool return-status instead of throwing the nested EmptyBoxException. This removes
__cxa_throw / _Unwind_* from the contraction hot path (measured up to ~27% of CPU
on throw-dense odeexpr decrease/positivity proofs). The public
Function::backward(y, x, callback) signature is unchanged, so no dReal solver
code changes — emptiness is still detected via iv.is_empty().
Adds a Phase-0 soundness net for correct empty-propagation, written against the
throw-based ibex FIRST and green through the conversion with zero assertion edits:
- contractor_ibex_fwdbwd_test: transcendental/forward-funnel/quotient empties +
a hard-contract-but-non-empty control.
- ibex_backward_callback_partial_empty_test: HC4 incompleteness preserved
(x*x == -1 must NOT empty in one backward — a spurious empty would be a
false-unsat; the genuine deep partial empty is not single-call constructible).
- contractor_{fixpoint,seq,join}_test: empties arising mid-composition must
propagate through the contractor combinators.
- hc4_empty_propagation_soundness_test: end-to-end UNSAT-must-hold (missed
empty -> false sat) and SAT-must-hold (spurious empty -> false unsat) verdicts.
- contractor_ibex_fwdbwd_fuzz_test: seeded fuzz over both directions.
A/B over all 50 odeexpr (Phase-2 vs pre-change baseline, CPU time): zero
SAT/UNSAT flips, zero regressions, solve set 14 -> 12 TIM (tanh_decrease__J0.6
TIM->SAT, cs5c_sigmoid__decrease TIM->UNSAT), tanh_decrease__J1.0 311->183s
(1.7x). __cxa_throw inclusive 26.6%/5.2% -> 0% on the two throw-densest benches.
Docs updated to the 11-patch fork state: CMakeLists pin/comment, CLAUDE.md
(dep entry, branch lineage, odeexpr hotspot now eliminated), DEPENDENCIES.md
(patch #11 + totals), CODAC_MIGRATION.md, and a new OPTIMIZATION_LOG.md section.
Verified: fresh gcc_build from cf3928c7 (clean clone of the pinned fork),
ctest 603/603; ibex `make check` 62/62.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
… profile ContractorIbexFwdbwd::Prune and ContractorIbexPolytope::Prune called stat.timer_pruning_.resume()/.pause() unconditionally, bypassing the stat.enabled() check. With the default spdlog level (off), stat.enabled() is false so the timer data was never read — yet 2× steady_clock::now() → mach_continuous_time fired per Prune call. Post-Phase-2 sample profiling found this at 16.3% of runtime on kuramoto__N6 (sin-heavy, short per-Prune work makes fixed overhead relatively large), 4.1% on tanh-heavy benchmarks. Fix: two one-line guards in each contractor (fwdbwd.cc lines 100,133; polytope.cc lines 155,157). Post-fix profile: mach_continuous_time 11.3%→0%. Kuramoto__N5 spot-check: ~88 s vs ~101 s baseline (~13% faster). Rounding debug gate: PASS. Also adds: - Post-Phase-2 profiling table (3 benchmarks) to OPTIMIZATION_LOG.md; confirms fesetround and __cxa_throw both at ~0%, documents the new attribution (gaol transcendentals 30–45% computational floor, HC4 ~22–27%, ExpressionEvaluator ~6%, allocation ~5%, branching <0.5%) - Open avenues A–E in OPTIMIZATION_LOG.md (ExpressionEvaluator, allocation, per-constraint skip-if-unchanged, constraint ordering, gaol Lever 3) - CLAUDE.md odeexpr hotspot note updated to include the timer fix and reference the open avenues section - Baseline and state.json refresh (post-Phase-2 local baseline) - compare_solvers.py: PAR2 table now scored over benchmarks solved by ≥1 solver, excluding never-solved entries that dilute comparisons Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…layers) A value like 2^-1075 (pow(0.5,1075)) underflows, and that surfaced as two independent false-unsat bugs: 1. ibex HC4 backward (fork patch #12, re-pin cf3928c7 -> d9930909): a forward op over-approximates an underflowed result up to the subnormal ceiling (pow(0.5,1075) -> [0, DBL_TRUE_MIN]), but the backward ops that invert via a tight gaol primitive (bwd_pow/exp/sqr/mul/div) were tighter and emptied a feasible operand on a subnormal-band target. The fork's underflow_saturate widens such a target to include 0 before the tight inverse. An FE_UPWARD audit confirmed exactly those five empty; sqrt/log/root invert via a loose forward op and stay sound. 2. Drake constant fold (sound_constant_fold in symbolic_expression.cc): the parser builds exactly-representable literals (0.5, integers) as Constant (double), so pow/mul/div of them eagerly fold via std::pow and an underflowed result becomes the lying scalar 0.0 -- pow(0.5,1075) > 0 then collapses to a false unsat. Fold instead to a sound RealConstant interval bracketing the true value (sign from std::signbit). This stays a constant (a symbolic all-constant Pow/Mul violates Drake's ExpressionMul AST invariant) yet is sound. Inexact decimals (0.1) are already RealConstant and never fold. Tests (3 layers): ibex_log_pow_edge_cases_test.cc (backward net + #321 end-to-end, un-DISABLED + modernized to assert box-emptiness not the patch-#11 return-status); denorm_constant_fold_test.cc (sound-interval folds); the DenormUnderflowEndToEnd suite (end-to-end SAT); denorm_underflow_smt2_test.cc (parse-and-check real SMT2). Validated: ibex make check 62/62, dreal4 suite 620/621 (only flaky Timer.Test1), empty-propagation net 24/24, rounding_debug_gate green. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Box::operator<< sorted the variable names alphabetically (added in 5774191) but kept reading intervals by a parallel counter values_[i++], which indexes in insertion order. Once insertion order != alphabetical order, every variable printed another variable's value -- visible as a "scrambled model" on QF_NRA_ODE problems whose vars (x_0_0, x_0_t, time_0, mode) are declared out of alphabetical order. The box itself was always correct; only the --model / delta-sat dump (and the .dr driver and DREAL_LOG_DEBUG) was wrong. The (get-model) path (PrintModel) was always correct because it walks variable(i)/box[i] by one shared index. Fix: revert the sort so operator<< collapses to the same trivial coupled-index walk PrintModel uses -- variable and value always read from the same i. Removes the sorted_vars copy, the std::sort, and the fragile i++ counter (pure subtraction); both printers now share one value-association idiom so the bug class can't reappear. Output returns to insertion order (matching dReal3). Regression test BoxTest.PrintPairsEachVariableWithItsOwnValue inserts vars in non-alphabetical order with distinct values and asserts each line carries its own value. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…5-sibling fix in counterexample_refiner Two related strands, both motivated by the BUG-005 scrambled-model class (commit 0296a8e): - Generalize `rounding_lint.py` → `lint.py` ("source-hygiene" lint). Same mechanism (file walk + per-line regex + `// lint: allow` escape), adds rule #5: forbid subscript by a side-effecting counter (`arr[i++]`/`arr[++i]`) — a manual index advancing in parallel with a range-for loop variable silently drifts out of sync once the two containers' orders differ (the BUG-005 shape). Marker renamed `rounding-lint: allow` → `lint: allow` (fallout in box.cc, rounding_debug_gate.sh, docs/contractors.md). - Fix the same pattern in CounterexampleRefiner::Refine: `init_[i++]` advanced over box-insertion order while nlopt indexes by `Box{forall_vec_}` order, so a forall variable's refined value could land in the wrong slot. Re-key both the initial-guess setup and the read-back off `forall_vec_[k]` position, aligning them with nlopt and each other regardless of box variable order. Gate: lint clean; full ctest 626/629 (known-flaky trio only). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Set CMAKE_EXPORT_COMPILE_COMMANDS ON so gcc_build/compile_commands.json is emitted with the project's full -I list (ibex-install, capd-install, generated parsers, the drake third_party tree). Symlink it to the repo root for clangd: ln -sf gcc_build/compile_commands.json compile_commands.json Survives a fresh FULL_BUILD.sh (reconfigures without -D flags). Tooling-only; no behavior change. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
… A/B harness The weighted-random /benchmark selection favours odeexpr, which is ODE-free, so it can't target the github/tacas/saradc ODE families an ODE-contractor A/B needs — which is what drove a one-off freelance A/B script. Make it first-class: - select.py: --family a,b,c restricts the corpus by odeexpr.family_of before selection; --all emits every benchmark of the filtered corpus deterministically (no random, no anomalies). e.g. `select.py --family github,tacas,saradc --all` → the 123 ODE-family jobs. - do_ab.sh BIN_A BIN_B [jobs]: A/B two builds over the same jobs (default = full ODE family), reusing run_batch.sh (DREAL_BINARY) + parse_results.py + compare_solvers.py. Runs the two SEQUENTIALLY, never concurrently — overlapping batches starve jobs and turn real solves into false wall-clock TIMs (the measurement artifact to avoid). The sanctioned way to compare HEAD vs a working-tree build instead of hand-rolling a harness. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…t on free-time integrals The Codac→CAPD rewrite's ODE contractor was UNSOUND. `run_capd_fwd` intersected the terminal box with only the enclosure at the SINGLE endpoint t_ub, so a free-time integral `(integral 0 time [x0] flow)` whose solution is reached at an interior time < t_ub was over-narrowed away → false `unsat` (the catastrophic direction for a delta-complete solver). Proven on github_oct5_0hz_k2_prostate_cancer (free time in [0,20]): committed HEAD (endpoint-only) -> unsat 0.03 s <- WRONG cav26 (trusted reference) -> delta-sat 209 s this change (per-slice) -> delta-sat 68 s <- matches cav26 The per-slice delta-sat witness has solution times ~1.7-4.4, far below the horizon 20 — states HEAD's enclosure(20) provably cannot contain. (dReal3 segfaults on these inputs, so cav26 + the witness are the oracle.) Restore cav26's per-slice tube filter (lost in the rewrite): - run_capd_fwd/bwd return the time-ordered trajectory tube as per-slice enclosures (sub-grid kHullGrid=16 per adaptive step), not a coarse hull. - contractor_ode_lohner::Prune walks slices: per-slice ForallT invariant check (first slice the HC4 contractors empty = interior violation -> stop), terminal- window X_t intersection, hull survivors -> narrowed X_t + time, empty survivor set -> set_empty (sound refutation via CAPD's outward over-approximation). - F4: integrate constant / RealConstant durations too (was is_variable-only, a latent skip). - order 10 -> 20 (kCapdTaylorOrder): per-slice cost is ~16x #steps, so order-10's many small steps explode the slice count; order-20 is cav26's co-designed partner (fewer, larger steps). Perf across the ODE families is under measurement via benchmark/do_ab.sh. - Exceptions: catch-all sound skip (found=false). Rethrowing real errors (the earlier F5 plan) crashes the solve — this architecture has no ICP-level contractor catch, so an escaping IntervalError reaches terminate(). Fixed the integrate_tube_slices header comment that still claimed "RETHROWN". Tests: contractor_odes_semantic_test (GravityInvariant interior-invariant, AntiCorrelated correlation refutation, DecayFlow infeasible/feasible/time-narrow/ constant-time) cover both refute and SAT-control directions. contractor_capd_test CapdFwd/CapdBwd updated feasible->empty: the sound per-slice refutation, verified against CAPD's rigorous full-set enclosure (consistent with the cav26-matching direction proven above). Gates: ctest 626/629 (known-flaky trio only); rounding_debug_gate PASS; 15/15 ODE tests. Docs (CLAUDE.md, OPTIMIZATION_LOG) carry the soundness narrative; CLAUDE.md also folds the lint-rename + benchmark-tooling doc lines (single file, not cleanly splittable here). state.json excluded — baseline contains HEAD false-unsats and is pending regeneration once the do_ab.sh sweep quantifies the affected set. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
… was truncating to 6 digits
to_capd_string(double) rendered ODE-RHS constants with std::to_string, which
emits only 6 fractional digits (sprintf %f). So a clock coefficient like
(/ 1 3) = 0.3333333333333333 became the literal "0.333333", and CAPD integrated
d/dt[tau] = 3*(1/3) as 0.999999 — a vector field unfaithful by 1e-6. A clock
whose terminal gate sits at the integration-window end (tau=1 at t=t_ub) then
has no surviving terminal slice, so the per-slice filter refutes a genuinely
satisfiable instance: a FALSE-unsat (the catastrophic direction for a
delta-complete solver).
Root cause, not the per-slice contractor. The bug is longstanding and SHARED by
main and cav26's source (git show cav26:.../to_capd_string.h uses the same
std::to_string); main's coarse-hull and cav26's looser filter MASKED the 1e-6
deficit, while HEAD's tighter per-slice tube EXPOSED it. So the per-slice filter
is sound — the feed lied.
Fix (to_capd_string.h): render at std::numeric_limits<double>::max_digits10 (17)
significant digits so CAPD's interval-parse of the decimal literal brackets the
exact double; scientific notation (|v|<1e-4 or huge) re-rendered as
fixed/setprecision(40) because CAPD's parser is unreliable on 1e-3 forms. Added
DREAL_ASSERT_ROUNDING(FE_TONEAREST): binary->decimal is correctly rounded only in
nearest, and the sole caller (build_imap_strings <- make_capd_ode_cache) already
runs under a NearestRoundingScope (mirrors format_double's discipline).
Tests (test-first):
- to_capd_string_test.cc::ConstantRoundTripsExactly (fail->pass); 14 golden
strings ported off the 6-digit format; suite converted to a fixture with a
NearestRoundingScope member (the 17-digit formatting is mode-sensitive, so the
direct-call tests must establish nearest like production — otherwise a prior
CAPD test's leftover FE_UPWARD mis-rounds and trips the Debug assert).
- contractor_capd_test.cc::{CapdFwd,CapdBwd}: these asserted box.empty() (a
refutation) on x'=1, p'=gaussian-pdf with gates xt=10, pt in [0,1]. But
p(20)=erf(10/sqrt2) is strictly < 1, so (x=10, p<1) is a true witness and the
old "empties" was the same truncation false-unsat. Rewritten to assert the
sound delta-sat + witness-band narrowing (instrumented: t0 ~ 20, pt < 1; BWD
p0 = 1-integral ~ 0).
Verification:
- cav26-oracle A/B over 123 ODE jobs (benchmark/results/ab_20260622_190607):
0 false-unsats in fixed-HEAD; the 3 committed-HEAD false-unsats
(k32/k64_water, k64_thermostat triple-network) are fixed AND 2 of cav26's own
residual false-unsats (k256/k64_thermostat-triple-network; k256 is
generator-labeled -sat) are now correct. 118/123 solved vs cav26's 109; PAR2
0.39x (~2.5x faster aggregate).
- Debug rounding gate (rounding_debug_gate.sh + full cmake-build-debug ctest):
lint clean, no rounding-assertion abort, 630/630 pass.
Docs: docs/ode-integration.md (per-slice tube+filter mechanism rewrite + feed-
faithfulness soundness section, order-20/kHullGrid), docs/contractors.md,
CLAUDE.md (new "ODE feed faithfulness" design note). ODE_SOUNDNESS_FIXES.md is
the full investigation log; ode_soundness_repros/ the minimal reproducers.
Known perf follow-up (not soundness): 3 benchmarks fixed-HEAD TIM'd that cav26
solved (k128_quad, k2_battery, k2_prostate_h2) — timeouts, not wrong verdicts.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…list The to_capd_string full-precision feed fix (a925eba) corrected three committed-HEAD false-unsats (the non--sat triple-network variants: k32_water, k64_water, k64_thermostat). A false-unsat empties the box instantly -> fast UNSAT -> aggregate.py flags it as a <0.6x-baseline "exceptional speedup." Since exceptional is monotonic (aggregate.py only .add()s, never removes), those bug-induced flags persisted. Removed the two false-unsat artifacts present in the list: - github_oct5_0hz_k32_water_water-triple-network.drh.n - github_oct5_0hz_k64_thermostat_thermostat-triple-network.drh.n Both entered exceptional together in 96fbd64 as fast false-UNSATs; A/B ab_20260622_162840 (committed-HEAD vs main) confirms committed-HEAD returned UNSAT where main returned SAT. (The 3rd false-unsat, k64_water non--sat, was never in the list.) Kept: the -sat triple-network variant and the -double-network entries -- correct SAT in every build, genuinely faster under the new IBEX/CAPD, so real speedups, not artifacts. Also folds in the pending aggregate.py auto-updates (2 runs at 0296a8e, anomalies cleared, last_run bumped). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ckstop to_capd_string formatted doubles with std::to_string — only 6 fractional digits (sprintf %f) — so a non-exact coefficient like (/ 1 3) fed CAPD the unfaithful literal "0.333333". A clock ODE whose terminal gate sits at the integration-window end (k32_water, k64_water, k64_thermostat) then found no surviving slice -> false-unsat, misattributed to the per-slice filter. Format at max_digits10 (round-trippable) with a fixed(40) fallback for the scientific forms CAPD's IMap parser rejects. All three now return delta-sat. Backstops so the class can't recur: - to_capd_string takes a NearestRounding token: the sole solver-feed path is now compiler-bound to FE_TONEAREST (like format_double / dump_json), threaded from make_capd_ode_cache's scope through build_imap_strings. Was a runtime DREAL_ASSERT_ROUNDING only. - lint.py forbids raw std::to_string feeding a parser (it truncates doubles); the legitimate integer-counter uses carry // lint: allow int. Tests: ToCapdStringTest gains ConstantRoundTripsExactly + a token helper; 27/27 green. Lint clean; rounding_debug_gate PASS (630/630). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…idy) This solver is memory-bound; an accidental by-value copy of a heavy type (Box, capd::IMap, Environment, IntervalVector, ...) where const-ref/move belongs is a silent perf regression that lint.py cannot see — a copy is semantic, not syntactic (auto x = f() copies or not by f's return type). Add a type-aware gate over clang-tidy's *built-in* performance-* copy checks (the "no real clang-tidy" note only ever applied to custom libTooling checks): - .clang-tidy: five copy-centric checks (unnecessary-value-param, for-range-copy, unnecessary-copy-initialization, move-const-arg, implicit-conversion-in-loop), scoped to src/dreal/ headers. No WarningsAsErrors here so editors/clangd surface them as plain warnings. - copy_lint.sh: the gate. Incremental by default (only .cc changed vs. the main merge-base + staged/unstaged), --all for a full sweep. Locates brew llvm's clang-tidy (fails loud, never auto-installs), adds the macOS -isysroot $(xcrun --show-sdk-path) fixup against the Apple compile DB, and --warnings-as-errors. bash-3.2-compatible (no mapfile). A flagged copy is fixed (const&/move) or justified inline with // NOLINT(performance-...) <reason> — the type-aware twin of // lint: allow. Verified: --all fails naming the capd::IMap by-value params at contractor_odes_capd.cc:97 (a double copy — IMap has no move ctor, so the std::move-into-member is a no-op too); clean files exit 0; incremental selects only the branch-changed .cc; no vendored /_deps/ paths leak; the NOLINT escape clears a finding. Existing fixes (non-copyable hot types, cleaning pre-existing findings in untouched files) deferred by design. Docs: CLAUDE.md source-hygiene note + DEPENDENCIES.md dev-tool prereq. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
CapdOdeCache took its two capd::IMap vector fields by value and std::move'd them into members. capd::IMap has no move constructor, so each std::move bound to the copy ctor: a silent no-op move + the by-value param itself = two full IMap copies (each carries the parsed automatic-differentiation tree). clang-tidy's performance-unnecessary-value-param + performance-move-const-arg (the new copy_lint.sh gate) flagged exactly this at contractor_odes_capd.cc:97. Have the constructor take the CAPD vector-field strings and build each IMap *directly into its member* (fn_fwd(fwd), fn_bwd(bwd)). The call site no longer materializes the two intermediate IMap locals — the IMap is built exactly once, in place, zero copies. A malformed string still throws inside make_shared (the IMap ctor) and is caught by the existing handler, which reads strs.fwd (passed by const ref, not moved) for the diagnostic. Verified: copy_lint clean on the file; Release ctest + Debug rounding gate green (only the known-flaky ITE/Timer trio); /benchmark 8 ran, 0 regressions, 0 correctness flips. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
clang-tidy --all flagged the four public CheckSatisfiability/Minimize overloads taking Config by value and then std::move-ing into Context(const Config&): the param is a pure copy (unnecessary-value-param) and the move is a guaranteed no-op (move-const-arg). const-ref the params, drop the dead std::move, remove the now-unused <utility>. No behavior change — there was never a move path. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Grow ./copy_lint.sh's gated check set from the 5 performance-* copy checks
to all performance-* (minus enum-size) plus an explicit allow-list of the
UB / memory-safety / segfault-class bugprone-* checks (use-after-move,
dangling-handle, undefined-memory-manipulation, ptr/array mismatches,
sizeof misuse, ...). Excludes the style/intent bugprone checks and the
FP-prone unchecked-optional-access as noise; excludes performance-enum-size
as a no-correctness-value micro-opt. Rationale + the two exclusions are
documented in .clang-tidy's header.
The whole tree is clean on every newly-gated check, so the UB checks are
zero-noise future-regression protection: copy_lint.sh --all PASSes across
all 76 TUs. Getting there required clearing the handful of genuine
performance-* findings the wider run surfaced:
- reserve() before an emplace_back loop (sat_solver_interval_logic.cc)
- rlim_t{63}*1024*1024 so the product is done in the wide type, not int
(dreal_main.cc) — bugprone-implicit-widening-of-multiplication-result
- std::endl -> '\n' at 23 output/debug sites (drivers, auditor, main,
profiler); content unchanged, several already had an explicit flush
copy_lint.sh header/messages and the CLAUDE.md gate references updated to
reflect the broadened scope.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…UG-005/008)
The per-slice terminal filter intersected X_t against each slice's full
trajectory tube `state` = curve(sub) over the sub-grid time interval. For a
pinned terminal time the only window-overlapping slice is the last sub-grid
step [t_ub - step/16, t_ub], whose tube fattens the endpoint by ~step/16·|dx/dt|.
That fat enclosure:
- bound the endpoint variable to an interior-time value (BUG-005, witness
mis-print), and
- let a sub-true X_t gate survive intersection (BUG-008, false delta-sat).
integrate_tube_slices now also computes per-slice `gate_state`: the trajectory
clipped to the terminal window [win_lb, t_ub] (curve over the window-intersected
curve-domain). For a pinned time the clip collapses to the point x(t_ub), so the
X_t gate contracts to the tight endpoint. The full `state` tube is retained for
the ForallT interior-invariant check, which must still see the whole interior.
win_lb is now threaded through run_capd_fwd/bwd into integrate_tube_slices, and
the terminal-eligibility test keys on a non-empty gate_state. Time hull uses the
in-window portion of each kept slice.
Also guard the longstanding implicit t0==0 assumption (the flow is integrated
from t=0; get_time_0() is never read) with an always-on throw, since a non-zero
or variable lower time bound would silently integrate from the wrong start.
Regression: PinnedDecayTest.FwdPinnedEndpoint_NarrowsToTrueValue (endpoint
narrows to x(1) not the fat tube) and PinnedRiseTest.FwdPinnedSubTrueGate_
BoxEmpties (sub-true gate refuted) in contractor_odes_semantic_test.cc.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…007/008
Encode the reproducers from simulink-to-dreal/docs/dreal-bugs.md as suite-level
regression guards, so a recurrence surfaces here instead of silently downstream.
New test/dreal/smt2/test/dreal_bugs_regression_test.cc — end-to-end SMT2-path
verdict/model guards via parse_string (embeds each bug's exact reproducer text):
BUG-001 nested-arithmetic define-ode RHS -> delta-sat (was false unsat)
BUG-003 ZOH-parameter coupled ODE under integral -> delta-sat (was false unsat)
BUG-005 --model (integral) endpoint value -> 60.653 (was scrambled/61.597)
BUG-006 unsat (integral) formula -> unsat (was false delta-sat)
BUG-008 endpoint asserted below true value -> unsat (was false delta-sat)
contractor_capd_test.cc — ContractorCapdNonConvNameTest exercises the
--visualize generate_trace path with the translator's non-conventional
`x_k<step>` state-var naming:
BUG-004 non-conventional name must emit a full, keyed trajectory (PASS)
BUG-007 per-segment `step` should reflect the BMC index — OPEN, mitigated
consumer-side; assertion GTEST_SKIP-marked (aspirational) until
extract_step learns the `_k<int>` suffix.
BUG-005/008 are also covered at the contractor level by PinnedDecayTest/
PinnedRiseTest (committed in a60b0ff). BUG-002 is excluded: negated (integral)
is silently dropped by design in every dReal version (documented §6 semantics).
All verdict/model guards pass on HEAD; full suite 638 passed / 1 skipped / 0
failed against cmake-build-debug.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…(BUG-007)
The --visualize trajectory JSON tags each ODE segment with a `step` index
derived by parsing the segment's start-variable name. The parser (was
`extract_step`) only recognized dReach's `<base>_<step>_{0,t}` convention and
returned 0 on any other shape, so for the SMT-LIB BMC unroller's `<base>_k<step>`
snapshot names (e.g. x_k0, x_k1) every segment collapsed onto step 0 — a
consumer keying on `step` lost all but the first segment (BUG-007 in
simulink-to-dreal/docs/dreal-bugs.md).
This is purely visualization metadata: start/end vars are identified
structurally from the Integral AST node (get_vars_0/get_vars_t), never by name,
and `step` is read by no solving path — so soundness/verdicts are unaffected.
Name parsing in extract_step was the only name-convention-dependent logic in the
ODE/parser/driver/solver paths.
Change: rename extract_step -> ode_step_from_name and lift it to a free function
in namespace dreal (declared in contractor_odes.h) so the parser is directly
unit-testable. Add a BMC branch (tried first) that reads the trailing `_k<int>`;
fall through to the existing dReach middle-token parse otherwise. The two formats
don't overlap (dReach needs a pure-integer token between the last two '_'; BMC
needs a trailing `_k<int>`), so both parse unambiguously.
Tests:
- ode_step_from_name_test.cc: string-level coverage of both conventions
(x_1_0->1, height_3_t->3, x_k1->1, x_decay_IntX_k0->0) plus base-with-
underscores and no-match edge cases.
- contractor_capd_test.cc: un-skip ContractorCapdNonConvNameTest.
StepFieldReflectsSegmentIndex (now asserts x_k1's segment reports step 1).
Verified on a current-source build (gcc_build): full suite 642/642, lint clean,
and end-to-end --visualize on the reproducers — bug007_trigger now
[('x_k0',0),('x_k1',1)] (was [...,('x_k1',0)]), bug007_baseline unchanged at
[('x_0_0',0),('x_1_0',1)].
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Heavy /condense pass over docs/ + root cheatsheets. The three accreted root logs (1389 ln, 38% of the doc tree) were chronological worklog about a removed backend; distil their hard-won lessons and drop the converged narrative. - Add docs/decisions.md — topic-keyed architecture/soundness ADRs: ODE backend (Codac→CAPD-only rationale: CAPD-20≥Codac-2 experiment, gradient root-cause, fork-ibex-team decision), per-slice ODE tube, ODE feed faithfulness, denormal/ underflow (#321), backward narrowing via −f(x). - Remove CODAC_MIGRATION.md (twice-superseded; dependency gone, decision executed) and ODE_SOUNDNESS_FIXES.md (converged worklog; outcome in CLAUDE.md, repros on disk). Bucket-A nuggets migrated to decisions.md. - Condense OPTIMIZATION_LOG.md 711→354: keep every Rejected lesson + Open avenues verbatim; drop superseded order-10 sweep tables and redundant odeexpr sample tables (outcomes live in CLAUDE.md / ibex-fork). - Lift to_capd_string + denormal #321 depth out of auto-loaded CLAUDE.md into docs/, leaving one-line pointers; trim the upgrade-ibex lineage bullet. - DEPENDENCIES.md: replace the drifted-stale 11-patch catalog (11/cf3928c7 vs actual 12/d9930909) with a categorized pointer to ../ibex-fork/MIGRATION.md. - Fixes: drop eigen deps from README (dropped with Codac); CAPD order-10→20 in docs/architecture.md + docs/README.md; repoint all in-scope CODAC_MIGRATION.md refs to docs/decisions.md. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The Jun 18-23 soundness fixes (FE_UPWARD rounding unification, #321 denormal/underflow, per-slice ODE filter restore, to_capd_string full-precision feed, BUG-005/007/008) change verdicts and timings, so the prior baselines and run data no longer reflect the solver. Remove the stale current-solver baselines (baseline.csv, baseline_local.csv, baseline_odeexpr.csv) and the anomaly tracker (state.json) — re-baseline at HEAD before the next /benchmark. Also drop the obsolete one-off probe experiment (probe_*, run_probe.sh). The cav26/dreal3 cross-solver references (baseline_odeexpr_cav26.csv, baseline_odeexpr_dreal3.csv, odeexpr_solver_comparison.txt, and their results/ run dirs) are kept — they are timing data for those binaries, valid as comparison points. All gitignored results/ scratch dirs were also trashed locally. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ull 4) Promote the CAPD ODE-contractor's compile-time constants to runtime --ode-* flags (CapdSolverParams threaded through run_capd_*), then retune the defaults via a meta-parameter sweep: forward & backward Taylor order 20->12 and hull-grid 16->4. 123-job ODE-family confirm vs the old default: ~2x faster (PAR2 0.49), +4 solved (121/123, incl. a newly-completed UNSAT), zero SAT<->UNSAT flips (bwd-12 adds ~5% over bwd-20). New flags (defaults in parens): --ode-taylor-order (12), --ode-backward-order (12), --ode-abs-tol/--ode-rel-tol (1e-10), --ode-hull-grid (4), --ode-c0-set (rect2|tripleton|horect2), --ode-backward (true), --ode-max-step (0=adaptive). C0-set is a runtime type-dispatch over the integrator; --ode-backward gates the BWD contractor at the theory_solver emit site. Soundness: lowering order/hull only WIDENS the enclosures (sound outward supersets), so it can never cause a false-unsat. The accepted cost is *completeness* -- a sharp interior invariant-violation below the hull-4 time-resolution may return delta-sat instead of unsat (the GravityInvariantTest F1 case). That test is pinned to hull-16 so it still guards the per-slice mechanism at adequate resolution. SEPARATELY, the per-slice tube is ~4x looser than CAPD's precision (a fixed hull COUNT over a large adaptive step -> wide sub-intervals -> polynomial dependency blow-up); the deferred width-based sub-slicing fix would recover that precision while keeping the speed. Full writeup: HULL_SOUNDNESS.md. Per-problem finding: the optimal forward order is problem-dependent (tacas inverters want ~8-12, stiff long-horizon github wants ~16-20), which is the main reason it stays a runtime flag. Benchmark tooling: run_batch.sh gains DREAL_ARGS (per-invocation flags) and TIMEOUT env hooks; new do_sweep.sh sweeps one binary over many flag configs in a single shuffled 12-way pool (no idle tail, CPU-time stays accurate). Methodology + per-knob/per-problem data: OPTIMIZATION_LOG.md "2026-06 re-tuning campaign". Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…1/hull as completeness (COMPLETENESS, not SOUNDNESS) Agents kept conflating soundness and completeness, and the mislabel had a concrete cost: the hull-grid "F1" finding (a refutation/completeness trade-off) was filed as a soundness issue, which read as a correctness emergency and got experiments cancelled. For this sound-but-δ-complete solver: - false `unsat` (asserts φ T-unsatisfiable on a T-satisfiable φ) = SOUNDNESS. - missed refutation / false `delta-sat` (asserts φ^δ T-satisfiable on a robustly T-unsatisfiable φ) = COMPLETENESS. Looseness only ever weakens this. Changes: - New canonical doc docs/soundness-vs-completeness.md: the four T-relations (quantifier-explicit), dReal's unsat/δ-sat guarantees, the dichotomy, and the reporting-notation convention. - CLAUDE.md: new terminology-discipline section mandating the model-theory parenthetical on every soundness/completeness claim. - HULL_SOUNDNESS.md -> HULL_COMPLETENESS.md, reframed as completeness; fixed the stale "defaults reverted to hull-16" status (superseded by the adopted hull-4). - contractor_odes_semantic_test.cc: the header framed both test directions as "SOUNDNESS"; relabeled every UNSAT-direction "box must empty" (refutation) gate SOUNDNESS GATE -> COMPLETENESS GATE (F1/F2/F4/BUG-006/BUG-008). The SAT-direction "remain non-empty" gates correctly stay SOUNDNESS. - qf_nra_ode_semantics.md: "soundness limitation for negated ODE formulas" -> completeness/incompleteness, consistent with the file's later "sound but incomplete" framing. - OPTIMIZATION_LOG.md / config.h: residual wording + HULL doc references. No behavior change (comments, message strings, docs, a rename). Test target builds; the 19 edited semantic tests pass; lint.py clean. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…/benchmarking.md CLAUDE.md hit the 40k auto-load limit. Move the FPU rounding / phase-hoisting / typed-doubles / lint-rules mass into docs/rounding.md and the benchmarking infrastructure detail into docs/benchmarking.md; replace the Architecture section (full duplicate of docs/architecture.md) with a 3-line pointer; compress branch lineage bullets to a 6-line table. Cross-references in docs/contractors.md and docs/ode-integration.md updated to point at docs/rounding.md. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Add test/dreal/smt2/test/dreal_future.cc — GTEST_SKIP-ed specifications of the desired future QF_NRA_ODE negation semantics behind BUG-002 (negated integral/ forall_t silently dropped). Suite Bug002NegatedOde: - 2 positive-forall_t controls that pass today (per-slice tube end-to-end). - Axis 1: genuine exists-t not-phi for negated forall_t (refute/witness pair). - Axis 2: the two rival readings of a negated integral — disequality vs. definitional binding — specified side-by-side on identical inputs so they can be A/B-experimented; a divergence table + the unintended implications of each. - Mixed combinatorial corners and the design-gap (no-trajectory) cases. Documents why "throw on the silent drop" is NOT a valid quick fix: link_integral_invariants runs inside the DPLL(T) loop on the SAT solver's transient literal subset, where a negated ODE literal — and a positive forall_t without its companion integral — occur legitimately during search. Throwing there crashes valid multi-step BMC benchmarks (github airplane/gen, verified). Rejecting user-asserted negations needs global problem scope (parse / Context::Assert layer), and is left unimplemented/aspirational. The drops are a COMPLETENESS hazard (missed refutation / false delta-sat), never soundness. Solver behavior is UNCHANGED (contractor_odes.h untouched). Fix a latent exception-unsafe std::cout redirect in RunSmt2String (the new file and dreal_bugs_regression_test.cc): a plain restore-after-parse is skipped during unwinding when parse_string throws, leaving std::cout with a dangling streambuf that segfaults the next writer (surfaced under ctest by the throwing tests). Now restored via an RAII guard on both paths. Docs: docs/ode-integration.md and docs/decisions.md record the constraint forms accepted, the silent-drop behavior, the COMPLETENESS (not soundness) characterization, and the parse-layer constraint. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Adds `_is_oom_risk` to `select.py`/`load_benchmarks` (imported by both `select.py` and `select_baseline.py`): - github/tacas: _k<N>_ with N >= 1024 crash the OS via unbounded SMT expansion - saradc: _<N>b_ with N >= 9 (bitwidth drives problem size independently of k) Removes the 4 already-in-baseline k>=1024 rows (k1024, k1280, k1536, k2048) from baseline.csv. Documents the filter in docs/benchmarking.md. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
… looseness Replaces naive curve(sub) with centered_curve_range(): evaluates the Taylor curve at the thin midpoint time (curve(mid), no time-widening), adds a derivative-bounded correction (curve.timeDerivative(sub) · (sub − mid)), then intersects with the naive curve(sub) so the result is never looser. Both forms are sound outward enclosures; intersecting them is still sound. The naive interval Horner over a wide sub-interval (large CAPD adaptive step + low hull-grid) lost time-correlation via the polynomial dependency problem, making the tube ~4× looser than CAPD's actual precision. Interior invariant refutation was therefore a function of hull-grid, making it secretly a completeness knob. The mean-value form cuts the slop to O(r²) in the sub radius regardless of step size, so hull-grid is no longer completeness- load-bearing. The F1 case (GravityInvariantTest interior violation, margin 0.2 >> δ) now refutes at the default hull-4, not only at hull-16. New test FwdInteriorInvariantViolation_DefaultHull_BoxEmpties is the completeness gate: it asserted delta-sat (missed refutation) before this fix and asserts unsat (empty box) after, with no hull pin. COMPLETENESS improvement (never a soundness risk — the tube only tightens). See HULL_COMPLETENESS.md "Resolution" for full derivation and benchmarks. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…IZATION_LOG; update CLAUDE.md HULL_COMPLETENESS.md: Status block updated from "open" to "RESOLVED (2026-06)"; new "Resolution" section documents the mean-value-in-time derivation, why it beats the width-based sketch, and the measured outcome (github/tacas faster, saradc +14% CPU, no correctness flips). The speculative Stage-2/3 sections are relabeled SUPERSEDED. Investigation history retained as the why-we-got-here record. OPTIMIZATION_LOG.md: "Open follow-up" bullet for the ~4× looseness replaced with "Follow-up RESOLVED" recording the actual fix, its trade-off, and the note that the per-knob numbers were measured on the old loose tube. CLAUDE.md: hull-grid description updated — no longer says "completeness knob"; adds BUG-002 paragraph (negated/unlinked ODE constraints, COMPLETENESS hazard, aspirational GTEST_SKIP tests, why parse-layer fix is unimplemented). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…ne to do_benchmark; PAR2 table in skill do_benchmark.sh: pass --frozen-baseline to aggregate.py so the run's PAR2 is compared against the frozen CSV baseline rather than the run's own mean. baseline_local.csv: refreshed local baseline (~30 stratified benchmarks) on this branch. The old committed baseline was stale (pre-FE_UPWARD-fix false-UNSAT results for k20/k28/k40 box benchmarks). probe_odes.tsv: 18 ODE-heavy benchmarks used for OFAT sweeps (tacas inverters + github prostate/thermostat + saradc box/nonlinear). state.json: seeded with empty anomalies/exceptional lists + baseline_source pointer. skill.md: benchmark skill now renders the per-family PAR2 comparison table from aggregate.json — Family | Weight | n | Baseline PAR2 | This run PAR2 | Ratio, sorted by descending weight, with regression/exceptional flags. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…al_popl27 binary simulink-to-dreal_bug_reports.md: verified bug log (BUG-001 through BUG-008) with dReal v3.16.12 + dReal4 oracle comparisons, minimal reproducers, and workarounds applied in the translator. issue321_repros/: minimal .smt2 reproducers for dreal/dreal4#321 (denormal/ underflow false-unsat): pow/mul/div fold underflow cases + faithful control. Companion to the sound_constant_fold + underflow_saturate fixes in docs/decisions.md "Denormal / underflow soundness". capd_docs/: CAPD API reference extracted from the CAPD source — classes, concepts, modules index, dreal-capd-usage notes, KNOBS.md (knob catalog), AUDIT.md (cross-ref of CAPD API against contractor_odes_capd.cc). Background reference for the ODE contractor; not build artifacts. .gitignore: add dreal_popl27 (ARM64 Mach-O binary, ~7.7MB; not a source artifact). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…mestamp --version now prints three lines: dReal 5.0.0.1.<feature-flags> Commit <hash> [<dirty>], Release Build. Built for Darwin 25.5.0 arm64, on Jun 25 2026 12:51:30. How the values are wired in: git hash / dirty — cmake/GenerateGitVersion.cmake runs `git rev-parse --short HEAD` and `git status --porcelain --untracked-files=no` at every build via an always-run CMake custom target (not a git hook). The output is written to gcc_build/git_version.h with copy_if_different so dreal_main.cc only recompiles when the hash or dirty status actually changes. Untracked files do not count as dirty. OS / arch — CMAKE_SYSTEM_NAME, CMAKE_SYSTEM_VERSION, CMAKE_SYSTEM_PROCESSOR injected as target_compile_definitions at CMake configure time. Timestamp — __DATE__/__TIME__ compiler built-ins, stamped when dreal_main.cc is compiled (which recompiles whenever git_version.h changes). Docker: .git/HEAD, .git/refs/, and a stub objects/ dir (required by git's repo-validation logic) are COPY'd into the image by Dockerfile.dreal_ubuntu so the real commit hash appears. Dirty is always 0 in Docker since there is no index or object store. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
… disambiguation Lit-review (papers/): four companion summaries forming the theory->procedure->tool-> exists-forall lineage (Gao-Avigad-Clarke LICS'12 + IJCAR'12, Gao-Kong-Clarke CADE'13, Kong-Solar-Lezama-Gao CAV'18), with a papers/ index and the PDFs. Cross-referenced into soundness-vs-completeness, architecture, and forall-semantics, plus three stable code anchors (// Ref: comments in contractor_forall.h, symbolic.cc, icp.h). Fixed the docs' conflated LICS-vs-IJCAR 2012 citation (two distinct papers). forall-semantics.md: rigorous delta-completeness expansion grounded in CAV'18 + code -- the two delta-regimes (contractor d/2 vs evaluator 0.99d, the paper's experimental value), the spurious-counterexample hazard and why inner_delta<epsilon<delta is mandatory, a soundness/completeness classification of forall failure modes (all completeness), the SLSQP/COBYLA-via-NLopt and CLP details, and the Lyapunov/global-opt encodings. Corrected the false 'initialized identically' claim about the formula evaluator. forall vs forall_t: corrected a mislabeled contractor in contractors.md (FORALL kind is the exists-forall NRA quantifier, not the ODE-time forall_t), and added greppable 'forall-vs-forall_t' pitfall anchors across docs (forall-semantics, qf_nra_ode_semantics, contractors, CLAUDE.md) and code (contractor.h Kind enum, contractor_forall.h, ode_types.h), with the canonical side-by-side in forall-semantics.md S7. ode-integration.md: documented the ForallT invariant contractor mechanism -- the CAPD per-slice tube fed through IBEX HC4 invariant contractors (construction, per-slice application, FWD-only rationale, reused-box-copy optimization, negated-invariant skip, rounding, soundness/completeness). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…-dup ADRs Establish a crisp build-doc role split: README.md = end-user build guide, docs/build.md = build-system config for devs modifying the build, CLAUDE.md §Build = agent quickstart + pointers. - Move the verbose `--version` value-wiring block out of CLAUDE.md's top-level Build section into the new docs/build.md (git-version target, compile definitions, Docker .git copy); add a build.md row to docs/README.md. - Trim CLAUDE.md §Build's duplication of README (brew prereqs, Docker Ubuntu/clang + bad-fd prose, "no Rosetta" note — all preserved in README / DEPENDENCIES.md); keep the agent-essential quickstart inline. - De-duplicate two decisions.md ADR "why" blocks (ODE feed faithfulness, BUG-002 negated/unlinked ODE constraints) to the load-bearing claim + a pointer to the full mechanism in docs/ode-integration.md, which already carries it verbatim. Docs-only; no behavior change. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…l usage Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…forall-semantics Audited every construct against dreal_popl27 + scanner.ll/parser.yy/sort.cc: - bounds need a comma: [lb ub] -> [lb, ub] (declare-fun/const, forall); the comma-less form is a hard parse error - push/pop: documented as working, actually crash (SatSolver::Push/Pop throw NOT YET IMPLEMENTED); marked unsupported - :precision is handled by set-option, not set-info (info_ is write-only) - get-model/get-value work without --produce-models; the flag only makes check-sat auto-print the model inline - forall: replace duplicated semantics summary with a pointer to forall-semantics.md (incl. forall vs forall_t disambiguation) - add "Recognized but unimplemented commands" list (reset, get-info, declare-sort, check-sat-assuming, ...) and fold in echo/define-fun-rec 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.