diff --git a/.clang-tidy b/.clang-tidy new file mode 100644 index 000000000..bbdf35ecb --- /dev/null +++ b/.clang-tidy @@ -0,0 +1,74 @@ +# clang-tidy gate config — the type-aware companion to the regex lint.py. +# +# Three concerns, all things a regex lint structurally cannot see (they are +# *semantic*, type-dependent), run via ./copy_lint.sh (incremental by default, +# --all for a full sweep; it adds --warnings-as-errors and the macOS -isysroot fixup): +# +# 1. Accidental by-value COPIES of heavy types (Box, capd::IMap, Environment, +# IntervalVector, ...). This solver is memory-bound; a stray copy where a +# const& / move belongs is a silent regression. Covered by the performance-* +# copy subset (unnecessary-value-param, for-range-copy, +# unnecessary-copy-initialization, move-const-arg, implicit-conversion-in-loop). +# +# 2. Other PERFORMANCE pitfalls (avoid-endl, inefficient-vector-operation, +# noexcept-move, etc.) — the rest of performance-*. +# +# 3. UNDEFINED BEHAVIOR / memory-safety / segfault-class bugs — an explicit +# allow-list of the bugprone-* checks whose findings are genuine UB or memory +# corruption (use-after-move, dangling-handle, undefined-memory-manipulation, +# ptr/array mismatches, sizeof misuse, ...). The whole tree is currently clean +# on every one of these, so they cost zero noise and exist purely to catch a +# future regression. NOT the style/intent bugprone checks (easily-swappable- +# parameters, narrowing-conversions, branch-clone, ...) — those are noise here. +# +# Findings are resolved by fixing (const& / move / the real bug) or, when genuinely +# intended, justified inline with // NOLINT() — the type-aware twin +# of lint.py's `// lint: allow`. +# +# Two deliberately-excluded checks (see ./copy_lint.sh history): +# -performance-enum-size micro-opt only (smaller enum base); 12 core +# enums, mild serialization/arithmetic risk, no +# correctness value. +# -bugprone-unchecked-optional-access crash-class but FP-prone; its only hits are +# in the semi-dead pattern_matching trie code. +# +# No WarningsAsErrors here on purpose: editors/clangd surface these as plain +# warnings; the hard fail is the gate script's job (copy_lint.sh adds it). +Checks: > + -*, + performance-*, + -performance-enum-size, + bugprone-bitwise-pointer-cast, + bugprone-bool-pointer-implicit-conversion, + bugprone-casting-through-void, + bugprone-dangling-handle, + bugprone-dynamic-static-initializers, + bugprone-fold-init-type, + bugprone-incorrect-roundings, + bugprone-invalid-enum-default-initialization, + bugprone-misplaced-operator-in-strlen-in-alloc, + bugprone-misplaced-pointer-arithmetic-in-alloc, + bugprone-misplaced-widening-cast, + bugprone-multi-level-implicit-pointer-conversion, + bugprone-multiple-new-in-one-expression, + bugprone-not-null-terminated-result, + bugprone-pointer-arithmetic-on-polymorphic-object, + bugprone-raw-memory-call-on-non-trivial-type, + bugprone-return-const-ref-from-parameter, + bugprone-shared-ptr-array-mismatch, + bugprone-signed-char-misuse, + bugprone-sizeof-container, + bugprone-sizeof-expression, + bugprone-string-constructor, + bugprone-string-literal-with-embedded-nul, + bugprone-stringview-nullptr, + bugprone-suspicious-memory-comparison, + bugprone-suspicious-memset-usage, + bugprone-suspicious-realloc-usage, + bugprone-suspicious-stringview-data-usage, + bugprone-unhandled-self-assignment, + bugprone-undefined-memory-manipulation, + bugprone-unique-ptr-array-mismatch, + bugprone-unused-raii, + bugprone-use-after-move +HeaderFilterRegex: 'src/dreal/.*' diff --git a/.claude/skills/benchmark-baseline/skill.md b/.claude/skills/benchmark-baseline/skill.md index 00b9e51a4..7c79da72c 100644 --- a/.claude/skills/benchmark-baseline/skill.md +++ b/.claude/skills/benchmark-baseline/skill.md @@ -6,7 +6,7 @@ description: Re-establish a local performance baseline by running ~30 stratified # /benchmark-baseline skill 1. **Confirm with user first:** - > This will run ~30 benchmarks (~15-20 min) and update `benchmark/state.json` to use a local baseline. Proceed? + > This will run ~70 benchmarks (all 43 odeexpr + ~10 each of saradc/github/tacas, at the 600 s timeout — can take 30-45 min) and update `benchmark/state.json` to use a local baseline. Proceed? Wait for confirmation before continuing. @@ -15,18 +15,18 @@ description: Re-establish a local performance baseline by running ~30 stratified 3. Spawn a Haiku subagent with this exact prompt: --- -Run the dReal4 baseline script (foreground, 1200000ms timeout): +Run the dReal4 baseline script (foreground, 1800000ms timeout): ```bash bash /Users/kunalsheth/Documents/new_dreal/dreal4-cmake/benchmark/do_baseline.sh ``` The script prints OUT_DIR to stdout when done. Use the Read tool to read `/aggregate.json`. Do not run any other commands or read any other files. -The `aggregate.json` contains a `family_comparison` key with per-family frozen vs local averages, and a `baseline_sha` key. +The `aggregate.json` contains a `family_comparison` key with per-family frozen vs local averages (including a weighted `odeexpr` family and a `weighted_overall` row), and a `baseline_sha` key. Return a formatted summary as your only output: -- Header: `Baseline established from — benchmarks across 3 families` -- Table: one row per family from `family_comparison` — family | n | frozen PAR2 avg | local PAR2 avg | ratio (keys: `frozen_avg_par2`, `local_avg_par2`) -- One sentence: faster/slower/comparable? Flag >20% systematic differences as potentially a build config issue. +- Header: `Baseline established from — benchmarks across 4 families` +- Table: one row per family from `family_comparison` — family | n | weight | frozen PAR2 avg | local PAR2 avg | ratio (keys: `frozen_avg_par2`, `local_avg_par2`, `weight`), then the `weighted_overall` row last +- One sentence: faster/slower/comparable? Flag >20% systematic differences as potentially a build config issue. PAR2 is CPU time (user+sys), 600 s timeout. - Last line: `baseline_local: benchmark/baseline_local.csv` Be terse. Only return the final summary — no narration. diff --git a/.claude/skills/benchmark/skill.md b/.claude/skills/benchmark/skill.md index c14bd331f..4be265d85 100644 --- a/.claude/skills/benchmark/skill.md +++ b/.claude/skills/benchmark/skill.md @@ -10,7 +10,7 @@ description: Run a quick regression benchmark batch (~8-12 benchmarks) for the d 2. Spawn a Haiku subagent with this exact prompt: --- -Run the dReal4 benchmark script (foreground, 420000ms timeout): +Run the dReal4 benchmark script (foreground, 1500000ms timeout): ```bash bash /Users/kunalsheth/Documents/new_dreal/dreal4-cmake/benchmark/do_benchmark.sh ``` @@ -18,12 +18,15 @@ The script prints OUT_DIR to stdout when done. Use the Read tool to read `/anomaly_report.txt` -Be terse. Only return the final summary — no narration. +Then, as the FINAL part of your output, ALWAYS render the per-family PAR2 table from `family_comparison` in `aggregate.json` (the run vs the frozen baseline, `baseline_sha` in the same file). One markdown table, one row per family plus `weighted_overall`, columns: Family | Weight | n | Baseline PAR2 (s) | This run PAR2 (s) | Ratio. Sort families by descending weight (odeexpr, saradc, tacas, github) with `weighted_overall` last. Flag ratio >1.5 as a regression and <0.6 as exceptional. If `family_comparison` is absent (older run), say so in one line instead of inventing numbers. + +Be terse. Only return the final summary + the PAR2 table — no narration. --- diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 000000000..06bc8b079 --- /dev/null +++ b/.gitattributes @@ -0,0 +1,2 @@ +# Binary research papers (docs/papers/) are stored via Git LFS, not as blobs. +*.pdf filter=lfs diff=lfs merge=lfs -text diff --git a/.gitignore b/.gitignore index 57d8ed76c..265e0f689 100644 --- a/.gitignore +++ b/.gitignore @@ -463,7 +463,10 @@ pip-selfcheck.json .idea .idea/** -smt2 +# top-level SMT2 examples/scratch dir only — anchored so it does NOT match the +# source dir src/dreal/smt2/ or the test fixtures under test/dreal/test/smt2/. +/smt2/ gcc_build past_compilations -benchmark/results/ \ No newline at end of file +benchmark/results/ +dreal_popl27 \ No newline at end of file diff --git a/CLAUDE.md b/CLAUDE.md index 52647de9d..f59ef6659 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -2,43 +2,70 @@ This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository. +## Docs index + +- `docs/architecture.md` — layers, ICP loop, Box, explanations, ODE/PM pointers +- `docs/contractors.md` — contractor types, composition, caching +- `docs/decisions.md` — topic-keyed ADRs (ODE backend, per-slice tube, feed faithfulness, underflow, backward narrowing) +- `docs/ode-integration.md` — CAPD ODE contractor mechanism, soundness invariants, input formats +- `docs/pattern-matching.md` — DeBruijn canonicalization, substitution_tree, symmetry filtering (CAV26) +- `docs/rounding.md` — FPU rounding regimes, phase-hoisting, typed doubles, source-hygiene lint rules +- `docs/benchmarking.md` — benchmark infrastructure, families, A/B, sweep, cross-solver comparison +- `docs/soundness-vs-completeness.md` — T-relation definitions, dReal guarantees, worked F1 example +- `docs/forall-semantics.md` — ∃∀ fragment: syntax, CE-guided contractor, nested-forall crash, QE limits, nested-quantifier project guide +- `docs/papers/` — foundational Gao et al. literature: companion summaries (δ-decidability/δ-complete/dReal-tool/∃∀) cross-referenced into the docs above, with paper↔code drift flagged (e.g. opensmt+realpaver → CaDiCaL+IBEX+CAPD) + +--- + ## Project Overview -dReal4 is a delta-complete SMT solver for nonlinear arithmetic over the reals. It takes SMT-LIB2 (`.smt2`) or Delta-Real (`.dr`) formatted formulas and checks satisfiability up to a precision parameter delta. The `cav26` branch holds pattern-matching/lemma-reuse research; `upgrade-ibex` (current) source-builds IBEX from the `ncsys-lab/ibex-lib@dreal-perf-patches` fork and uses CAPD as the sole ODE backend. +dReal4 is a delta-complete SMT solver for nonlinear arithmetic over the reals. It takes SMT-LIB2 +(`.smt2`) or Delta-Real (`.dr`) formatted formulas and checks satisfiability up to a precision +parameter delta. The `cav26` branch holds pattern-matching/lemma-reuse research; `upgrade-ibex` +(current) source-builds IBEX from the `ncsys-lab/ibex-lib@dreal-perf-patches` fork and uses CAPD +as the sole ODE backend. -## Build +--- -**Prerequisites** (macOS — ARM or x86 Homebrew; Rosetta no longer required): -- bison, flex, gmp, cadical (install via `/opt/homebrew/bin/brew` on Apple Silicon) -- CMake source-builds IBEX from `https://github.com/ncsys-lab/ibex-lib.git@dreal-perf-patches` (override the URL via `-DIBEX_GIT_REPOSITORY=file:///path/to/ibex-fork` for local-dev iteration against an unpushed checkout) and builds CAPD from source automatically +## Soundness vs. completeness (read before reporting either) -**Full build** (first time — creates `gcc_build/`): -```bash -./FULL_BUILD.sh -``` +dReal is **sound but δ-complete**; conflating them has cost real experiments here (the hull-grid +"F1" finding was filed as soundness when it was completeness, and got runs cancelled). -**Incremental build** (subsequent builds): -```bash -./BUILD.sh -``` +- **false `unsat`** (returns `unsat` on a δ-satisfiable φ) = **SOUNDNESS** violation — forbidden. + Soundness breaks only where a box is narrowed past a true model (wrong FPU rounding, truncated + ODE feed, strict-bound `nextafter`, scrambled model, underflow). +- **missed refutation / false `delta-sat`** = **COMPLETENESS** violation. Looser enclosures + weaken this, never soundness. -Both scripts build target `dreal4` with `-j8`. The binary is at `gcc_build/dreal4`. +**Mandate:** whenever you report, label, comment, or commit a soundness/completeness issue — +in chat, code, docs, or commit messages — append the model-theory characterization in parentheses. +Templates: `SOUNDNESS (asserts φ T-unsatisfiable on a T-satisfiable φ — false unsat)`; +`COMPLETENESS (asserts φ^δ T-satisfiable on a T-unsatisfiable φ — missed refutation)`. +Canonical reference: `docs/soundness-vs-completeness.md`. Model-theory depth: the +`smt-model-theory` skill. -**macOS note**: arm64-native builds work without Rosetta — IBEX `971f8eb0` (March 2025) added arm64-gaol support, and CAPD master uses its own `DoubleRounding` (via `CAPD_INTERVAL_TYPE=NATIVE`) so FILIB is not pulled in. The old `rosetta_cmake.sh`/`rosetta_lldb.sh` wrappers are vestigial. +--- -**Docker** (Linux hermetic verification via `Dockerfile.dreal_ubuntu`): -```bash -# The container's IBEX source-build clones from the GitHub fork; the build -# sandbox needs outbound HTTPS. For local-dev against an unpushed checkout, -# pass --build-arg or edit IBEX_GIT_REPOSITORY in CMakeLists.txt before build. -docker build -f Dockerfile.dreal_ubuntu -t dreal-linux-verify . -cat query.smt2 | docker run --rm -i dreal-linux-verify ./dreal4 --in --model -``` -Ubuntu 24.04 + clang-18 + bison-3.8.2 + flex-2.6.4 + cadical-3.0.0 + GMP 6.3.0 (all source-built inside the container). Docker on macOS may have `-j` filesystem bugs — reduce parallelism if you see bad file descriptor errors. +## Build + +End-user build guide for cloning the repo (prerequisites, native macOS/Linux, Docker): +`README.md`. Build-system configuration for modifying the build (`--version` wiring, CMake +git-version target, IBEX/CAPD source-build): `docs/build.md`. + +`./FULL_BUILD.sh` (first build — creates `gcc_build/`) and `./BUILD.sh` (incremental) build +target `dreal4` with `-j8`; binary at `gcc_build/dreal4`. Override IBEX source via +`-DIBEX_GIT_REPOSITORY=file:///path/to/ibex-fork` for local-dev against an unpushed checkout +(`CMakeLists.txt` pins the fork sha `d9930909`). + +**Docker** (Linux hermetic verification): after `docker build -f Dockerfile.dreal_ubuntu -t +dreal-linux-verify .`, run `cat query.smt2 | docker run --rm -i dreal-linux-verify ./dreal4 --in +--model`. Bad-fd `-j` caveat: `README.md`. + +--- ## Running Tests -Tests are built as `dreal4_cmake_test`. Build and run: ```bash cd gcc_build cmake --build . --target dreal4_cmake_test -j8 @@ -46,13 +73,23 @@ ctest # run all tests ./dreal4_cmake_test --gtest_filter="*Box*" # run a single test by name pattern ``` -Test sources live under `test/dreal/` mirroring `src/dreal/` structure (e.g., `test/dreal/util/test/box_test.cc`). +Test sources live under `test/dreal/` mirroring `src/dreal/` structure. + +**New test file footgun:** test sources are globbed at configure time (`file(GLOB_RECURSE)`, +no `CONFIGURE_DEPENDS`). A new `.cc` is only picked up after a CMake reconfigure (`cmake gcc_build` +or `FULL_BUILD.sh`). `BUILD.sh` and bare `cmake --build` silently skip new files — the suite +count going up is the tell. + +**Rounding-mode gate:** `./rounding_debug_gate.sh` builds the Debug target (`cmake-build-debug`) +and runs the suite; `DREAL_ASSERT_ROUNDING` only fires in Debug. Run it before merges, alongside +`./copy_lint.sh` (incremental clang-tidy copy + UB/perf gate). -**Known flaky tests (ignore until fixed):** three tests fail spuriously and are unrelated to solver correctness — a clean run is "569/572 with only these failing": -- `IfThenElseEliminatorTest.NestedITEs` and `IfThenElseEliminatorTest.ITEsInForall` — the ITE-elimination golden strings hard-code auxiliary-variable names (`ITE0`, `ITE1`, …) but the underlying counter is a process-global that other tests increment, so the expected vs actual names drift (`ITE0` vs `ITE3`) depending on test/registration order. A test-isolation bug, not a preprocessing bug. -- `Timer.Test1` — timing-threshold assertion that fails under load/scheduling jitter. +**Known flaky tests (ignore — unrelated to solver correctness):** a clean run is "585/588 with +only these failing": +- `IfThenElseEliminatorTest.NestedITEs` and `IfThenElseEliminatorTest.ITEsInForall` — process-global ITE counter causes auxiliary-variable name drift across test registration order +- `Timer.Test1` — timing-threshold assertion fails under load/scheduling jitter -These fail identically on a pristine tree (verified by stashing local changes), so they do not indicate a regression. When validating a change, confirm the failure set is exactly this trio. +--- ## Running the Solver @@ -63,145 +100,126 @@ These fail identically on a pristine tree (verified by stashing local changes), Key flags: `--precision `, `--produce-models`, `--logic `, `--verbose`. -## Architecture - -### Solving Pipeline - -1. **Parsing** (`src/dreal/smt2/`, `src/dreal/dr/`): Flex/Bison grammars generate parsers at build time into `cmake-build-*/parsers/`. Parsed commands go through a `Driver` → `Context`. - -2. **Preprocessing** (`src/dreal/util/`): Formulas are put through if-then-else elimination (`if_then_else_eliminator`), predicate abstraction (`predicate_abstractor`), and Tseitin CNF conversion (`tseitin_cnfizer`) before solving. - -3. **SAT Layer** (`src/dreal/solver/sat_solver.cc`): CaDiCaL solves the abstracted Boolean formula. Two logic modes: interval-based (`sat_solver_interval_logic.cc`) and model-based (`sat_solver_model_logic.cc`). +**CAPD ODE tuning:** `--ode-taylor-order` (default 12), `--ode-hull-grid` (4 — per-step sub-slice +count; lower widens enclosures (never a false-`unsat`). Since the 2026-06 centered-in-time tube +fix (`HULL_COMPLETENESS.md`) the per-slice range is mean-value-in-time, so the default tube sits +near CAPD precision and hull-grid is no longer a completeness knob; raise to 16+ only for +pathologically sharp invariants), +`--ode-backward` (true), `--ode-abs-tol`/`--ode-rel-tol` (1e-10), `--ode-max-step` (0=adaptive). +Full flag list + performance rationale: `docs/ode-integration.md` §Performance. 2026-06 retuning +campaign: `OPTIMIZATION_LOG.md`. -4. **Theory Layer** (`src/dreal/solver/theory_solver.cc`, `icp*.cc`): When SAT produces an assignment, the theory solver validates it via Interval Constraint Propagation (ICP). Both sequential (`icp_seq`) and parallel (`icp_parallel`) implementations exist. +--- -5. **Contractors** (`src/dreal/contractor/`): ICP works by iterating contractors — algorithms that shrink variable domains. Key contractors: - - `contractor_ibex_fwdbwd`: IBEX forward-backward propagation (main workhorse) - - `contractor_ibex_polytope`: Polytope relaxation - - `contractor_fixpoint`: Runs a contractor to fixpoint - - `contractor_seq` / `contractor_join`: Sequential and disjunctive composition - - `contractor_ode_lohner`: ODE contractor wrapping CAPD's order-10 `IOdeSolver` + `ITimeMap` (`contractor_odes_capd.{h,cc}`). The trivial-flow short-circuit (every RHS is literal 0) bypasses CAPD and just intersects X_0 ∩ X_t. `--visualize` produces step-by-step CAPD enclosures via `run_capd_trace`. CAPD divergence on a Prune call silently skips narrowing for that call. The previous Codac/CAPD gated hybrid was retired; see `CODAC_MIGRATION.md`. - -6. **Pattern Matching / Lemma Generation** (`src/dreal/util/pattern_matching/`): CAV26 feature — generates lemmas from previously solved subproblems to prune future search via `substitution_tree` and `lemma_generator`. Randomization in `substitution_tree.cc` iteration is a recent optimization. - -### Key Data Structures - -- **`Box`** (`src/dreal/util/box.h`): The central solution type — a map from `Variable` to `ibex::Interval`. Represents both the current search space and satisfying witnesses. -- **`Variable` / `Expression` / `Formula`** (`src/dreal/symbolic/`): Vendored from Drake. Symbolic algebra layer with hash-consing. -- **`ContractorStatus`** (`src/dreal/contractor/contractor_status.h`): Carries the current `Box` plus metadata through contractor composition. - -### Vendored Third-Party Code (`src/third_party/`) - -Do not modify these unless necessary — they are external projects vendored in: -- `com_github_robotlocomotion_drake/`: Drake's symbolic expression library -- `com_github_khizmax_libcds/`: Lock-free concurrent data structures -- `com_github_progschj_threadpool/`: Thread pool for parallel ICP -- `com_github_pinam45_dynamic_bitset/`: Bitset for variable index sets -- `com_github_dreal-deps_picosat/`: PicoSAT (legacy, mostly unused) - -### Auto-downloaded Dependencies - -CMake fetches and builds at configure time: -- **IBEX** (`ncsys-lab/ibex-lib@dreal-perf-patches`, source-built via ExternalProject from `${IBEX_GIT_REPOSITORY}` defaulting to `https://github.com/ncsys-lab/ibex-lib.git`; override to `file:///path/to/ibex-fork` for local-dev iteration). 7 surgical patches on top of mainline `ibex-team/ibex-lib` (lazy-grad, backward callback, parser.yc ADL fix, mathlib arm64-Linux, plus 3 callback audit fixes for vector/matrix args, reference aliasing, and `EmptyBoxException` precision); see `../ibex-fork/MIGRATION.md`. Installed into `gcc_build/ibex-install/`. -- **CAPD** (`CAPDGroup/CAPD@b353e170`, master pin for in-development `6.1.0`, `CAPD_INTERVAL_TYPE=NATIVE`): Built from source via ExternalProject into `gcc_build/capd-install/`. Native intervals (CAPD's own `DoubleRounding`) skip FILIB and work on ARM64. -- **fmt**, **spdlog**, **nlopt**: Via FetchContent -- **GTest**: Via FetchContent - -Codac and Eigen3 are no longer dependencies. See `DEPENDENCIES.md` for the current stack and `CODAC_MIGRATION.md` for the historical migration narrative. - -### Vendored PicoSAT - -`com_github_dreal-deps_picosat/` is legacy and effectively unused. The SAT solver was upgraded to CaDiCaL early in `main`'s history (after a brief revert back to PicoSAT confirmed CaDiCaL was the right choice). Don't touch PicoSAT code. +## Architecture -## Branch Lineage and History +See `docs/architecture.md` (full pipeline, ICP loop, Box, explanations), `docs/contractors.md` +(types and composition), `docs/ode-integration.md` (ODE), `docs/pattern-matching.md` (CAV26 PM). -This project started as a CMake port of the original dReal4 (which used Bazel). The `main` branch holds the stable base; research branches layer experiments on top. +**Vendored third-party** (`src/third_party/`): Drake symbolic, libcds, threadpool, +dynamic_bitset, PicoSAT (legacy, unused). Do not modify without cause. -**`main`**: Foundation work — CMake build, IBEX upgrade (2.7.4 → 2.8.9), PicoSAT → CaDiCaL upgrade, core performance fixes (lambda callbacks to avoid `Box` copies, O(N²) explanation matching fix, `Variable::get_id()` inlining, FPU rounding mode guards), and the initial trie-based pattern matching data structure. +**Auto-downloaded:** IBEX (`ncsys-lab/ibex-lib@dreal-perf-patches`, sha `d9930909`), CAPD +(`b353e170`, `CAPD_INTERVAL_TYPE=NATIVE`), fmt, spdlog, nlopt, GTest. See `DEPENDENCIES.md` for +build wiring; `../ibex-fork/MIGRATION.md` for the 12 ibex-fork patch catalog. -**`fmcad25-experiments`**: First serious research branch. Added: -- The core "learned clause" pattern matching idea: when the theory solver produces an explanation (UNSAT witness), pattern-match it against known lemmas and inject reuse into the SAT solver via `CaDiCaL::Learner`. -- A neural-network-based "WORTH IT" heuristic for deciding when pattern matching pays off (later ripped out in `cav26` in favor of simpler thresholds). -- `FMCAD25_MODE_*` compile-time macros for benchmarking modes. -- The concept of "underconstrained models" in `context_impl.cc`. -- Application target: analog/mixed-signal circuit verification (SAR-ADC benchmarks, ASPLOS circuit problems). +--- -**`tacas26-odes`**: Extends `fmcad25-experiments` with full ODE support: -- Added `Integral` and `ForallT` AST node types to the Drake symbolic library. -- Parser backward-compatibility with dReal3's ODE input format (`.dr` files using `d/dt[x] = ...` syntax). -- Ported the CAPD contractor from dReal3 and wired it into the existing contractor framework. -- ODE symbol table in the parser/driver; `LookupOde(double)` for dReal3 compat. -- `--visualize` flag and JSON flow dumps for ODE trajectory visualization. +## Branch map -**`upgrade-ibex`** (current): The post-Codac-elimination architecture, on top of `tacas26-odes`. IBEX is source-built from `ncsys-lab/ibex-lib@dreal-perf-patches` (7 surgical patches catalogued in `../ibex-fork/MIGRATION.md`). CAPD master is the sole ODE backend. -- ODE contractor in `contractor_odes.cc`: forward via `run_capd_fwd` (CAPD `IOdeSolver` order-10 (tunable `kCapdTaylorOrder`), forward integration of `f(x)`, terminal intersection with X_t, backward sweep from narrowed X_t via `-f(x)` for joint narrowing of X_0); backward via `run_capd_bwd` (one-shot backward image via the cached `-f(x)` IMap); `run_capd_trace` for `--visualize`. -- Per-flow `CapdOdeCache` holds both the forward `f(x)` and the negated `-f(x)` `capd::IMap` objects, built once and reused per flow. `IOdeSolver` instances are constructed per-call because they carry mutable step state. The trivial-flow short-circuit bypasses CAPD entirely when every RHS is literal 0. -- `contractor_ibex_fwdbwd::Prune` uses the IBEX fork's `Function::backward` callback patch to populate the output bitset directly without a before/after snapshot. +| branch | purpose | +|---|---| +| `main` | stable CMake base; CaDiCaL, IBEX 2.8.9, core perf fixes | +| `fmcad25-experiments` | first PM research; NN heuristic; SAR-ADC application | +| `tacas26-odes` | ODE AST nodes (`Integral`, `ForallT`); CAPD contractor; dReal3 `.dr` compat | +| `upgrade-ibex` **(current)** | post-Codac; IBEX fork (12 patches); per-slice ODE tube | +| `cav26` | DeBruijn PM; `substitution_tree`; symmetry filtering | -**`cav26`**: Replaces the old trie-based pattern matcher with a fundamentally different approach: -- **DeBruijn canonicalization** (`debruijn_canonical.cc`): Converts AST terms to a canonical alpha-equivalent form using De Bruijn indices, so structurally identical formulas up to variable renaming hash the same. -- **`substitution_tree.cc`**: Efficient alpha-bijection checking. `substitutions_map` "forward"/"backward" terminology refers to the two directions of the bijection being maintained during matching. -- **Flat-vector `substitutions_map`**: Replaced `std::unordered_map` with a flat vector for cache-friendliness. -- **Symmetry filtering** (`context_impl.cc`): CAV26's main contribution — filters redundant lemmas at the lemma level using variable symmetry information. `CAV26_NOT_PURE_ANY` tags mixed symmetries. -- **Dummy Variables**: Variables with negative IDs are internal/dummy variables used by the pattern matcher; not real solver variables. -- Removed all heuristic infrastructure (`predicate_heuristic.cc`, `pattern_matching_heuristic.cc`) that was in earlier branches. -- PM thresholds and timeouts are now CLI-configurable (`--drpm-max-size`, `--drpm-max-time`) instead of compile-time. -- Randomized iteration order in `substitution_tree.cc` to avoid biasing towards early-indexed variables when a timeout interrupts matching. +--- ## Benchmarking -Run `/benchmark` after every meaningful code change. This is the primary regression-detection mechanism during active development — run it frequently, not just before commits. Suggest it proactively at natural breakpoints even if the user doesn't ask. +Run `/benchmark` after every meaningful code change. Run proactively at natural breakpoints. -**Infrastructure** (`benchmark/` directory): -- `baseline.csv` — frozen DRPM_0L reference times for 102 benchmarks (good_benchmarks.csv subset) -- `state.json` — persistent anomaly/exceptional tracker; updated automatically each run -- `run_batch.sh` — parallel runner: reads TSV from stdin, runs each with `gtime -v -o` and `timeout 300` -- `select.py` — picks 8 random benchmarks + all current anomalies; outputs TSV (csv_name TAB filepath) -- `parse_results.py` — parses gtime output + solver stdout into `summary.csv` -- `aggregate.py` — compares vs baseline, flags regressions/exceptional, updates `state.json` -- `results/` — per-run output directories (gitignored) +- `/benchmark` — ~8-12 benchmarks, Haiku subagent interprets, 2-4 sentence summary +- `/benchmark-baseline` — full baseline (43 odeexpr + ~10 each other family) -**Skills** (invoke from Claude Code prompt): -- `/benchmark` — runs ~8-12 benchmarks in parallel, spawns a Haiku subagent to interpret results, reports back 2-4 sentence summary with regression/exceptional counts -- `/benchmark-baseline` — runs ~30 benchmarks to establish a fresh local baseline (use before branch merges or when exceptional list grows stale) +**Thresholds:** PAR2 >1.5× baseline = regression; <0.6× = exceptional; SAT↔UNSAT flip = immediate +escalation. CPU time (user+sys), not wall clock. -**Thresholds**: regression if PAR2 time >1.5× baseline (PAR2 = actual time if solved, 2× timeout = 600 s if TIM/OOM/ERR); exceptional if PAR2 time <0.6× baseline. Correctness flips (SAT↔UNSAT) are always escalated immediately regardless of timing. +**Benchmark sources:** +- `~/Documents/new_dreal/ode_expressivity/benchmarks/` — odeexpr family (43 `.smt2`) +- `~/Documents/new_dreal/nraode_to_nra/drealgithub_sunoct5/rolled/` — github_oct5_ +- `~/Documents/new_dreal/nraode_to_nra/VNAMSCwI_satoct11/rolled/` — tacas_c2e2_ +- `~/Documents/new_dreal/AMS-verification-bundle-of-sticks/saradc/rolled/` — 1mhz_ -**Benchmark sources** (raw `.smt2` files, not in this repo): -- `~/Documents/new_dreal/nraode_to_nra/drealgithub_sunoct5/rolled/` — github_oct5_ family -- `~/Documents/new_dreal/nraode_to_nra/VNAMSCwI_satoct11/rolled/` — tacas_c2e2_ family -- `~/Documents/new_dreal/AMS-verification-bundle-of-sticks/saradc/rolled/` — 1mhz_ family +Full infrastructure (run_batch.sh, select.py, do_ab.sh, do_sweep.sh, families/weighting, +cross-solver comparison): `docs/benchmarking.md`. -**Manual invocation** (if not using the skill): -```bash -python3 benchmark/select.py | bash benchmark/run_batch.sh benchmark/results/run_$(git rev-parse --short HEAD)_$(date +%s) -python3 benchmark/parse_results.py -python3 benchmark/aggregate.py -``` +--- ## Verification discipline -When reporting "tests pass" or "build green," confirm which artifact (commit, build dir, container image) the verification actually ran against. The trap to avoid: ctest reports a pass against `build-old-pin/` (a proven baseline) while changes are on a new branch with a fresh build dir — the report says "tests pass" but the new code was never exercised. +When reporting "tests pass" or "build green," cite the artifact: build dir, commit, or container +image. The trap: ctest reports a pass against `build-old-pin/` (a proven baseline) while the new +build dir is never exercised. -Always run the verification command against the new artifact explicitly and cite the build dir / commit / image tag in the report (e.g. "ctest against `build-final/` at HEAD ``: 537/539"). +--- ## Key Design Notes -**dReal3 backward compatibility is intentional.** The DR parser (`src/dreal/dr/`) handles the older dReal3 ODE syntax. Don't break this. - -**`auditor.cc`** (`src/dreal/solver/auditor.cc`) is a development/verification tool. It reprints learned lemmas in dReal3-compatible format so they can be re-checked by dReal3 independently. It is not part of the core solving loop. - -**FPU rounding mode** (read this before touching any interval/ODE code — the failure mode is extremely sneaky): the solver controls the FPU rounding mode explicitly via `RoundingModeGuard` (`src/dreal/util/rounding_mode_guard.h`), which sets a mode on construction and restores the *previous* mode on destruction. Two interval backends with **conflicting** ambient-mode expectations coexist: - -- **gaol** (IBEX's interval backend) is sound only under **`FE_UPWARD`**. Under any other mode its directed rounding inverts (`lo > hi`), so an inexactly-FP-representable subexpression collapses to an *empty* interval. -- **CAPD** (ODE backend) expects **`FE_TONEAREST`**; its `DoubleRounding` sets directed modes per-op and restores nearest. Crucially, **linking CAPD leaves the process FPU in `FE_TONEAREST`** (its static init / `roundNearest()`), so there is no longer a safe ambient mode to assume. - -Invariant: **every gaol↔CAPD boundary must establish its mode explicitly — never rely on the ambient FPU state.** gaol-using code (the ibex contractors) guards `FE_UPWARD`; CAPD-using code guards `FE_TONEAREST`. Concretely: `ContractorIbexFwdbwd::Prune` guards `FE_UPWARD` (added after CAPD's `FE_TONEAREST` clobber caused a false-UNSAT regression — see below); `contractor_ode_lohner::Prune` / `generate_trace` / the CAPD cache build guard `FE_TONEAREST`. The `brancher.cc` `DREAL_ASSERT_ROUNDING(FE_UPWARD)` only *asserts* the invariant (and is compiled out under `NDEBUG`), it does not establish it. - -The sneaky part: a wrong ambient mode does **not** crash or warn — it silently produces an inverted interval that empties the box, surfacing as a **false `unsat`** (delta-complete soundness is violated) only on formulas containing inexact constant arithmetic inline in inequalities (e.g. `(* 3.3 x)`, `(* C (pow 10 -N))`). It is invisible on exactly-representable values (`0.5`, `0.25`, `*1.0`). Regression test: `test/dreal/api/test/gaol_directed_rounding_false_unsat_test.cc`. Historical guards also live in `prefix_printer.cc`. Don't add floating-point/interval code without an explicit `RoundingModeGuard` for the backend it touches. - -**`filter_assertion` soundness**: There was a soundness bug where strict upper bounds were handled incorrectly due to a wrong `nextafter()` call. The `forward`/`backward` naming in `substitutions_map` also had a soundness bug that was fixed. Be careful around strict vs. non-strict inequality handling in contractors and the SAT interval logic. - -**ODE performance baseline**: Pre-Codac-elimination benchmarking confirmed CAPD order-20 was at or below Codac CtcLohner runtime on all tested ODE benchmarks (cardiac, prostate, bouncing-ball families). See `CODAC_MIGRATION.md` for the historical benchmark tables. The `--capd-t-gate` / `--capd-ndim-gate` CLI flags have been removed — they were only meaningful under the old Codac/CAPD gated hybrid. - -**Benchmarking instrumentation**: Several `std::cerr` prints and JSON dumps exist specifically for benchmarking runs. Log levels (TRACE/DEBUG/INFO) are tuned so that `--verbose` (DEBUG) is useful for development without flooding output on large queries. TRACE is for deep debugging only. +**dReal3 backward compatibility is intentional.** The DR parser (`src/dreal/dr/`) handles the +older dReal3 ODE syntax. Don't break this. + +**`auditor.cc`** (`src/dreal/solver/auditor.cc`) reprints learned lemmas in dReal3-compatible +format for independent re-checking. Not part of the core solving loop. + +**FPU rounding mode:** Read `docs/rounding.md` before touching any interval/ODE/printing code. +The failure mode is a **silent false `unsat`** — wrong ambient mode inverts gaol's directed +rounding with no warning, invisible on exactly-representable constants. Two regimes: +`FE_UPWARD` (gaol/interval → `UpwardRoundingScope`) and `FE_TONEAREST` (CAPD/formatting → +`NearestRoundingScope`). Mode established once per ICP phase, not per contractor call. Two +sanctioned clobberers (`ExpectClobber` tag): CAPD adapters and ibex's interval `operator<<`. + +**Source-hygiene lint:** `python3 lint.py` (regex routing) + `./rounding_debug_gate.sh` (lint + +Debug ctest) + `./copy_lint.sh` (clang-tidy copy/UB/perf gate). Key forbidden patterns in +`src/dreal/`: raw `.mid()`/`.diam()` (→ `safe_mid`/`safe_diam`), raw +`ibex::Function::backward` (→ `ibex_hc4_backward`), raw `std::to_string` feeding CAPD (→ +`to_capd_string`), interval from scalar `+`/`-` (→ `make_sound_interval`), `arr[i++]`/`arr[++i]` +subscript (BUG-005 scrambled-model class). Full rules: `docs/rounding.md`. + +**`filter_assertion` soundness:** strict bound handling had a wrong `nextafter()` call — fixed. +`substitutions_map` forward/backward naming had a soundness bug — fixed. Take care around strict +vs. non-strict inequalities in contractors and the SAT interval logic. + +**ODE feed faithfulness** (`to_capd_string` precision): constants render at 17 sig figs; +`std::to_string`'s 6-digit truncation was a false-`unsat` soundness bug. Details: +`docs/decisions.md` "ODE feed faithfulness" and `docs/ode-integration.md` §Soundness. + +**Denormal/underflow soundness** (dreal/dreal4#321): sound in two layers (ibex HC4-backward +`underflow_saturate` + Drake `sound_constant_fold`). Full record + accepted delta-completeness +tradeoff: `docs/decisions.md` "Denormal / underflow soundness". + +**ODE performance baseline:** CAPD order-20 was at or below Codac CtcLohner on all tested ODE +benchmarks. The `--capd-t-gate`/`--capd-ndim-gate` flags have been removed (Codac hybrid retired). +Details: `docs/decisions.md` "ODE backend". + +**`forall` vs `forall_t` are independent machinery (`forall-vs-forall_t`).** `forall` = the +∃∀ NRA quantifier (`Formula::Forall` → `ContractorForall`, `Kind::FORALL`, CE-guided; +`docs/forall-semantics.md`). `forall_t` = the ODE trajectory invariant (`FormulaKind::ForallT`, +checked per-slice in `contractor_ode_lohner` / `Kind::ODE_LOHNER`; +`docs/qf_nra_ode_semantics.md` §5). Same prefix, unrelated code paths — never swap them. The +docs were confused here once (a mislabeled contractor); grep `forall-vs-forall_t` for the +anchored warnings, and `docs/forall-semantics.md` §7 for the canonical side-by-side. + +**Negated/unlinked ODE constraints (BUG-002):** a negated `integral`/`forall_t`, and a `forall_t` +not linked to an integral (invariant must reference the endpoint var `x_t`, not the flow var `x`), +are silently dropped in `link_integral_invariants` — a COMPLETENESS hazard (missed refutation, +never false-`unsat`). This can't be made a throw there (it runs inside DPLL(T) on transient search +literals; throwing crashes valid BMC benchmarks); rejection must be parse-layer (unimplemented). +Desired future semantics is specified as aspirational `GTEST_SKIP` tests in +`test/dreal/smt2/test/dreal_future.cc`. Details: `docs/decisions.md` "Negated / unlinked ODE +constraints", `docs/ode-integration.md`. + +**Benchmarking instrumentation:** `std::cerr` prints and JSON dumps exist for benchmarking runs. +`--verbose` (DEBUG) is useful for development; TRACE is deep debugging only. diff --git a/CMakeLists.txt b/CMakeLists.txt index 2f26c2c2d..19406d998 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -2,10 +2,34 @@ cmake_minimum_required(VERSION 3.16) project(dreal4_cmake) include(CMakePrintHelpers) +find_package(Git QUIET) +if(NOT GIT_FOUND) + set(GIT_EXECUTABLE git) +endif() +set(GIT_VERSION_HEADER "${CMAKE_BINARY_DIR}/git_version.h") +# Always-run target: git queries are fast; copy_if_different in the script +# means git_version.h timestamp (and thus dreal_main.cc recompilation) only +# updates when the hash or dirty status actually changes. +add_custom_target(git_version_h + COMMAND "${CMAKE_COMMAND}" + "-DGIT_EXECUTABLE=${GIT_EXECUTABLE}" + "-DOUTPUT_FILE=${GIT_VERSION_HEADER}" + -P "${PROJECT_SOURCE_DIR}/cmake/GenerateGitVersion.cmake" + COMMENT "Capturing git version info" + VERBATIM +) + set(CMAKE_VERBOSE_MAKEFILE ON) set(CMAKE_CXX_STANDARD_REQUIRED ON) set(CMAKE_CXX_STANDARD 17) +# Emit gcc_build/compile_commands.json so clangd/editors resolve 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 to find it: +# ln -sf gcc_build/compile_commands.json compile_commands.json +# Survives a fresh FULL_BUILD.sh (which reconfigures without -D flags). +set(CMAKE_EXPORT_COMPILE_COMMANDS ON) + # NOTE: CMAKE_OSX_ARCHITECTURES is no longer forced to x86_64. # CAPD (the original x86-only ODE library) has been replaced with Codac, which # supports ARM64 natively. If you need to override (e.g. for cross-compilation), @@ -82,6 +106,14 @@ add_library(dreal4_cmake STATIC ${BISON_smt2_parser_OUTPUTS} ${FLEX_smt2_scanner_OUTPUTS} ${BISON_dr_parser_OUTPUTS} ${FLEX_dr_scanner_OUTPUTS} ) +# -frounding-math tells the compiler not to assume a fixed FPU rounding mode, so it +# cannot constant-fold or reorder FP arithmetic across fesetround calls. dReal runs +# gaol/ibex under FE_UPWARD and formatting/CAPD under FE_TONEAREST; without this flag +# Clang's #pragma STDC FENV_ACCESS ON support is incomplete and the directed-rounding +# ops in rounded_interval.h (sub_up/sub_down/add_up/add_down) could be silently +# mis-compiled. gaol itself is already compiled with -frounding-math by IBEX's +# CMakeLists; this covers dReal4's own source. PUBLIC propagates to dreal4 and tests. +target_compile_options(dreal4_cmake PUBLIC -frounding-math) target_include_directories(dreal4_cmake PUBLIC "${PARSERS_HOME}" "${PROJECT_SOURCE_DIR}/src/" @@ -113,7 +145,7 @@ target_link_libraries(dreal4_cmake PUBLIC "${CADICAL_LIB}") # --------------------------------------------------------------------------- # IBEX via ExternalProject — source-built from the dReal team's fork # -# The fork carries seven surgical patches on top of ibex-team/ibex-lib@master: +# The fork carries eleven surgical patches on top of ibex-team/ibex-lib@master: # 1. function: lazy-init gradient (perf-critical, ~65% of Function::init) # 2. Function::backward callback (perf-critical, eliminates HC4 snapshot) # 3. parser.yc namespace-qualify apply() (Linux/clang ADL fix) @@ -121,7 +153,14 @@ target_link_libraries(dreal4_cmake PUBLIC "${CADICAL_LIB}") # 5. fire backward callback for non-scalar args (soundness: callback audit) # 6. copy old-value in backward callback to avoid alias (soundness: callback audit) # 7. HC4Revise: report partial narrowings on EmptyBoxException (soundness: callback audit) -# See ../ibex-fork/MIGRATION.md for the divergence catalog. All seven are +# 8. gaol: Interval::log/pow soundness gaps (strict-< for ub==0, fractional pow) +# 9. gaol: inline aarch64 FPCR rounding fast-path (perf: ARM64 transcendental fesetround) +# 10. gaol: batch the nearest-rounding region in transcendentals (perf: ~8% on odeexpr) +# 11. function: empty domains via return-status instead of EmptyBoxException +# (perf: removes __cxa_throw unwinding from the HC4 backward hot path) +# 12. gaol: underflow_saturate backward targets (soundness: dreal/dreal4#321 — +# bwd_pow/exp/sqr/mul/div no longer false-unsat on subnormal-band targets) +# See ../ibex-fork/MIGRATION.md for the divergence catalog. All twelve are # candidate upstream PRs; once they land, drop the fork and point at # ibex-team/ibex-lib directly. # @@ -138,7 +177,12 @@ include(ExternalProject) set(IBEX_INSTALL_DIR "${CMAKE_BINARY_DIR}/ibex-install") set(IBEX_GIT_REPOSITORY "https://github.com/ncsys-lab/ibex-lib.git" CACHE STRING "Git repository for the ibex fork (override with file://path for local dev)") -set(IBEX_GIT_TAG "dreal-perf-patches" +# Pinned to the fork HEAD sha (reproducible) rather than the moving branch ref. +# d9930909 = the 12-patch series; patch #12 adds underflow_saturate so HC4 +# backward ops stop false-unsat'ing on subnormal-band targets (dreal/dreal4#321). +# Bump when fork patches land. (Local-dev iteration still works via +# -DIBEX_GIT_TAG= and -DIBEX_GIT_REPOSITORY=file:///path/to/ibex-fork.) +set(IBEX_GIT_TAG "d99309094850efb84e2ebc11a62ee655d690639f" CACHE STRING "Git ref for the ibex fork (branch, tag, or sha)") set(EP_ARCH_ARGS "") @@ -297,6 +341,13 @@ target_link_libraries(dreal4_cmake PUBLIC "${GMP_C_LIB}" "${GMP_CXX_LIB}") # executable add_executable(dreal4 "${PROJECT_SOURCE_DIR}/src/dreal/dreal_main.cc") target_link_libraries(dreal4 PRIVATE dreal4_cmake) +add_dependencies(dreal4 git_version_h) +target_include_directories(dreal4 PRIVATE "${CMAKE_BINARY_DIR}") +target_compile_definitions(dreal4 PRIVATE + DREAL_BUILD_OS="${CMAKE_SYSTEM_NAME}" + DREAL_BUILD_OS_VERSION="${CMAKE_SYSTEM_VERSION}" + DREAL_BUILD_ARCH="${CMAKE_SYSTEM_PROCESSOR}" +) # tests diff --git a/CODAC_MIGRATION.md b/CODAC_MIGRATION.md deleted file mode 100644 index 3b19da95c..000000000 --- a/CODAC_MIGRATION.md +++ /dev/null @@ -1,442 +0,0 @@ -# Codac Migration - -> **STATUS (2026-06-08): RESOLVED — Codac has been removed.** This document is -> retained as historical context. The current architecture: source-built IBEX -> from `ncsys-lab/ibex-lib@dreal-perf-patches` (7 surgical patches on top of -> mainline; see `../ibex-fork/MIGRATION.md`) + CAPD master (sole ODE backend, -> with a CAPD-based `run_capd_trace` for `--visualize`). See `DEPENDENCIES.md` -> for the current stack. -> -> The performance regression analysis below correctly identified the -> `Function::init` gradient allocation as the dominant cost. The resolution -> (the lazy-grad patch) is now a candidate upstream PR rather than a -> downstream-only hack. - -Replaced `ncsys-lab/ibex-lib` + `ncsys-lab/capdDynSys-4.0` with Codac v2 + `lebarsfa/ibex-lib`. - -## Motivation - -Both forked dependencies were unmaintained snapshots requiring heavy local patches for correctness and platform support (ARM64/Rosetta, C++17, interval semantics). Codac v2 (https://www.codac.io) is actively maintained, supports ARM64 natively, wraps `lebarsfa/ibex-lib`, and provides a cleaner ODE API via `CtcLohner`. Some breaking changes in ODE semantics were accepted as the cost of getting onto a maintained stack. - -## Accepted trade-offs - -| Trade-off | Notes | -|---|---| -| One extra `IntervalVector` copy per `fwdbwd` backward pass | Restores pre-callback behavior; critical for lemma quality (see Migration phases below) | -| Gradient always allocated in upstream IBEX | **Major CPU cost, not memory.** `sample` profiling on `1mhz_k20_saradc_2b_box_4a_-1e` (see "Re-investigation 2026-06-07" below) shows ~65% of total wall time inside `ibex::Gradient::Gradient(ibex::Eval&)` and `ibex::ExprLinearity::ExprLinearity`, both called unconditionally from `ibex::Function::init`. `Function::backward` (the only IBEX entry point fwdbwd actually uses) takes the `_hc4revise` path and never touches `_grad`. ncsys-lab's `_grad = nullptr` hack was load-bearing for this Prune-time cost; lebarsfa's stock build pays it on every cache miss in `TheorySolver::contractor_cache_`. **This is the dominant component of the post-migration non-ODE slowdown.** See "Open lines of attack" item 7 for the IBEX-source-patch path. | -| Tube-based ODE semantics | Codac's `CtcLohner` operates on `SlicedTube`s, not step-by-step CAPD integration | -| Taylor order 2 (vs CAPD's order 20) | Hardcoded in Codac internals; primary source of ODE-benchmark slowdown | - -## Status - -- [x] Phases 1–5: CMake restructuring, `fwdbwd` callback removal, ibex_converter API check, ODE contractor rewrite, doc updates -- [x] `./FULL_BUILD.sh` succeeds on ARM64 macOS -- [x] ODE benchmarks produce correct results (with documented exceptions; see "Known issues") -- [x] Three iterative optimization passes landed (see "Performance timeline") - ---- - -## Migration phases (completed) - -**Phase 1 — CMake restructuring.** `CMakeLists.txt` switched from `FetchContent` of the old IBEX fork plus `ExternalProject` of CAPD+FILIB to two `ExternalProject_Add` blocks: `ibex_external` (`lebarsfa/ibex-lib@ibex-2.8.9.1`) installs into `gcc_build/ibex-install/`, then `codac_external` (`codac-team/codac@v2.0.2`, `WITH_CAPD=OFF`) installs into `gcc_build/codac-install/`. `CMAKE_OSX_ARCHITECTURES=x86_64` override removed — ARM64 native works. - -**Phase 2 — `contractor_ibex_fwdbwd.cc` callback removal.** Upstream IBEX has no per-variable callback on `Function::backward()` (that was our fork's patch). Restored pre-callback behavior: snapshot before, compare after, populate the "changed variables" set the lemma pipeline downstream consumes. **Why this matters for lemma quality:** the "changed" set feeds the conflict clause that the pattern matcher learns from. Without it, lemmas contain the whole model and are useless for reuse. The naïve full-box snapshot was replaced in Pass 2 with an input-restricted thread-local snapshot — see "Performance timeline". - -**Phase 3 — `ibex_converter.cc` API check.** No code changes needed; the IBEX 2.8.x expression-tree API (`ExprSymbol::new_`, `ExprConstant::new_scalar`, `NumConstraint`, `System`, `CtcPolytopeHull`, `LinearizerXTaylor`, `cleanup`) is stable across forks. Only `#include` paths shifted to `IBEX_INSTALL_DIR`. - -**Phase 4 — ODE contractor rewrite.** `contractor_capd_full` and its CAPD-string converter (`to_capd_string.h`) were deleted; `contractor_odes_codac.{h,cc}` is the new implementation, compiled as C++20. The current shape is described in "Current implementation" below. - -**Phase 5 — Documentation.** This file, `CLAUDE.md`, and `DEPENDENCIES.md` were rewritten. - ---- - -## CAPD v6 ARM64 path (active — gated hybrid) - -> **Updated 2026-06-06.** CAPD master (in-development `6.1.0`) now exposes -> `CAPD_INTERVAL_TYPE` as a clean CMake variable. With -> `-DCAPD_INTERVAL_TYPE=NATIVE`, `capdExt/CMakeLists.txt` skips -> `add_subdirectory(filibsrc)` entirely and CAPD's own ARM64-capable -> `DoubleRounding` becomes the interval backend. **The two-file -> FILIB-bypass patch documented below is no longer needed.** What follows -> is preserved as a historical artifact; the live build wiring is the -> `ExternalProject_Add(capd_external)` block in `CMakeLists.txt` pinning a -> recent master SHA (currently `b353e170`, 2026-05-18). The contractor -> runs alongside Codac's `CtcLohner` as a gated second backend; see -> "CAPD-Lohner gated hybrid" below. - -After measuring the early 26× ODE perf gap, restoring CAPD as the primary backend via CAPD v6.0.0 was attempted and reverted. The v6.0.0 source unconditionally required FILIB, which fails to build on ARM64. With master, that blocker is solved upstream — CAPD is now reintroduced as a gated second contractor (see below). - -### What was implemented (then reverted) - -- `src/dreal/contractor/odes/contractor_odes_capd.cc` — CAPD Taylor-order-20 integration using `capd::IOdeSolver` (order 20), `capd::C0Rect2Set`, adaptive stepping, 16-sub-interval curve evaluation, intersection-based enclosure filter. -- `CMakeLists.txt` — `ExternalProject_Add(capd_external)` for CAPD v6.0.0. -- ODE string format `"var:x,v;fun:v,(-9.8);"` for `capd::IMap`. - -All changes were reverted via `git checkout --` on the modified files after the failure was diagnosed. - -### Why it was abandoned - -CAPD v6.0.0 unconditionally depends on FILIB for directed rounding. FILIB's `CMakeLists.txt` has a `FATAL_ERROR` for any non-x86_64 platform: - -``` -capdExt/filibsrc/CMakeLists.txt: - if(x86_64) ... else() FATAL_ERROR "Unknown or unsupported processor architecture." -``` - -The failure chain: -1. CAPD root `CMakeLists.txt`: unconditionally `add_dependencies(capd filib)` + `-D__USE_FILIB__` -2. `capdExt/CMakeLists.txt`: unconditionally `add_subdirectory(filibsrc)` -3. `capdExt/filibsrc/CMakeLists.txt`: FATAL_ERROR on non-x86 - -`-DCAPD_INTERVAL_TYPE=NATIVE` does **not** exist in CAPD v6.0.0 (hallucinated CMake option). `__USE_NATIVE__` also does not exist. - -### The correct ARM64 fix (for future reference) - -CAPD v6 already ships ARM64 `DoubleRounding` in `capdAlg/src/capd/rounding/DoubleRounding.cpp` (uses `msr fpcr` assembly). Without `__USE_FILIB__`, `capd::interval` = `Interval` — fully ARM64-capable. The only fix needed is skipping FILIB on ARM64. - -**Two-file patch** (deliverable via `PATCH_COMMAND` in `ExternalProject_Add`): - -`CMakeLists.txt` — wrap FILIB dependency: -```cmake -if(CMAKE_SYSTEM_PROCESSOR MATCHES "arm64|aarch64") - message(STATUS "ARM64: using CAPD native DoubleRounding intervals (no FILIB)") - target_compile_options(${PROJECT_NAME} PUBLIC -O2 -frounding-math) -else() - add_dependencies(${PROJECT_NAME} filib) - target_compile_options(${PROJECT_NAME} PUBLIC -D__USE_FILIB__ -O2 -frounding-math) - target_link_libraries(${PROJECT_NAME} PUBLIC filib) -endif() -``` - -`capdExt/CMakeLists.txt` — guard `filibsrc`: -```cmake -if(NOT CMAKE_SYSTEM_PROCESSOR MATCHES "arm64|aarch64") - add_subdirectory(filibsrc) -endif() -``` - -If the ODE perf gap ever becomes unacceptable, this patch plus reconstructing `contractor_odes_capd.cc` from the session transcript is the primary path to restoring CAPD Taylor-order-20. - ---- - -## CAPD-Lohner gated hybrid (current) - -CAPD is back as a *second* ODE contractor running alongside `CtcLohner`. The plan, the per-step rationale, and the decision tree are in `codac_docs/analysis/codac_capd_extension_assessment.md` and the project plan file. Summary of what landed: - -- **Build wiring** (`CMakeLists.txt`). `ExternalProject_Add(capd_external)` pins CAPD master SHA `b353e170` (2026-05-18) and passes `-DCAPD_INTERVAL_TYPE=NATIVE` so FILIB is skipped on ARM64. CAPD installs into `gcc_build/capd-install/` as a single `libcapd.a` + headers under `include/capd/`. The `capd_imported` IMPORTED target sets `INTERFACE_COMPILE_DEFINITIONS=__USE_NATIVE__` so consumers pick up the matching template instantiations. -- **Contractor TU** (`src/dreal/contractor/odes/contractor_odes_capd.{h,cc}`). Mirrors the Codac TU's surface and lifetime model: per-flow `CapdOdeCache` holding two `capd::IMap` instances (`f(x)` for forward integration, `-f(x)` for backward); per-call `capd::IOdeSolver(order=20)` + `capd::ITimeMap` (these carry mutable step state, so not shared across parallel ICP workers). The string builder lives in `src/dreal/contractor/odes/to_capd_string.h` (forward-ported from the pre-Codac-migration version). Same `unordered_map` + `shared_ptr` ownership pattern as `make_codac_ode_cache` — closes the same pointer-reuse hazard. -- **Dispatch / gate** (`contractor_odes.cc::Prune`). After the parameter intersect / T=0 / invariant steps, Prune evaluates `use_capd = (t_ub > capd_t_gate) || (n_state_vars >= capd_ndim_gate)`. On a true gate, CAPD runs first; if it diverges (`GlobalEnclosureError`-equivalent, parser failure, or null cache) we fall back to Lohner. The Codac `m_codac_cache` is always built — the trivial-flow short-circuit and Lohner fallback both rely on it. -- **CLI flags**. `--capd-t-gate ARG` (double, default `5.0`) and `--capd-ndim-gate ARG` (int, default `6`). Set `--capd-t-gate 1e18 --capd-ndim-gate 1000000` to disable CAPD entirely; use `--capd-t-gate 1e-300 --capd-ndim-gate 1` to force CAPD on every Prune. Note: both flags use positive-value validators and reject `0` — the help text saying "set 0" is wrong. -- **Soundness gates**. `test/dreal/contractor/test/contractor_odes_semantic_test.cc` now ships 26 tests across four fixtures: - - 7 original (Lohner under default gates) — trivial / decay / mock-prostate × FWD/BWD plus the BWD interior-point preservation gate - - 7 `_Capd`-suffixed (`MakeCapdForcedConfig` forces `(t_gate=0, ndim_gate=0)`) — same instances, CAPD path - - 9 new gate-dispatch tests — long-horizon at `t_ub=20` (CAPD triggered via t-gate), gate boundary at `t_ub=4.99` vs `5.01`, backend-consistency (Lohner-forced vs CAPD-forced) on the same instance, and trivial-flow short-circuit precedence over the CAPD gate at `t_ub=20` - - 3 `SixDimDecayTest` — 6-dimensional decoupled decay exercising the `capd_ndim_gate` branch (n=6 ≥ gate=6) independent of the t-gate - Plus a sibling 26-test file `test/dreal/contractor/test/to_capd_string_test.cc` covering the Expression → CAPD `IMap` string translator (constants incl. scientific-notation round-trip + negative wrap, variables, every supported `ExpressionKind` incl. `tan` → `sin/cos`, `abs` → `sqrt(sqr)`, `sinh`/`cosh`/`tanh` → exp-form, and `if_then_else` throws). All 52 pass. - The aggregate.py ground-truth flip classifier in `benchmark/aggregate.py` is the next-layer tripwire — any flip against an annotated `_SAT`/`_UNS` benchmark is escalated as `SOUNDNESS REGRESSION`. - -### Benchmark validation (2026-06-07, PAR2-corrected) - -`/benchmark-baseline` rerun against HEAD (`bd8a7ce99`) on the 30-benchmark stratified sample with PAR2 scoring (TIM/OOM/ERR entries penalized at 2× timeout = 600 s). PAR2 is the correct metric for SMT benchmarking: a benchmark that transitions from TIM to solved *lowers* the PAR2 average, while the old raw-average approach silently excluded timed-out entries from both sides and gave a misleading picture. - -Family PAR2 averages vs the CAV26 *frozen* `baseline.csv` (CAPD-x86-Rosetta historical times): - -| Family | n | Frozen PAR2 avg | Local PAR2 avg | Ratio | -|--------|---|-----------------|----------------|-------| -| github | 10 | 74.69 s | 425.30 s | 5.69× | -| tacas | 10 | 115.03 s | 300.41 s | 2.61× | -| saradc | 10 | 73.17 s | 567.11 s | 7.75× | - -Net: the ARM64/Codac-v2 stack is substantially slower than the old x86/Rosetta CAPD+IBEX stack across all three families under PAR2 scoring. The prior analysis (which showed github "flat" at 0.97× and tacas "2.3× faster") was an artifact of excluding timed-out benchmarks from the family average on both sides — those benchmarks now correctly contribute 600 s each to the local PAR2 average. The dominant component of the across-the-board non-ODE slowdown is now root-caused: see "Re-investigation 2026-06-07" below for the gradient-allocation finding and "Open lines of attack" item 7 for the fix. The CAPD-Lohner hybrid vs the prior Lohner-only state of `upgrade-ibex` is still a strict improvement (zero regressions; the two formerly-TIM'd SARADC benchmarks now solve, lowering their contribution from 600 s each to their actual solve times). - -### Pre-existing stale test note - -`test/dreal/contractor/test/contractor_capd_test.cc` (`ContractorCapdFullTest.{CapdFwd,CapdBwd}`) is a dReal3-era port whose output-bit expectations assumed a contractor doing BVP-style time narrowing. Neither current Lohner nor the new CAPD contractor performs that inverse-time reasoning — they compute reachable sets at the *given* `t_ub`. Test expectations were realigned to match current behavior; the test is now pinned to the Lohner backend (`--capd-t-gate 1e18` equivalent) so its mechanical-invariant checks stay stable regardless of any future CAPD tuning. The dReal3 BVP-style narrowing is not on the implementation roadmap; the semantic tests above are the source of truth for soundness. - -### Tuning gates from benchmark sweeps - -`kDefaultCapdTGate=5.0` and `kDefaultCapdNdimGate=6` are pre-measurement guesses, not optimized values. The intended workflow is: - -1. Run `/benchmark-baseline` to relock the regression baseline with the new contractor in place. -2. Sweep `--capd-t-gate ∈ {2, 5, 10}` × `--capd-ndim-gate ∈ {4, 6, 10}` on a representative subset including `bouncing_ball`, `quad`, `cardiac`, and the SARADC family. -3. Pick the lowest gate that doesn't hurt easy benchmarks (Lohner-friendly thin tubes) and update the defaults in `src/dreal/solver/config.h`. - ---- - -## Current implementation - -All ODE-contractor source lives under `src/dreal/contractor/odes/`. The C++17 surface (`contractor_odes.{h,cc}`) drives `Prune`; the C++20 translation unit (`contractor_odes_codac.{h,cc}`) wraps Codac. - -- **`CodacOdeCache`** — opaque to C++17, defined in the C++20 TU. Holds the translated `codac2::AnalyticFunction` and a `codac2::CtcLohner` instance (its `contract` is `const`, safe to share across parallel ICP workers). Constructed once per flow; reused on every `Prune`. -- **Global per-`OdeFlow*` cache.** Static `unordered_map` under a static `std::mutex`, where `CacheSlot { shared_ptr flow, shared_ptr cache }`. Keyed by raw `OdeFlow*` for fast lookup; the slot's `shared_ptr` keeps the keyed flow alive so the address cannot be reused while the entry is live (this closes the pointer-reuse hazard previously listed under "Known issues" — see resolved-issues note). `make_codac_ode_cache` takes `shared_ptr` to make the ownership contract explicit. Process-scoped. -- **FWD direction** — `run_lohner_integration` uses `CtcLohner` with `TimePropag::FWD_BWD`, `contractions=2`, `eps=0.1`, and adaptive `n_steps = clamp(max(n_steps_hint, ceil(t_ub * 2)), n_steps_hint, 60)` with `n_steps_hint = 20`. Catches `codac2::GlobalEnclosureError` and returns without pruning (sound but incomplete on stiff dynamics). -- **BWD direction** — `run_lohner_bwd_oneshot` uses `codac2::LohnerAlgorithm(&cache->fn, h, /*forward=*/false, u0)` with `u0 = X_t`, iterating `algo.integrate(1)` for `n_steps` (same adaptive formula). Returns `algo.getLocalEnclosure()` as the backward image of `X_t` at real time 0. Default `contractions=1`. Soundness rests on the BWD swap analysis below. -- **Trivial-flow short-circuit.** At cache build time, walk the flow's `ode_list`; if every RHS is `is_zero`, set `cache->trivial = true`. `Prune` then takes the `T=0` branch (`X_0 ∩ X_t` componentwise) and never enters CtcLohner. Handles `d/dt[d] = 0` planning benchmarks with 1280 modes. -- **Trace / visualization** — `run_lohner_trace` uses `LohnerAlgorithm` directly for the `--visualize` path. - -`Prune` flow (`contractor_odes.cc`): (1) intersect parameter vars; (2) `T=0` shortcut (intersect state vars at endpoints); (3) check invariants at `X_0` via IBEX contractors (negated invariants logged-and-skipped — see `docs/qf_nra_ode_semantics.md` §6); (4) call into FWD or BWD `run_lohner_*` based on `m_dir`. - ---- - -## Performance timeline - -**Pass 1 — Per-flow cache + CtcLohner reuse + trivial-flow short-circuit + `contractions=2`.** Pre-cache, `build_ode_fn` re-walked the symbolic RHS tree and constructed a brand-new `AnalyticFunction` on every `Prune`. With `N_modes × 2` contractors built and many `Prune` calls each, translation cost was a real bottleneck (especially for the 15-var quad flow with sin/cos sub-trees). The cache amortizes translation to ~1× per distinct flow per process. `contractions=2` (was 5) was the empirical speed/tightness sweet spot. Pass 1 also skipped BWD's Step 4 entirely as a stopgap because the `m_vars_0 ↔ m_vars_t` constructor swap made `CtcLohner FWD_BWD` ask the wrong question (the forward-image question on swapped gates, not the backward image); Pass 3 restored a sound BWD direction. - -**Pass 2 — Adaptive `n_steps` + `contractor_ibex_fwdbwd::Prune` snapshot restriction.** `run_lohner_integration` had `n_steps = 20` hardcoded, so `h = t_ub / 20` scaled linearly with horizon: at `t_ub = 30` (cardiac), `h ≈ 1.5` was too coarse for order-2 Taylor — CtcLohner spent its contractions budget widening the per-step enclosure back to soundness instead of narrowing. Pass 2 introduced `n_steps = clamp(max(20, ceil(t_ub * 2)), 20, 60)` — keeps the 20-step floor so short-horizon benchmarks (bouncing ball, fedor, normal) are unchanged, only adds steps when `t_ub > ~10`. Independently, Pass 2 replaced the Phase-2 full-box snapshot in `contractor_ibex_fwdbwd::Prune` with a `thread_local std::vector>` saving only the constraint's free-var intervals (typically 2–10 of a 50–500-variable box). `thread_local` is safe because `Prune` is never invoked recursively. Steady-state per-call allocation drops to zero once buffer capacity saturates. - -**Pass 3 — BWD contractor restoration via `LohnerAlgorithm(forward=false)`.** Pass 1's BWD Step 4 skip was unsound in the worst case (could let a false δ-SAT through if BWD was the load-bearing narrower); Pass 3 added `run_lohner_bwd_oneshot` so the BWD contractor computes a real backward image. Soundness rests on: every concrete `x_0 ∈ X_0` reaching some point of `X_t` under forward dynamics must lie in the backward image of `X_t`, so removing states outside that image is sound. Verified by seven semantic-soundness gates on trivial / decay / mock-prostate fixtures (see `test/dreal/contractor/test/contractor_odes_semantic_test.cc`) and by a ground-truth-aware regression classifier in `benchmark/aggregate.py` that distinguishes soundness regressions (flips against annotated ground truth) from completeness improvements (refutations of spurious δ-witnesses, which are silent under Pass 3). Cost: ~50% of one `CtcLohner FWD_BWD` call per BWD `Prune` — bouncing ball went 2.8 s → 4.2 s; this is the floor. - ---- - -## Headline numbers (current) - -ARM64 macOS, `upgrade-ibex` HEAD post-Pass-3. Baselines from `benchmark/baseline.csv` (CAV26 reference times). - -| Benchmark | Baseline | Current | Net | Notes | -|---|---|---|---|---| -| `bouncing_ball_with_drag_10_0` | ~0.5 s (CAPD order-20, x86 Rosetta) | ~4.2 s | 8.4× slower | Order-2 floor; CAPD v6 fix above is the way out | -| `0hz_k64_cardiac_new_cardiac` | 85 s | ~120 s | 1.4× slower | Adaptive `n_steps` recovered most of the headroom | -| `github_oct5_0hz_k4_cardiac_new_cardiac` | 29 s | ~5 s | 6× faster | Long-horizon win from adaptive `n_steps` | -| `tacas_c2e2_k10_NOR__sigmoid_SAT` | 142 s | 0.8 s | 170× faster | Pass 2 | -| `tacas_c2e2_k11_inverter_ramp_SAT` | 103 s | 2.1 s | 48× faster | Pass 1 cache | -| `tacas_c2e2_k17_NOR__sigmoid_UNS` | TIM | 13.6 s | resolved | Pass 2 | -| `tacas_c2e2_k21_NOR__sigmoid_SAT` | 234 s | 7.7 s | 30× faster | Pass 2 | -| `0hz_k32_cardomain_car-8-flat-linear` | 49 s | 0.7 s | 70× faster | Pass 1 | -| `0hz_k64_cardomain_car-8-flat-nonlinear` | 66 s | 0.5 s | 130× faster | Pass 1 | -| `0hz_k128_quad_quad2-1` | 38 s | TIM (>300 s) | regressed | 15-var ODE with sin/cos; order-2 Taylor is the ceiling | -| `0hz_k1280_planning_one-var` | 31 s | TIM | regressed | Trivial flow + huge mode count; SAT layer dominates | -| `0hz_k2_prostate_prostate_p10` | 42 s | TIM | regressed | Coupled rational dynamics; see "Known issues" | - ---- - -## What we tried but reverted - -- **`contractions=1` on CtcLohner.** Bouncing ball improved (3.3 s → 2.5 s) but cardiac fell off a cliff (108 s → TIM at 90 s budget) — wider per-step enclosures forced many more ICP bisections, net-slower. Kept at `contractions=2`. -- **`contractions=1` with adaptive `n_steps`.** Tried because smaller `h` might compensate for wider per-step enclosure. Didn't measure better on cardiac and risked bouncing ball. Reverted. -- **Aggressive `n_steps = clamp(ceil(t_ub * 10), 5, 50)`** (the heuristic Pass 1 doc suggested). Reduced steps for medium-horizon benchmarks: bouncing ball went 3 s → 4.25 s mid-ICP as `t_ub` narrowed. Replaced with the floor-preserving max policy now in place. -- **`inflate_by = max_rad × 2`** (was `× 10`) for the tube envelope. Bouncing ball unchanged (~3.0 s); cardiac unchanged within noise. Envelope width isn't the bottleneck. Kept at `× 10` for headroom on untested dynamics. -- **Tighter CtcLohner `eps`** (default `0.1`). Risks `GlobalEnclosureError` on dynamics we haven't tested. Left at default. -- **Skipping the entire BWD contractor** (not just its Step 4). Considered to halve ICP passes through ODE constraints. Rejected because invariant checking (Step 3) at the X_0 endpoint is direction-aware via the swap and contributes genuine narrowing. Step-4-only skip kept that — see Pass 3 for the eventual sound restoration. -- **Skipping CtcLohner when `t_ub` is small** (early-out for short tubes where the envelope contains both gates and no narrowing is possible). Cheap check but rarely fired — by the time it would matter, ICP had already narrowed `t_ub`. Removed. -- **Memoizing `CtcLohner::contract` results by `(X_0, X_t, t_ub)`.** Boxes monotonically shrink during ICP, so cache hit rate ~0. Not implemented. -- **Splitting FWD into two passes** (`TimePropag::FWD` then `TimePropag::BWD`) to interleave `nl_ctcs` propagation. Bookkeeping in `Prune` (gates from `tube.first_slice()` vs `tube.last_slice()`) doesn't compose cleanly across two contract calls without sharing the tube object. Deferred — see "Open lines of attack" item 5. -- **`TimePropag::FWD` only on the FWD contractor** (Open lines of attack item 3 — first attempt). Attempted post-Pass-3 on the theory that Pass 3's BWD contractor now lands `X_0` narrowing soundly and the FWD pass's `TimePropag::BWD` direction is now redundant work. `github_oct5_0hz_k4_cardiac_new_cardiac` flipped UNSAT → δ-SAT (3.3 s) — the suspicious soundness-direction flip, surfaced by the new ground-truth-aware classifier. Reverted. Lesson: FWD's BWD pass was carrying narrowing that the BWD contractor alone (with `LohnerAlgorithm` `contractions=1`) doesn't replicate. Re-attempt would need either bumped BWD `contractions` or compensation elsewhere; relock the local baseline first per item 3. - ---- - -## What we learned (tribal knowledge) - -### Codac `CtcLohner` knobs (verified by reading `codac-install/include/codac-core/codac2_CtcLohner.h`) - -- `CtcLohner(const AnalyticFunction& f, int contractions = 5, double eps = 0.1)` -- `void contract(SlicedTube& tube, TimePropag t_propa = FWD_BWD) const` -- **Taylor order is hardcoded to 2** in the `LohnerAlgorithm` private members (`_z` is the order-2 Taylor-Lagrange remainder per the field comment). Not exposed as a public knob; would need a Codac patch. -- `eps` is the inflation parameter for the **internal** global enclosure inside CtcLohner. Not the same as our outer `init_box.inflate(...)` factor. -- User-facing levers: `contractions`, `eps`, `TimePropag`, `n_steps` (via the `TDomain`'s `dt = t_ub / n_steps`), initial tube envelope width. Everything else (Taylor order, step adaptation, parallelotope basis updates) is internal. - -### dReal-side cost model for ODE Prune - -For an ODE-heavy benchmark with `N_modes` modes and `K` ICP iterations: -- Pre-cache, per-`Prune` was dominated by `build_ode_fn` for complex flows. With per-flow caching, translation cost amortizes to ~1× per distinct flow. -- Post-cache, per-`Prune` is dominated by `CtcLohner::contract`: `contractions × n_steps × |t_propa|` AnalyticFunction evaluations. At `n_steps=20`, `contractions=2`, `FWD_BWD`, that's 80 step-evaluations per Prune, each doing multivariate Taylor expansion on the ODE RHS. -- Tube allocation (`SlicedTube`, `TDomain`, gate `set`) is non-trivial but smaller than the contraction itself. - -### Why naïve per-Prune box snapshots are expensive in `contractor_ibex_fwdbwd` - -The Phase-2 callback removal originally took a full `iv_before = iv` + `std::set` of changed indices. The downstream loop only consults `changed_vec` for bits already in `input()` (the constraint's free vars, typically 2–10 of a 50–500-variable box). Snapshotting the whole interval vector was paying for information that was thrown away. The Pass-2 fix uses a `thread_local std::vector>` saving only the constraint's free-var intervals — O(|free_vars(f)|) instead of O(|box|). Important because most non-ODE benchmarks spend the majority of theory-solver time in this Prune. - ---- - -## Open lines of attack - -Items below survive into ongoing work. Item 2 from earlier passes (proper backward-direction integration) landed in Pass 3 and is removed from this list. - -1. **Detect partially-trivial flows.** A flow with `d/dt[x] = 0` for some state vars and non-zero for others currently uses CtcLohner on the whole vector. Splitting into "trivial sub-vector" (just intersect X_0 ∩ X_t) and "active sub-vector" (CtcLohner on the reduced system) shrinks the `AnalyticFunction` dimensionality and per-step work. Implementation cost is higher because the dimension reduction has to be plumbed through the gate reading/writing. - -2. **Static `flow_cache_map` eviction at end of solve.** Currently caches accumulate for the lifetime of the process — and the post-fix `CacheSlot` holds a `shared_ptr` that pins each flow in memory until the process exits. Fine for a single-query CLI; problematic if dReal is ever embedded in a long-running service. Add a hook in `Context` destruction to clear flow caches whose `OdeFlow` is no longer referenced elsewhere; a `weak_ptr`-based key (or content-hash key) would let unused entries collect themselves as a follow-on. - -3. **`TimePropag::FWD` only on the FWD contractor.** Cuts CtcLohner's internal work in half but only narrows `X_t`. Now that Pass 3's BWD contractor lands `X_0` narrowing soundly via `LohnerAlgorithm(forward=false)`, this is the natural follow-on. Worth measuring on benchmarks where the BWD contractor is the load-bearing narrower (cardiac, prostate). Re-lock the regression baseline before measuring. - -4. **Tighter `eps` parameter** on `CtcLohner`. Default `0.1` controls the algorithm's internal global enclosure inflation. Tightening might converge in fewer contractions. Risks `GlobalEnclosureError` on stiff dynamics — needs careful benchmark sweep. - -5. **Splitting FWD into two passes** (`TimePropag::FWD` then `TimePropag::BWD`) to interleave `nl_ctcs` propagation between directions. Bookkeeping needs to share the tube object across calls — requires refactoring `run_lohner_integration`. Deferred but tractable. - -6. **Fuzz the BWD contractor with sympy-derived polynomial closed-form fixtures.** Pass 3 verified soundness on seven hand-picked fixtures (trivial flow, linear decay, mock-prostate rational coupling). Random RHS within a polynomial template would harden confidence further. Especially valuable on dynamics with closed-form solutions where ground-truth flips are easy to detect. - -7. **Restore the `_grad = nullptr` patch on IBEX — via a fork of `ibex-team/ibex-lib`.** Highest-payoff non-ODE item. The 2026-06-07 re-investigation showed ~65% of saradc wall time is spent in `ibex::Function::init` building `_grad` — work `Function::backward` never uses. **The recommended path is now to fork `ibex-team/ibex-lib` directly and drop Codac entirely** (see "Strategic reassessment 2026-06-07" below for the full rationale and benchmark evidence). The fix then requires: - - Fork `ibex-team/ibex-lib` (not `lebarsfa/ibex-lib` — see below for why). - - Apply gradient patch to the fork: lazy-init `_grad` in `Function::gradient(...)` / `Function::deriv_calculator()` (set to nullptr in `init`, build on first use). Option (b) — `IBEX_NO_GRAD_INIT` CMake flag — also works but is noisier. Skipping `ExprLinearity` init is a separate ~37% win on top; same lazy-init pattern applies to `_lin`. - - Switch `ibex_external` in `CMakeLists.txt` from the prebuilt-zip download to `ExternalProject_Add` building from our fork's source with appropriate ARM64 configure flags (gaol/ultim, no FILIB). Drop the `codac_external` block entirely; remove `contractor_odes_codac.{h,cc}` and `codac-install/` references. CAPD becomes the sole ODE backend. - - No `IBEXConfig.cmake` is needed — dreal4's CMakeLists.txt already wires IBEX manually as `ibex_imported` / `ibex_gaol` / `ibex_ultim` IMPORTED targets, bypassing `find_package(IBEX)`. The `IBEXConfig.cmake` requirement was only for Codac's own build. - - Address the `std::apply` ADL conflict in IBEX's Bison-generated parser (affects both macOS and Linux source builds; a one-liner forward-declaration patch). - - Verification: re-run `1mhz_k20_saradc_2b_box_4a_-1e` + `/benchmark-baseline` post-patch; expect saradc PAR2 average to drop ~3× from 567 s toward ~190 s, github similarly. - Effort: ~half-day for a careful patch; changes are contained to `CMakeLists.txt` + a small upstream-IBEX diff + removal of the `contractor_odes_codac.{h,cc}` TU. - ---- - -## Re-investigation 2026-06-07: root-causing the non-ODE slowdown - -Triggered by the user observation that "long-standing non-ODE slowdown from the Codac migration" was written before Pass 2 landed and had never been independently re-profiled. The 2026-06-07 PAR2 numbers (github 5.69×, tacas 2.61×, saradc 7.75×) made the gap large enough to be worth a focused investigation. - -### Method - -- `1mhz_k20_saradc_2b_box_4a_-1e.smt2` chosen as probe — frozen baseline 48 s, small enough to iterate on. -- Saradc benchmarks were checked first for `(integral_...)` / `(forall_t ...)` terms — zero matches. The `(set-logic QF_NRA_ODE)` header is dReal3-compat boilerplate; the actual ODE contractor never fires. So the ODE-side rewrites (CtcLohner, CAPD hybrid, BWD restoration) are mechanically irrelevant for saradc. -- A temporary `ContractorIbexPolytopeStat` was added to `contractor_ibex_polytope.cc` mirroring the fwdbwd one. `--polytope` is off by default — polytope never fires on saradc, so the polytope full-box snapshot at the old `contractor_ibex_polytope.cc:88` was not on the saradc critical path. (The Pass-2-equivalent fix landed anyway, since it's a strict improvement for `--polytope` users.) -- `dreal4 --verbose info` stat dumps + `sample 30` (macOS profiler) on the probe. - -### Findings - -| Stat (from `--verbose info` end-of-run dump) | Value | -|---|---| -| Total CheckSat (Theory level) | 400 | -| Total time in CheckSat | **77.20 s** | -| Total ibex-fwdbwd Pruning calls | 109,819 | -| Total time in Pruning | 0.022 s | -| Total ibex-converter Convert calls | 877 | -| Total time in Converting | 0.004 s | -| Total ibex-polytope Pruning | (never fired — polytope disabled by default) | - -The pruning hot path is essentially free (0.022 s for 110 K calls). The ~77 s in theory CheckSat is unaccounted for by any existing stat. - -`sample` resolves the missing 77 s precisely: -- 100% of samples → `dreal::TheorySolver::CheckSat` → `BuildContractor` → `make_contractor_ibex_fwdbwd` → `ContractorIbexFwdbwd::ContractorIbexFwdbwd` → `ibex::Function::Function` → `ibex::Function::init` -- **~65% inside `ibex::Gradient::Gradient(ibex::Eval&)`** — called unconditionally from `Function::init` -- **~37% inside `ibex::ExprLinearity::ExprLinearity`** (a child of Gradient ctor; walks the expression tree categorizing each sub-tree as linear / nonlinear / constant via `visit(ExprMul)`, `visit(ExprAdd)` etc.) -- The dominant micro-cost is `operator new` for `TemplateDomain` builds inside each `visit(ExprMul)` — many small heap allocations per gradient construction. - -These costs are paid on every cache miss in `TheorySolver::contractor_cache_` (the per-formula contractor cache at `theory_solver.cc:179, 198`). For this probe: 877 cache misses × ~88 ms each = ~77 s, matching the unaccounted CheckSat time. `Function::backward` (the path fwdbwd actually uses for HC4Revise contraction) **never reads `_grad`** — the gradient is constructed, immediately discarded, and rebuilt the next time a new formula is seen. - -### Diagnosis vs the original "Pre-existing correctness flips" framing - -The original framing (this doc lines 308-320 pre-update) said the `.n` correctness flips were "likely IBEX fork upgrade + Phase-2 callback removal" — same broad attribution but no specific mechanism. The 2026-06-07 profile is more precise: the *timing* component of the regression is the gradient-allocation cost. The *correctness* component (SAT↔UNSAT flips on water-double-network, airplane-single-network, gen, thermostat) is unrelated to the gradient finding and remains open as a separate soundness investigation. - -The "saradc/frozen ratio is the long-standing non-ODE slowdown from the Codac migration" line that prompted this investigation was **correct in attribution** (the migration introduced it via the IBEX fork swap) but **wrong in framing** (it was treated as a fundamental loss when in fact the upstream-IBEX `_grad = nullptr` patch is a small, well-understood fix). The trade-off table at the top of this doc is updated to reflect this. The "Open lines of attack" item 7 captures the fix path. - -### What landed in this round - -- Polytope contractor at `src/dreal/contractor/contractor_ibex_polytope.cc::Prune` now uses the input-restricted thread_local snapshot recipe from `contractor_ibex_fwdbwd.cc` (Pass-2 trick). Quiet win for `--polytope` users; no effect on default-config saradc which never hits polytope. -- Temporary `ContractorIbexPolytopeStat` block left in place — useful for future investigations under `--polytope --verbose info`. Drop if/when it becomes noise. -- Stale claim at the pre-update line 320 ("`1mhz_k28_saradc_3b_box_4a_-1e` family TIMs at HEAD without any of the optimization-pass changes") was wrong: that benchmark now solves in 279 s per the 2026-06-06 baseline. Updated. - -### What did *not* land (deferred to a follow-on session) - -The IBEX-source-patch path described in "Open lines of attack" item 7. That work is contained but requires switching `ibex_external` from prebuilt-zip to source-build + applying a small upstream diff + verifying it doesn't break gaol/ultim — substantial enough to be its own session. - ---- - -## Soundness analyses - -### Correctness analysis of the BWD swap (load-bearing argument for Pass 1's Step-4 skip and Pass 3's `LohnerAlgorithm(forward=false)` restoration) - -Let `f` be the forward ODE dynamics. The Integral constraint says: - -> ∃x(·): dx/dt = f(x) ∧ x(0) ∈ X_0 ∧ x(t_ub) ∈ X_t. - -The **FWD** contractor (no swap) builds a `SlicedTube` with `gate_0 = X_0` (codac t=0) and `gate_t_ub = X_t` (codac t=t_ub), then runs `CtcLohner FWD_BWD`. This computes the intersection of trajectories of `dx/dt = f(x)` passing through both gates — the correct constraint. Both endpoint gates get narrowed soundly. - -The **BWD** contractor (constructor swaps `m_vars_0 ↔ m_vars_t`) ends up with `gate_0 = X_t` and `gate_t_ub = X_0` and the *same* `dx/dt = f(x)` analytic function. `CtcLohner FWD_BWD` on this tube finds trajectories of forward dynamics from `X_t` (at codac t=0) to `X_0` (at codac t=t_ub). For a non-time-symmetric ODE, the set of points in `X_t` with a forward trajectory landing in `X_0` is **not** equal to the backward-image of `X_t` under `f`, which is what soundness for the original constraint demands. So BWD's CtcLohner narrowing could remove valid endpoint values → false UNSAT. - -Pass 1's response: skip BWD Step 4 entirely. Sound but lossy (BWD never narrows `X_0`). - -Pass 3's response: replace BWD Step 4 with `run_lohner_bwd_oneshot`, which uses `LohnerAlgorithm(&cache->fn, h, /*forward=*/false, u0 = X_t)`. This is the genuine backward image: `LohnerAlgorithm` with `forward=false` integrates the *backward* dynamics `du/dτ = -f(u)` starting from `X_t` at `τ = 0`, producing at `τ = t_ub` the set of forward-pre-images of `X_t`. Intersecting that with the current `m_vars_t` (= original `X_0`) is sound: every concrete `x_0 ∈ X_0` whose forward trajectory hits `X_t` must lie in this pre-image set. - -The chosen mechanism (`LohnerAlgorithm` rather than a second `AnalyticFunction` with `dx/dt = -f(x)`) shares the cache slot per flow and avoids re-translating the RHS. A `-f(x)`-based alternative remains available as a fallback if benchmarks show looseness from the single-shot `LohnerAlgorithm` path. - -### Pass 3 verification methodology (ground-truth-aware classification) - -The prior "any SAT↔UNSAT flip aborts" criterion was replaced. dReal is sound + delta-complete: a baseline `delta-sat` can be a spurious δ-witness, and a tighter contractor refuting it is a *completeness improvement*, not a soundness bug. - -Three pieces of infrastructure landed alongside the code change: - -- **`benchmark/baseline.csv` + `benchmark/baseline_local.csv` `ground_truth` column** — populated only from filename conventions (VNAMSCwI `_SAT`/`_UNS`, SARADC `-1e`/`5000e`). dReal3 is not propagated; it has the same δ-completeness limitations as dReal4 and is not authoritative. -- **`benchmark/aggregate.py` flip classifier** — emits `CORRECTNESS IMPROVEMENT` (flip toward annotated ground truth), `SOUNDNESS REGRESSION` (flip away from it), or `UNDETERMINED FLIP` (no annotation). The previous blanket "correctness regression" alert now fires only on SOUNDNESS. Adds a frozen-baseline fallback so flips on anomaly-list rows missing from `baseline_local.csv` aren't invisible. -- **`test/dreal/contractor/test/contractor_odes_semantic_test.cc`** — closed-form-derived soundness gates for FWD and BWD on three ODE families: trivial (`dx/dt = 0`), linear decay (`dx/dt = -x`), and mock-prostate coupled rational dynamics (`dx/dt = -x·z/(z+2), dz/dt = -z`). Each gate is a SAT-known instance; box must remain non-empty after Prune. The mock-prostate fixtures are the load-bearing case — rational coupling is the shape of dynamics where the suspected unsoundness might live. - -All 7 gates pass on HEAD and under the BWD-restoration experiment: - -``` -TrivialFlowTest.FwdInfeasible_BoxEmpties PASS / PASS -TrivialFlowTest.BwdInfeasible_BoxEmpties PASS / PASS -DecayFlowTest.FwdFeasible_BoxRemains PASS / PASS -DecayFlowTest.BwdFeasible_BoxRemains PASS / PASS -MockProstateTest.FwdFeasible_BoxRemains PASS / PASS -MockProstateTest.BwdFeasible_BoxRemains PASS / PASS -MockProstateTest.BwdFeasible_PreservesInteriorPoint PASS / PASS -``` - ---- - -## Known issues - -### Resolved: cache-key pointer-reuse bug in `make_codac_ode_cache` - -`make_codac_ode_cache` keyed its static `flow_cache_map` by raw `OdeFlow*`. If an `OdeFlow` was destroyed and a new one later allocated at the same address with different dynamics, the cache returned stale data for the new flow — surfaced reproducibly by the Pass-3 semantic tests when fixtures created and destroyed `OdeFlow`s between `TEST_F` instances. **Fixed in commit `fed8a02a1`**: the map now stores a `CacheSlot { shared_ptr flow, shared_ptr cache }` keyed by raw pointer; the held `shared_ptr` keeps the keyed flow alive while the cache entry is live, so the address cannot be reused. `make_codac_ode_cache`'s signature changed from `(const OdeFlow&, …)` to `(shared_ptr, …)` to make the ownership contract explicit. Eviction (see "Open lines of attack" item 2) is now the only remaining cache-lifetime concern, relevant only for embedded-service use. - -### Pre-existing correctness flips (not introduced by the migration optimizations) - -These benchmarks flip vs. the CAV26 baseline. The `.n` (non-ODE) cases cannot be the ODE contractor's fault. The `→ TIM` rows are the *timing* component of this regression and are now root-caused (see "Re-investigation 2026-06-07" above — gradient-allocation cost in `Function::init`, fixed by "Open lines of attack" item 7). The genuine SAT↔UNSAT flips (water-double-network, airplane-single-network) are a separate *soundness* concern that the timing fix does not address. - -| Benchmark | Baseline | Current | Notes | -|---|---|---|---| -| `0hz_k64_water_water-double-network-sat.drh.n` | SAT | UNSAT | `.n` file (no ODE); likely IBEX fork upgrade + Phase-2 callback removal | -| `0hz_k8_airplane_airplane-single-network-sat.drh.n` | SAT | UNSAT | `.n` file (no ODE); same root-cause hypothesis as above | -| `prostate_h2.drh.o` | δ-sat (11.27 s) | unsat (0.08 s) | UNDETERMINED ground truth. Working hypothesis: spurious δ-witness in baseline; Pass-3 BWD correctly refutes. Not a soundness regression by the aggregate.py classifier. | -| `prostate_cancer2_scaled`, `prostate_cancer_scaled_infix`, `prostate_p10` | δ-sat | unsat | Same hypothesis as `prostate_h2`. | -| `0hz_k256_gen_gen-0-multi-nonlinear.drh.n` | UNSAT | TIM | `.n` file; non-ODE regression | -| `0hz_k256_gen_gen-0-single-nonlinear.drh.n` | UNSAT | TIM | `.n` file; non-ODE regression | -| `0hz_k256_thermostat_thermostat-double-network-sat.drh.n` | SAT | TIM | `.n` file; non-ODE regression | - -Removing an unsound contractor can only **introduce** correctness flips by allowing the search into a false-SAT branch that the false-UNSAT was masking. Empirically this did not happen on any benchmark in the sampled batches across the three passes — every new EXCEPTIONAL was simply a benchmark finishing faster on a path that already exists. The prostate-family flips are best explained by the BWD restoration refuting spurious δ-witnesses, not by a regression. - -`1mhz_k28_saradc_3b_box_4a_-1e` was previously claimed to TIM at HEAD; it now solves in 279 s per the 2026-06-06 baseline. The remaining gap on this benchmark is the same gradient-allocation cost identified in "Re-investigation 2026-06-07" (~65% of wall time inside `ibex::Function::init`), not a separate SAT-layer issue. Open lines of attack item 7 closes the rest of the gap. - ---- - -## Strategic reassessment 2026-06-07: fork `ibex-team/ibex-lib` + eliminate Codac - -### Context - -Two paths exist for applying the gradient fix (Open lines of attack item 7) and resolving the fork-of-a-fork dependency chain: - -- **Option A** — Fork `lebarsfa/ibex-lib`, apply gradient patch, keep Codac. `lebarsfa` is 100+ commits behind `ibex-team/ibex-lib`, is not controlled by this project, and could fall arbitrarily far behind the mainline. Rebasing to ibex-team would require also porting lebarsfa's divergence. Codac itself is a prebuilt ZIP per-arch-per-OS that becomes a maintenance liability if it breaks on a new macOS or glibc release. - -- **Option B** — Fork `ibex-team/ibex-lib` directly, apply gradient patch, drop Codac. `IBEXConfig.cmake` (the only feature lebarsfa adds that we need) is only required by Codac's own CMake build — dropping Codac makes it unnecessary. dreal4's CMakeLists.txt already wires IBEX via manual IMPORTED targets and never calls `find_package(IBEX)`. This path gives full control, direct rebase access to the ibex-team mainline, and reduces the dependency tree to: our ibex-team fork + CAPD + dreal4. - -### Experiment: CAPD-forced vs Codac-default on ODE benchmarks - -Before committing to Option B, the performance of native ARM64 CAPD (order-20) was measured against Codac `CtcLohner` (order-2) across all available `integral`-based ODE benchmarks. Each benchmark run twice: once with default settings (Codac fires when `t_ub ≤ 5` and `n_state_vars < 6`) and once with `--capd-t-gate 1e-300 --capd-ndim-gate 1` (CAPD forced on every Prune). - -| Benchmark | State vars | Codac default | CAPD forced | Verdict | -|---|---|---|---|---| -| `bouncing_ball_with_drag_10_0` (10 modes, t_ub=3) | 2 | **4410 ms** | **3391 ms** | identical (δ-sat) | -| `cardiac_new_cardiac` (4 modes) | 5 | **8935 ms** | **8972 ms** | identical (unsat) | -| `prostate_h2` (2 modes) | ~4 | **19400 ms** | **18520 ms** | identical (δ-sat) | -| `prostate_h1` (32 modes) | ~4 | **14110 ms** | **14070 ms** | identical (unsat) | -| `prostate_cancer_scaled` (2 modes) | ~4 | **148 ms** | **149 ms** | identical (unsat) | - -**CAPD is never slower than Codac across all tested benchmarks, and is 23% faster on the canonical reference case (`bouncing_ball`) where Codac was supposed to be the fast path.** The reason: CAPD's higher Taylor order (20 vs 2) requires fewer timesteps per integration, and on native ARM64 the per-step overhead is low enough that fewer steps wins. No verdict differences were observed. - -The remainder of wall time on all benchmarks (including bouncing_ball) is dominated by the SAT layer, IBEX fwdbwd, and `forall_t` contractors — not the ODE backend — so the ODE-backend choice is not the performance bottleneck regardless. - -### Decision - -**Option B.** The performance argument for keeping Codac is eliminated by the experiment above. The remaining strategic considerations all favor Option B: - -- Full control over the IBEX dependency; direct rebase path from ibex-team mainline. -- Dropping Codac removes a per-arch-per-OS prebuilt ZIP and eliminates the lebarsfa dependency entirely. -- CAPD is already the better ODE backend. The gated-hybrid complexity (`contractor_odes_codac.{h,cc}`, `CodacOdeCache`, the dispatch logic in `contractor_odes.cc`) can be deleted; CAPD becomes the unconditional ODE contractor. -- The `contractor_odes_codac.cc` 471-line TU was load-bearing only as the "fast path." That role is gone. - -### Implementation checklist (not yet started) - -- [ ] Fork `ibex-team/ibex-lib`; verify ARM64 source build (gaol/ultim, no FILIB). -- [ ] Apply gradient lazy-init patch + ExprLinearity lazy-init patch. -- [ ] Address `std::apply` ADL conflict in Bison-generated parser (macOS + Linux). -- [ ] Switch `ibex_external` in `CMakeLists.txt` from prebuilt-ZIP to `ExternalProject_Add` from our fork. -- [ ] Remove `codac_external` block and `codac-install/` references from `CMakeLists.txt`. -- [ ] Delete `contractor_odes_codac.{h,cc}`; remove Codac includes and link targets. -- [ ] Update `contractor_odes.cc` dispatch to remove the Codac path and gate logic (CAPD is unconditional). -- [ ] Update tests: remove Codac-specific fixtures; confirm CAPD-path semantic tests still pass. -- [ ] Run `/benchmark-baseline`; expect saradc PAR2 average to drop ~3× from 567 s. -- [ ] Update `CLAUDE.md` and this file to reflect the new dependency stack. diff --git a/DEPENDENCIES.md b/DEPENDENCIES.md index bbdba663a..32d5c9be6 100644 --- a/DEPENDENCIES.md +++ b/DEPENDENCIES.md @@ -3,35 +3,41 @@ This document describes the external libraries dReal4 depends on, including the rationale for choosing specific versions and the changes made from upstream. -> **Status (2026-06-08):** Codac is no longer used. IBEX is now source-built -> from the dReal team's fork (`ncsys-lab/ibex-lib@dreal-perf-patches`) and -> CAPD is the sole ODE backend. See `CODAC_MIGRATION.md` for the historical -> context and `../ibex-fork/MIGRATION.md` for the (minimal) patch catalog of -> the IBEX fork. +> **Status:** Codac is no longer used. IBEX is source-built from the dReal +> team's fork (`ncsys-lab/ibex-lib@dreal-perf-patches`) and CAPD is the sole +> ODE backend. See `docs/decisions.md` "ODE backend" for the migration +> rationale and `../ibex-fork/MIGRATION.md` for the IBEX fork's patch catalog. --- ## IBEX (`ncsys-lab/ibex-lib`) -**Version**: branch `dreal-perf-patches` (7 patches on top of mainline `ibex-team/ibex-lib@65ed5877`). +**Version**: `dreal-perf-patches` on top of mainline `ibex-team/ibex-lib`; `CMakeLists.txt` pins the exact fork sha. **Build**: `ExternalProject_Add` source-build from `https://github.com/ncsys-lab/ibex-lib.git` (cache var `IBEX_GIT_REPOSITORY`, overridable to a `file://` path for local-dev iteration against `../ibex-fork`), installed into `gcc_build/ibex-install/`. **Role**: Interval arithmetic + constraint propagation. Provides `IntervalVector`, `Function`, `HC4Revise` (the forward-backward contractor), polytope hull (`CtcPolytopeHull`), and the symbolic expression tree. ### Why a fork at all -The fork hosts seven surgical patches that aren't yet upstream (see `../ibex-fork/MIGRATION.md` for the full catalog): - -1. **`function: lazy-init gradient`** (2 files, ~24 lines). `Function::init` no longer eagerly allocates the `Gradient` object; an inline `lazy_grad()` accessor builds it on first use. Profiling in `CODAC_MIGRATION.md` traced ~65% of `Function::init` wall time to this allocation when dReal never touches the gradient API. -2. **`Function::backward callback`** (4 files, ~16 lines). Adds an optional `std::function` argument to `Function::backward`. dReal's HC4 contractor (`contractor_ibex_fwdbwd.cc`) uses the callback to track narrowed variables without an `IntervalVector` snapshot. -3. **`parser.yc namespace fix`** (2 files, ~6 lines). Qualifies two unqualified `apply(...)` calls in the Bison-generated parser as `ibex::parser::apply(...)`, which avoids ADL ambiguities on modern toolchains (clang-18 + libc++ and GCC 13 + libstdc++). -4. **`mathlib: support aarch64/arm64 Linux`** (1 file, ~8 lines). Mainline mathlib's `CMakeLists.txt` doesn't recognize arm64 Linux as a supported platform; without this, `Dockerfile.dreal_ubuntu` fails to build on Apple Silicon (Docker defaults to native `linux/arm64`). -5. **`function: fire backward callback for non-scalar args`** (2 files, ~100 lines additive). Audit fix for patch #2: the non-scalar branch of `read_arg_domains` previously bypassed the callback for vector/matrix-typed function arguments. SMT theory-lemma generation relies on per-variable change events for soundness; this patch closes the gap via a new callback-aware `load()` overload in `ibex_TemplateDomain.h`. -6. **`function: copy old-value in backward callback to avoid alias`** (1 file, 1 line). Audit fix for patch #2: the scalar branch bound `old_value` as a const reference to a memory cell that the next line overwrote. Callers that retain `old_value` would see stale data. Copy by value. -7. **`HC4Revise: report partial narrowings on EmptyBoxException`** (1 file, ~7 lines). Audit fix for patch #2: when backward propagation throws `EmptyBoxException`, surface any narrowings that completed before the contradiction before calling `set_empty()`. Tightens theory-lemma precision for callers (dReal stays sound either way via its own empty-box handling). - -Total fork diff vs mainline: 9 files, +166/−19 (excluding docs). - -All seven are intended as upstream PRs. Once any/all merge, drop the corresponding commit; when all seven land, swap the `GIT_REPOSITORY` back to `ibex-team/ibex-lib` and delete the fork. +The fork hosts a series of surgical, intended-as-upstream-PR patches that aren't yet in +mainline. The authoritative, per-patch catalog (with file/line counts, soundness gates, and +measured effects) lives in **`../ibex-fork/MIGRATION.md`** — it is the single source of truth for +the patch set and its count; do not restate the list here (it drifts). The categories: + +- **Performance levers (the reason the fork exists):** lazy-init `Gradient` (the dominant + non-ODE cost — ~65% of `Function::init` wall time built an object `Function::backward` never + reads; see `docs/decisions.md` "ODE backend"); inline aarch64 FPCR rounding write + batched + nearest-rounding region in gaol transcendentals (bit-identical, ~8% on transcendental-dense + odeexpr); and replacing `HC4Revise`'s `EmptyBoxException` control flow with a return-status + (`__cxa_throw` off the contraction hot path). +- **Correctness / soundness:** `Function::backward` per-variable callback (lemma quality) plus + its audit fixes for non-scalar args, reference aliasing, and partial-narrowing precision; gaol + `Interval::log`/`pow` soundness gaps; and `underflow_saturate` for subnormal-band HC4 backward + targets (dreal/dreal4#321 — see `docs/decisions.md` "Denormal / underflow soundness"). +- **Platform / build:** Bison-parser `apply(...)` namespace qualification (clang-18/GCC-13 ADL); + mathlib aarch64/arm64-Linux support (Apple-Silicon Docker build). + +Once a patch merges upstream, drop it; when all land, swap `GIT_REPOSITORY` back to +`ibex-team/ibex-lib` and delete the fork. ### Source-build invocation (from `CMakeLists.txt`) @@ -99,6 +105,8 @@ ctest --output-on-failure Brew packages (auto-detected by `find_brew_package` in `CMakeLists.txt`): `bison`, `flex`, `gmp`, `cadical`. +Optional dev-lint tool: `./copy_lint.sh` (the incremental clang-tidy copy gate) needs `brew install llvm` for its `clang-tidy`. It is not a build dependency — `CMAKE_CXX_CLANG_TIDY` stays unset and the build never invokes it. + ### Linux (Ubuntu 24.04 + clang-18) via Docker The `Dockerfile.dreal_ubuntu` is the hermetic Linux test harness. Because the IBEX source-build needs `../ibex-fork` available inside the container, the Docker build context must be the parent of `dreal4-cmake/`: @@ -114,5 +122,5 @@ The container builds CaDiCaL 3.0.0, GMP 6.3.0, Bison 3.8.2, and Flex 2.6.4 from ## Migration History -- `CODAC_MIGRATION.md` — the original migration off `ncsys-lab/ibex-lib` to Codac, the perf-regression analysis that motivated returning to a fork, and the final resolution. -- `../ibex-fork/MIGRATION.md` — divergence catalog of the IBEX fork (7-patch series). +- `docs/decisions.md` "ODE backend" — the Codac→CAPD-only migration rationale, the perf-regression analysis that motivated returning to a fork, and the resolution. +- `../ibex-fork/MIGRATION.md` — divergence catalog of the IBEX fork. diff --git a/Dockerfile.dreal_ubuntu b/Dockerfile.dreal_ubuntu index ad174fbb7..465652c21 100644 --- a/Dockerfile.dreal_ubuntu +++ b/Dockerfile.dreal_ubuntu @@ -71,7 +71,7 @@ RUN rm /usr/local/lib/libgmpxx.so* # BEGIN DREAL BUILD # The IBEX source-build ExternalProject clones from -# https://github.com/ncsys-lab/ibex-lib at the dreal-perf-patches branch +# https://github.com/ncsys-lab/ibex-lib at the pinned dreal-perf-patches sha # (see CMakeLists.txt's IBEX_GIT_REPOSITORY / IBEX_GIT_TAG cache variables). # Override either at `docker build --build-arg` time if pointing at a local # checkout — the default needs only outbound HTTPS from the build sandbox. @@ -81,6 +81,15 @@ RUN rm /usr/local/lib/libgmpxx.so* RUN mkdir /dreal/ COPY src/ /dreal/src COPY test/ /dreal/test +COPY cmake/ /dreal/cmake +# Minimal .git metadata so --version reports the real commit hash. +# HEAD + refs/ is sufficient for `git rev-parse --short HEAD`; the object +# store is not needed. Dirty detection (git status) is always 0 in Docker +# because .git/index and objects/ are not present. +COPY .git/HEAD /dreal/.git/HEAD +COPY .git/refs/ /dreal/.git/refs/ +# git repo validation requires objects/ to exist even when empty. +RUN mkdir -p /dreal/.git/objects/pack /dreal/.git/objects/info COPY CMakeLists.txt /dreal/CMakeLists.txt COPY FULL_BUILD.sh /dreal/FULL_BUILD.sh RUN /dreal/FULL_BUILD.sh diff --git a/HULL_COMPLETENESS.md b/HULL_COMPLETENESS.md new file mode 100644 index 000000000..7a09c9291 --- /dev/null +++ b/HULL_COMPLETENESS.md @@ -0,0 +1,363 @@ +# Hull-grid completeness coupling — a latent looseness in the per-slice ODE tube + +**Soundness vs. completeness:** the failure mode here is **COMPLETENESS** +(missed refutation / false-`delta-sat`), **not** SOUNDNESS (false-`unsat`). The +file's old name (`HULL_SOUNDNESS.md`) mislabeled it, which read as a correctness +emergency and cancelled experiments — the cautionary case behind +`docs/soundness-vs-completeness.md` (the dichotomy + notation discipline). + +**Status: RESOLVED (2026-06) by a centered-in-time range, NOT the width-based +fix this file originally sketched.** The actual root cause is narrower than the +"sub-interval width" framing below: CAPD's `curve(sub)` was already centered on +the initial-condition spread but evaluated the Taylor polynomial in *time* by +naive interval Horner over the whole sub-interval — the time-dependency problem. +Replacing that single evaluation with a mean-value-in-time enclosure +`x(mid) + x'(sub)·(sub−mid)`, intersected with the naive result (so it is never +looser), tightens the whole tube uniformly with **no knob change and no +subdivision**. The F1 interior-violation case now refutes at the **default** +hull-grid; `--ode-hull-grid` is no longer completeness-load-bearing. See +"Resolution" below for the implementation and measured trade-off. The +width-based subdivision (Stage 2) and refine-on-demand (Stage 3) were **not +needed** and were not built. The investigation history below is retained as the +record of *why* hull-grid was a completeness knob and how the fix was scoped. + +## TL;DR + +The per-slice tube enclosures the ODE contractor produces are **far looser than +CAPD's actual precision allows**, because the sub-slicing uses a fixed *count* +(`kHullGrid`) per CAPD step. When CAPD takes a large adaptive step, each +sub-interval is wide, and evaluating the Taylor curve over a wide time-interval +(`curve(sub)`) blows up via the **polynomial dependency problem**. This silently +weakens refutation power — most visibly, **interior invariant-violation +detection** — and couples a *completeness-relevant* (refutation) capability to a +*performance* knob. Lowering `--ode-hull-grid` for speed therefore trades away refutation +completeness, invisibly. The fix is to bound the sub-interval **width**, not its +count. + +## How it surfaced + +The 2026-06 meta-parameter sweep (OPTIMIZATION_LOG.md "2026-06 re-tuning +campaign") found that forward order 12 + hull-grid 4 was ~2× faster on the +123-job ODE corpus with **zero** SAT↔UNSAT flips, and that default was briefly +adopted. The Debug suite then failed exactly one test: + +``` +[ FAILED ] GravityInvariantTest.FwdInteriorInvariantViolation_BoxEmpties +``` + +This is the regression test (`test/dreal/contractor/test/contractor_odes_semantic_test.cc`) +for the cav26 per-slice restoration (commit `5d619fe3f`) — it checks that an +invariant violated **only at a trajectory's interior** (not at either endpoint) +is still detected and refutes. + +**The wrong first instinct** (caught in review) was to bump hull-grid back up +until the test passed (hull-8 passes). That is gaming the verifier: it hides the +defect behind the same fragile coupling instead of fixing it. See the amended +`rules/dont-game-the-verifier.md`. + +## The scenario + +Gravity flow `dx/dt = v, dv/dt = -1`, from a **point** initial condition +`x0 = 0, v0 = 1`, terminal pinned at `t = 2`. The exact trajectory is + +``` +v(t) = 1 - t (exactly linear) +x(t) = t - t²/2 (exactly quadratic; peak x(1) = 0.5) +``` + +Invariant `∀t∈[0,2]. x ≤ 0.3`. It holds at both endpoints (`x(0)=x(2)=0`) and on +the terminal gate box, but is violated at the **interior peak** `x(1)=0.5 > 0.3` +(margin 0.2 — enormous vs the 1e-3 precision). Ground truth: **UNSAT**. A correct +per-slice filter refutes by finding a slice whose `x` enclosure lower bound +exceeds 0.3. + +## The evidence (slice dump at hull-grid 4, order 12) + +Instrumenting the per-slice invariant loop (`contractor_odes.cc`) to print each +slice's time span and state enclosure: + +``` +slice t=[0.0,0.5] x=[0.000000, 0.500000] v=[0.500000, 1.000000] violated=0 +slice t=[0.5,1.0] x=[0.250000, 0.750000] v=[0.000000, 0.500000] violated=0 +slice t=[1.0,1.5] x=[0.250000, 0.750000] v=[-0.500000, 0.000000] violated=0 +slice t=[1.5,2.0] x=[0.000000, 0.500000] v=[-1.000000,-0.500000] violated=0 +``` + +Read this carefully: + +- There are **exactly 4 slices spanning [0,2]** → CAPD integrated the whole + window in **one step of size 2.0** (the dynamics are trivial, so the adaptive + step controller maximized the step), and hull-grid 4 split that one step into 4 + sub-intervals of width **0.5**. +- The **`v` enclosures are exact** (`v(t)=1-t` is linear; e.g. `[0.5,1.0]` over + `t∈[0,0.5]` is the true range). +- The **`x` enclosures are ~4× too wide.** Over `t∈[0.5,1.0]` the TRUE range of + `x` is `[x(0.5), x(1)] = [0.375, 0.500]` (x is monotone up to the peak), but + the enclosure is **`[0.25, 0.75]`** — width 0.5 vs true 0.125. Its lower bound + 0.25 < 0.3, so the violation at the peak is **missed** on every slice. + +`x(t)=t-t²/2` is an exact degree-2 polynomial and the IC is a point, so an +order-12 (let alone order-20) Taylor method has ~zero remainder — the *true* +enclosure should be essentially `[0.375, 0.500]`. The 4× blow-up is not a +fundamental interval-arithmetic limit; it is the **dependency problem** in +evaluating the Taylor curve over a wide time sub-interval. + +At hull-grid 16 the same step is cut into width-0.125 sub-intervals; `curve(sub)` +over a narrow interval is tight enough that the near-peak slice has lb > 0.3, and +the test passes. **It passes by luck of the step size, not by design.** + +## Root cause + +``` +sub_interval_width = (CAPD adaptive step size) / kHullGrid ← fixed COUNT +enclosure looseness ≈ O(sub_interval_width²) (polynomial dependency) +``` + +`kHullGrid` is a fixed **count per step**, so the sub-interval width — and hence +the per-slice enclosure tightness — is at the mercy of CAPD's adaptive step +controller. A trivial flow that admits a huge step gets wide sub-intervals and +loose enclosures. The per-slice invariant check refutes only when some slice's +`x`-enclosure lower bound clears the constraint, so its **refutation power is +coupled to `(step_size / hull_count)`** — a quantity no one is bounding. + +## Why this is a real problem (not just this test) + +1. **Interior-invariant detection silently weakens** when steps are large — the + F1 test is one instance; production flows with large steps over a sharp + interior excursion could be under-refuted at hull-16 too. +2. **The whole tube is looser than CAPD's precision**, so terminal-gate + intersection and time-narrowing are weaker than they should be **corpus-wide**. + The sweep's "speedups with zero flips" were partly measuring *less of an + already-too-loose computation* — i.e. the baseline itself is leaving precision + (and possibly solve-power) on the table. +3. It makes `--ode-hull-grid` a **completeness-relevant knob (refutation power) + disguised as a performance knob.** Lowering it for speed quietly buys missed + refutations (false-`delta-sat`), never false-`unsat`. + +### Completeness classification (the precise model-theory) + +This is a **COMPLETENESS** failure, **not** SOUNDNESS — and writing the +T-relations out (the discipline `CLAUDE.md` mandates) makes that unmissable: + +> **COMPLETENESS** (returns `delta-sat` / asserts φ^δ is *T-satisfiable* on a +> *T-unsatisfiable* φ — a missed refutation). It is **not** SOUNDNESS: lowering +> hull-grid only makes each sub-slice enclosure *wider* (still a sound outward +> over-approximation), so it can never wrongly refute a feasible instance — there +> is no path to a false-`unsat` (which would be asserting φ *T-unsatisfiable* on a +> *T-satisfiable* φ). + +The per-slice filter's *entire purpose* is this refutation, and a violation with +margin 0.2 ≫ δ should never be missed — so the F1 regression is a first-class +**completeness gate**, even though it is not a soundness hole. Filing it as "HULL +SOUNDNESS" was the mislabel that read as a correctness emergency and cancelled +experiments; see `docs/soundness-vs-completeness.md`. + +## Resolution (2026-06) — centered-in-time mean-value range + +The fix that shipped is **not** the width-based subdivision sketched below. While +scoping that fix, reading CAPD's `Curve::operator()` (`diffAlgebra/Curve.hpp:59`) +showed the dependency blow-up is purely in the **time** argument: the doubleton +form already cancels the initial-condition spread (`xx ∩ (phi + jacPhi·deltaX)`), +but the polynomial in time is summed by naive interval Horner +(`xx[d] = xx[d]*h + coeff`) over the *whole* wide sub-interval `h`. CAPD also +exposes `timeDerivative(h)` (Curve.hpp:178), so a mean-value-in-time bound is +computable from the existing API: + +``` +mid = scalar midpoint of sub +enclosure = curve(point(mid)) + timeDerivative(sub) · (sub − mid) // mean-value +result = enclosure ∩ curve(sub) // never looser +``` + +`curve(point(mid))` is a thin-time evaluation (no time-widening); the correction +term is derivative-bounded and `O(r²)` in the sub radius. Both forms are sound +outward enclosures, so their intersection still encloses the true trajectory — +and intersecting with the naive result guarantees the tube is **never looser** +than before, hence **no soundness risk and no completeness loss on any flow** +(narrow-sub stiff flows where naive was already tight just keep the naive bound). +Implemented as `centered_curve_range()` in `contractor_odes_capd.cc`, applied to +both the tube `state` and the window-clipped `gate_state`. + +**Why this beats the width-based sketch:** it tightens the *same* computation +instead of adding sub-slices, so it has no `h_max` scaling question, no knob type +change, and no extra cost on the small-step flows that width-based would have +left untouched while still paying its branch. It is the subtract-before-add +option the file's "Open questions" gestured at ("does `curve` have a tighter +range mode"). + +### Measured outcome + +- **Completeness:** `GravityInvariantTest.FwdInteriorInvariantViolation_DefaultHull_BoxEmpties` + (new test, default hull-grid, no pin) failed pre-fix (missed refutation) and + passes post-fix. The pinned-16 mechanism test and the no-invariant SAT control + still pass; full unit suite 643/643. +- **No correctness flips** in any benchmark sample (provably impossible — the + tube only tightens). +- **Performance is mixed and net-positive**, matching the "depends on the corpus + step-size distribution" prediction: + - github (UNSAT-via-ODE-refutation, same-instance vs frozen baseline): ~0.19× + PAR2 — tighter tube refutes faster. tacas: ~0.60×. + - saradc (same-instance A/B, old vs new binary): **+~14% CPU**, identical + `unsat` verdicts on the two instances that decide; the one apparent + "timeout regression" (`k90_4b_box`) times out on the **old** binary too + (pre-existing hard instance — the family-aggregate 4.2× was a sampling + artifact: `--family saradc` drew harder k84/k90 instances than the baseline's + k20–k70 pool). + - odeexpr is NRA (no ODE), code path untouched → neutral. +- **Owner's-call lever (not taken):** the ~14% saradc cost is the extra + curve/timeDerivative evaluations on flows where the mean-value form doesn't pay + off (already-tight narrow sub-intervals). It could be clawed back by computing + the mean-value form only when the sub-interval is wide, at the cost of one + branch — deliberately *not* added (minimize-logic; the cost is modest and the + clean uniform path is preferred unless the owner says otherwise). + +--- + +## Proposed fix — SPECULATIVE (design sketch, NOT validated) — SUPERSEDED, see "Resolution" above + +> ⚠️ **Treat this entire section as a hypothesis, not a spec.** It is reasoned +> from a *single* gravity slice-dump (one trivial flow) plus the standard +> interval-overestimation scaling argument — it has **not** been prototyped, +> measured, or checked against CAPD's actual `curve` internals. Any of it can be +> wrong in practice: the cost predictions, the `O(r²)` scaling, even "width +> subdivision is the right lever." **If you implement this and the measurements +> disagree, trust the measurements and rewrite this section — do not bend the +> code to match the sketch** (that would be the exact verifier-gaming trap that +> produced this file; see `dont-game-the-verifier.md`). Re-derive the mechanism +> on 2–3 *different* flows (not just gravity) before committing to a direction. + +### Why the enclosure blows up (the hypothesised mechanism) + +`curve(sub)` evaluates the step's Taylor polynomial (with interval coefficients) +over a time sub-interval. Over a **wide** sub-interval this loses variable +correlation — the interval **dependency problem**. For gravity `x(s)=s−s²/2` +over `s∈[0.5,1.0]` (true range `[0.375,0.5]`, width 0.125): + +- naive monomial interval eval: `s − s²/2 = [0.5,1] − [0.125,0.5] = [0.0,0.875]` + — 7× too wide, because the two occurrences of `s` are treated as independent; +- CAPD's *actual* dump enclosure was `[0.25,0.75]` — 4× too wide: better than + naive (so CAPD uses some centered/doubleton form), but still loses correlation + over a width-0.5 interval. + +A degree-2 interval extension over-estimates by `O(r²)` in the sub-interval +radius `r`, so **narrowing the sub-interval shrinks the slop quadratically**: +hull-16's sub-width 0.125 is 4× narrower than hull-4's 0.5, hence ~16× tighter — +which is why hull-16 clears `lb > 0.3` and hull-4 does not. *(This `O(r²)` claim +is the textbook interval-extension argument applied to this polynomial; the exact +CAPD `curve` representation is **unverified** — confirm before relying on it.)* + +### The change (bound the width, not the count) + +`integrate_tube_slices_impl` (contractor_odes_capd.cc) currently splits each CAPD +step into a fixed COUNT `params.hull_grid`: + +```cpp +const double dd = (d_hi - d_lo) / kHullGrid; // sub-width = step / count +for (int k = 0; k < kHullGrid; ++k) { ... curve(sub) ... } +``` + +so the sub-width = `step_size / hull_grid` floats with the adaptive step size. +The sketch: bound the sub-width by a constant `h_max` instead — + +```cpp +const int n_sub = std::max(1, (int)std::ceil(step_size / h_max)); +const double dd = step_size / n_sub; // sub-width <= h_max always +``` + +so `curve(sub)` is always evaluated over a narrow interval regardless of the +controller. This is a **type change of the knob**: `Config::ode_hull_grid` +int→double, `CapdSolverParams::hull_grid` int→double, the `--ode-hull-grid` flag +a positive double (consider renaming to `--ode-hull-width`). The trace path +(`run_capd_trace_impl`, used only by `--visualize`) carries its own fixed +`n_steps` — lower priority, but give it the same treatment or document it as +deliberately count-based. + +### The catch — this is in DIRECT TENSION with the adopted speedup + +Part of the ~2× from hull-4 is simply doing **fewer** sub-slice evaluations per +step. The looseness only bites flows that take **large** adaptive steps +(trivial/non-stiff dynamics — gravity took ONE step of size 2.0); many-small-step +(stiff) flows already get narrow sub-intervals at any count. Width-based +subdivision **adds** sub-slices precisely on the large-step flows to reach +adequate resolution — i.e. it **claws back speed exactly where hull-4 won it**, +while leaving small-step flows ~unchanged. So the fix is **not free**: net speed +depends on the corpus step-size distribution and MUST be re-measured (full OFAT + +123). Plausible outcome: the corrected tube lands somewhere *between* the old +order-20/hull-16 and the current order-12/hull-4 on speed. + +### Alternatives considered + +- **Refine-on-demand for the invariant check ONLY** — keep the fast coarse tube + for terminal narrowing, but when a slice's enclosure *straddles* an invariant + boundary (`lb ≤ threshold ≤ ub`), subdivide just that slice (re-evaluate + `curve` on halves) until it resolves or hits a floor. **Now arguably the + preferred direction:** the owner already *accepted* the looser terminal tube + (the completeness/speed tradeoff is fine), so the only thing worth restoring is + detection robustness — and this does it **without** re-adding cost to the + terminal path the width-based fix would slow. Narrower blast radius, keeps the + speedup. Downside: a second code path for the invariant check. +- **Cap CAPD's step (`--ode-max-step`)** — a band-aid: fights the adaptive + controller globally, hurt performance in the OFAT, and doesn't fix `curve` + looseness within whatever step remains. +- **A tighter CAPD range API** — if `curve`/the doubleton offers a non-naive + range bound (centered form, monotonicity test), that could cut the needed + subdivision. Worth a look, but subdivision is robust to whatever `curve` does. + +## Current state / decision + +After the soundness-vs-completeness distinction was clarified (this is a +**completeness** tradeoff — missed refutation / false-`delta-sat` — never a +false-`unsat`), the owner **accepted the tradeoff** and the faster default was +**adopted**: + +- **Default = forward order 12 / backward order 12 / hull-grid 4** (123-confirm: + ~2× faster, PAR2 0.49, +4 solved, zero SAT↔UNSAT flips; bwd-12 adds ~5% over + bwd-20). `config.h` carries the soundness/completeness note + a pointer to this file. +- The F1 regression test (`GravityInvariantTest.FwdInteriorInvariantViolation`) + is **pinned to hull-grid 16** so it still guards the per-slice *mechanism* + (interior violations ARE refuted at adequate resolution); it intentionally + does **not** assert the hull-4 default catches this sub-resolution sharp case — + the accepted completeness limit, documented here (the owner chose not to add a + separate limitation test). +- All Phase-1 runtime-flag plumbing stays; the `--ode-*` flags let any workload + override (e.g. order 16–20 + hull 16 for refutation-critical / sharp-invariant + problems). + +**The looseness defect itself is still open** (independent of the accepted +tradeoff): the tube is ~4× looser than CAPD's precision allows. The width-based +sub-slicing fix below remains the proper next step — it would recover the lost +refutation precision (and likely tighten narrowing corpus-wide) **while keeping +the speed**, after which the default would detect the F1 case too and hull-grid +would stop being completeness-relevant. Tracked as a follow-up. + +## Reproduce + +```bash +# hull-4 is now the DEFAULT, but the F1 test pins hull-16 internally so it passes. +# To SEE the sub-resolution miss, drop the `set_from_command_line(16)` hull pin in +# the FwdInteriorInvariantViolation test (so it uses the hull-4 default), rebuild: +cmake --build gcc_build --target dreal4_cmake_test -j8 +gcc_build/dreal4_cmake_test --gtest_filter='GravityInvariantTest.*' # interior-violation test then fails to empty at hull 4, passes at >= 8 +# slice dump: re-add the DREAL_DEBUG_INV fprintf in the invariant loop of +# contractor_odes.cc (removed after this investigation) and re-run. +``` + +## Open questions for the fix (resolve these BEFORE committing to a direction) + +- **Width-based vs refine-on-demand** — which to build? Given the owner accepted + the looser terminal tube, refine-on-demand (detection-only) may keep the + speedup that width-based would partly spend. Decide based on whether anything + *other than* interior-detection actually needs the tighter tube (does the loose + terminal tube measurably cost solves on the 123?). +- **Confirm the mechanism on ≥2 non-gravity flows.** The `O(r²)` / dependency + story is from one trivial polynomial flow; verify a stiff and a transcendental + flow behave the same before trusting the scaling. +- **`h_max` units/scaling.** Absolute time, or relative to the step, or to + `t_ub`? Horizons span ~1 to ~20+ across the corpus, so a single absolute + constant may over-resolve short flows and under-resolve long ones. +- **Does `capd::...Curve::operator()` have a tighter-than-naive range mode** that + would reduce (or remove) the needed subdivision? +- **Re-measure cost vs speed.** Width-based adds work on large-step flows — run + the full OFAT + 123 on the corrected tube; the tighter tube may shift every + knob's effect and could itself change solve counts. Do NOT re-pick a default + from the loose-tube numbers in this campaign. diff --git a/OPTIMIZATION_LOG.md b/OPTIMIZATION_LOG.md index 373c1aae1..fd7959964 100644 --- a/OPTIMIZATION_LOG.md +++ b/OPTIMIZATION_LOG.md @@ -5,6 +5,160 @@ or **Rejected** (with numbers + reason). Acceptance bar: net PAR2 improvement probe + gate sets, **zero** SAT/UNSAT correctness flips vs ground truth, no >1.5× regressions. Soundness guardrails (FE_UPWARD/FE_TONEAREST guards, no silent fallbacks) are non-negotiable. +> **Scope:** §Adopted and §Rejected below are **all CAPD/ODE-path tuning** — the probe set +> is ODE-heavy and the baseline profile is an ODE benchmark where `contractor_ode_lohner` +> is 90.8% of runtime. The ODE-free `ode_expressivity` (odeexpr) family shares **none** of +> this code; for its assumption re-check and its (different) hotspot, see the +> **odeexpr** section at the bottom of this file. + +## 2026-06 re-tuning campaign — runtime knobs + pooled sweep (IN PROGRESS) + +The ODE contractor's performance regime **changed** under the soundness fixes on +`rounding-mode-fixes` (per-slice tube filter restored `5d619fe3f`; full-precision +vector-field feed `a925eba2c`; terminal-gate window clip `a60b0ff8e`). Those fixes were +measured against the *old* coarse-endpoint contractor, so the **§Adopted / §Rejected +numbers below are superseded** for the current architecture and are being re-measured by +this campaign. (They remain as the historical record of what was tried and why.) + +### What changed in the code + +The CAPD knobs are no longer compile-time `constexpr` in `contractor_odes_capd.cc`; they +are **runtime CLI flags** threaded through a `CapdSolverParams` struct (`ode_types.h`), +resolved per contractor instance from `Config` (`contractor_odes.cc` ctor, direction-aware +for the Taylor order): + +| Flag | Default (= old constexpr) | Knob | +|---|---|---| +| `--ode-taylor-order` | 20 | forward CAPD `IOdeSolver` Taylor order | +| `--ode-backward-order` | 20 | backward (`-f(x)`) Taylor order (a lohner instance is single-direction) | +| `--ode-abs-tol` / `--ode-rel-tol` | 1e-10 | CAPD step-control tolerances | +| `--ode-hull-grid` | 16 | per-step tube sub-slices in the filter | +| `--ode-c0-set` | `rect2` | enclosure set: `rect2`/`tripleton`/`horect2` (runtime type-dispatch) | +| `--ode-backward` | `true` | enable the backward (X₀-narrowing) contractor (emit-guard in `theory_solver.cc`) | +| `--ode-max-step` | 0 (adaptive) | optional `setMaxStep` cap | + +Defaults equal the prior constexprs, so default behavior is unchanged — **proven** by a +123-job A/B (`/tmp/dreal4_head` HEAD vs worktree@default): identical solve-set (117/123), +zero SAT/UNSAT disagreements, CPU within noise (aggregate 0.99×). The order-20 rationale +moved onto the `kDefaultOde*` constants in `solver/config.h`. + +### Experimental design for a meta-parameter sweep + +Screen wide and cheap, then confirm narrow and clean: + +1. **OFAT on the probe set** (`benchmark/probe_odes.tsv`, 18 ODE-heavy: tacas inverters + + github prostate/thermostat/quad/cardiac/water + saradc box/nonlinear; mix of fast k2 and + stress k256+). Vary **one knob at a time** around the default; `base` is one of the + configs. Screens main-effect *direction* and flags any verdict change. +2. **Targeted 2-factor sweeps** only for the architecturally-coupled pairs — **order × + hull-grid** (per-slice cost ≈ hull_grid × #steps, and #steps falls with order) and + **order × c0-set**. Probe set only. +3. **Confirm** the best 1–3 configs on the **full 123 ODE-family** via the sequential + `do_ab.sh` (cleaner timing than the pool) before any recommendation. + +**Metric & guardrails.** CPU time (user+sys) **ratio vs `base`** is the screen — within one +pooled sweep, `base` and every variant are shuffled together so they share the same average +contention, making the *ratio* fair even though absolute CPU shifts ~10–17% vs an isolated +run (memory-bandwidth contention). A **SAT↔UNSAT change vs base is the soundness signal**: a +coarser enclosure (lower order / fewer slices / looser tol / backward-off) can only +*fail-to-refute* → a `base`-UNSAT turning delta-sat means base was the tighter/sounder answer; +investigate against the cav26 oracle, never silently accept. The probe screens **large** +effects reliably; sub-contention-noise effects need the confirmation run. + +### Pooled sweep harness (`benchmark/do_sweep.sh`) + +`do_sweep.sh NAME1="flags1" NAME2="flags2" …` sweeps **one** binary over many flag configs on +the same jobs and emits a `compare_solvers.py` table (N columns). Key behavior: + +- **Pooled, not per-config batches.** All (config × benchmark) pairs run in **one shuffled + 12-way pool**, not 20 separate 18-job batches. *Why:* an 18-job probe drains to its 2–3 + long-poles (e.g. a k256 thermostat) while the other ~9 cores idle — across 20 configs that + idle tail wastes most of the wall time. Pooling overlaps a slow config's long-pole with + other configs' fast jobs, so the cores stay full (≈2.2 hr → ≈40 min for the 20×18 OFAT). + It does **not** oversubscribe: ≤`MAXJOBS` solvers run at once, each `nice -n 1` on its own + core, so per-process CPU-time stays accurate — same per-core fairness as `run_batch`'s 12-way, + just better packed. The shuffle spreads long-poles so the only thin tail is the last ~12 jobs. +- **Env:** `JOBS` (default `probe_odes.tsv`; point at `select.py --family … --all` for the + full-corpus confirm), `DREAL_BINARY`, `MAXJOBS` (default **12** — the project standard), + `TIMEOUT` (default 600; the OFAT probe uses a tighter cap, e.g. 400, to bound stress-TIM cost + while the 123-job confirm keeps 600). Per-config flags ride a bash array-free TSV column with + an empty-flags `NONE` sentinel (bash 3.2 on macOS has no assoc arrays, and an empty TSV field + is collapsed by tab-IFS `read`). +- **Enablers** (in `run_batch.sh`): `DREAL_ARGS` injects per-invocation solver flags; `TIMEOUT` + overrides the 600 s cap. Both default to the prior behavior. +- **Usage:** + ```bash + # OFAT probe (one knob), tighter cap: + JOBS=benchmark/probe_odes.tsv TIMEOUT=400 bash benchmark/do_sweep.sh \ + "base=" "ord12=--ode-taylor-order 12" "bwoff=--ode-backward false" + # Full-corpus confirm of a winner (sequential do_ab is cleaner for final numbers): + bash benchmark/do_ab.sh /path/to/binA gcc_build/dreal4 + ``` + +### Lessons learned + +- **Pooling > per-config batching** for a sweep with skewed per-job runtimes (above). +- **Count solvers with `pgrep -x dreal4`, not `pgrep -f gcc_build/dreal4`** — the `-f` form also + matches the `gtime`/`nice`/`timeout` wrapper procs (≈3 per solve), so 12 real solves read as + ~39 and look like a broken throttle. The `while (( $(jobs -r | wc -l) >= MAX ))` throttle is + correct (same pattern as `folderops/unroll_folder.sh`); cap is **12**. +- **A timing-sensitive run needs a quiet machine** — a background CLion `-j14` auto-build (it + rebuilds on file save) silently inflates wall time and risks false 600 s TIMs; quit it before + the A/B / sweep. Builds and ctest (correctness, not timing) can overlap; baselines/A-Bs cannot. +- **A cleanup wiped local-only benchmark artifacts** (`baseline.csv`, `baseline_local.csv`, + `baseline_odeexpr.csv`, `state.json`, `probe_odes.tsv` — all untracked) and `do_baseline.sh` + dies if `state.json` is absent (`set_local_baseline.py` reads it). Reconstructible: + `baseline.csv` ← `/tmp/good_benchmarks.csv` (same schema, documented superset); seed an empty + `{"anomalies":[],"exceptional":[]}` `state.json`. +- **A benchmark "zero verdict flips" does NOT clear a correctness-class (soundness *or* + completeness) change** — the sweep's lower order/hull-grid flipped no verdict on 141 + benchmarks, yet a curated unit test (`GravityInvariantTest`) caught that hull-grid 4 silently + breaks interior-invariant refutation — a *completeness* gate (asserts φ^δ T-satisfiable on a + T-unsatisfiable φ — missed refutation), not soundness. Curated refutation/completeness tests + exercise sharp cases a benchmark corpus can't. And the + reflex to "bump hull-grid back up until the test passes" is gaming the verifier — the test was + exposing a real looseness defect. **Root cause + the deferred fix: `HULL_COMPLETENESS.md`.** + +### Per-knob findings (measured on the current — still ~4× loose — tube) + +These drove the adopted default (order 12 / hull-grid 4 / backward 12); numbers reflect the +SHIPPED tube, which `HULL_COMPLETENESS.md` shows is ~4× looser than CAPD's precision and will +tighten once the width-based sub-slicing fix lands (re-tune then). Soundness direction: lower +order/hull only *widens* enclosures (no false-`unsat`); the cost is missed refutation +(completeness), which the F1 test catches for the sharp interior case below the hull-4 resolution. + +- **Taylor order is problem-dependent** (the strongest reason it stays a flag): tacas inverters + want low (~8–12, up to ~2.5× faster); stiff long-horizon github wants high (~16–20). Order 16 + was the best global compromise; order 10 *regressed* github. +- **hull-grid is NOT a free speed knob** — it is the time-resolution of interior-invariant + detection (see `HULL_COMPLETENESS.md`). Lowering it looked like a universal win on benchmarks but + trades away refutation completeness. +- **backward-order / tolerance / c0-set**: minor (±5%). `c0-set=horect2` slightly slower + (matches the old §Rejected). Tolerance is a *minor* lever — the earlier smoke-test "looser tol + is 2.4× slower" was contention noise; the clean OFAT vindicates the old "tolerance ≈ no effect". +- **max-step cap**: harmful (slower + lost the stress benchmark). Keep adaptive (0). +- **backward off**: ~2× faster but loses X₀-narrowing (completeness risk) — a per-workload flag, + never a default. + +### Campaign status (2026-06-23) + +- Phase 0 re-baseline ✓; Phase 1 runtime-flag plumbing ✓ + gates; Phase 2 behavior-neutral A/B ✓. +- Phase 3 sweep ✓ (OFAT 20 configs + order×hull-grid interactions + 123-confirm). +- Phase 4: default **ADOPTED** at forward & backward order 12 + hull-grid 4. The F1 + "soundness" test failure was diagnosed (not gamed) as a *completeness* gate — missed + refutation / false-`delta-sat`, never false-`unsat` — an owner-accepted tradeoff + (`HULL_COMPLETENESS.md`). 123-confirm: ~2× faster (PAR2 0.49), +4 solved (121/123), zero flips; + bwd-12 adds ~5% over bwd-20. F1 test pinned to hull-16 (guards the mechanism at adequate + resolution). Suite green (641/641 modulo the Timer flaky); Debug rounding gate ✓. +- **Follow-up RESOLVED (2026-06):** the ~4× looseness was fixed — but by a **centered-in-time + (mean-value) range**, not the width-based sub-slicing originally proposed (the real cause was + naive Horner in the *time* argument, not sub-interval count; see `HULL_COMPLETENESS.md` + "Resolution"). hull-grid is no longer completeness-relevant and the F1 case now refutes at the + hull-4 default. Same-instance trade-off: github/tacas faster (~0.19×/0.60× PAR2), saradc ~+14% + CPU, no correctness flips. The per-knob numbers above were measured on the OLD loose tube; a + full OFAT/123 re-tune on the tightened tube is the remaining optional step before re-picking + any default. + ## Measurement setup - **Baseline:** `benchmark/baseline_local.csv` (~30 stratified, refreshed on this branch). @@ -31,89 +185,48 @@ Soundness guardrails (FE_UPWARD/FE_TONEAREST guards, no silent fallbacks) are no | `contractor_ode_lohner::Prune` | **90.8%** | the ODE contractor is the bottleneck | | `run_capd_fwd` | 85.4% | forward CAPD integration (BWD contractor is the small remainder) | | `OdeSolver::encloseC0Map` | 84.5% | | -| `computeTaylorCoefficients` (order 20) | **74.2%** | **primary target** — scales with Taylor order | +| `computeTaylorCoefficients` (order 20) | **74.2%** | scales with Taylor order | | `autodiff::Div::eval` | ~17% | vector-field division AD (inverter sigmoid has `/`) | | `DoubleRounding::roundUp/roundDown` (leaves) | ~9.3% | per-op FPU-mode switches (CAPD NATIVE intervals) | | `capd::intervals::operator*` (leaves) | ~6.9% | interval multiplies | -Takeaway: CAPD forward Taylor integration dominates nonlinear-ODE runtime. Highest-value levers -(profiling-justified): **lower Taylor order**, **looser tolerance** (fewer steps), and reducing -the AD operation count. Set type is already `C0Rect2Set` (doubleton + QR reorganization). - -## Backlog (ordered; profiling-justified first) - -1. Centralize the 3 duplicated CAPD config sites into one helper (refactor; behavior-identical). — prerequisite -2. Lower Taylor order 20 → {16,14,12,10} (sweep). Targets the 74% hotspot directly. -3. Looser tolerance 1e-10 → {1e-9,1e-8,1e-7}. Fewer steps. -4. Joint order×tolerance sweep. -5. Adaptive `n_steps` clamp `[20,60]` / factor `2.0` retune. -6. Set representations: `C0Rect2RSet` / `C0HORect2Set` / tripleton (tightness vs cost). -7. `SolutionCurve` reuse; warm-start step size across ICP iterations. -8. C1/variational backward narrowing (interesting, higher effort). -9. Allocation reduction in `with_params` IMap deep-copy per Prune. +Takeaway: CAPD forward Taylor integration dominates nonlinear-ODE runtime. Set type is already +`C0Rect2Set` (doubleton + QR reorganization). --- -## Open approaches (not yet attempted) - -### Vector-field simplification / CSE before to_capd_string - -The forward integration is ~69% of order-10 runtime, dominated by -`computeODECoefficients` — CAPD's automatic differentiation of the ODE RHS, with -`autodiff::Div` (division AD) alone ~17%. CAPD's parser does common-subexpression -elimination *within* one IMap string but does not factorize. The ODE RHS for the -inverter/cardiac models has large repeated transcendental subterms (the same -`log(... exp ...)` block appears across multiple `d/dt`). Pre-simplifying / CSE-ing -the RHS with Drake's symbolic layer before emitting `to_capd_string` could cut the -per-step AD cost at its root. Medium-high effort, **low confidence**: -- The `a / c → a * (1/c)` constant-denominator rewrite is **N/A** for the probe - families — their divisions are state-dependent (prostate `(/ z (+ z 2))`, the - inverter's 60 divisions are sigmoid terms), so the expensive division AD is - inherent, not a constant-fold artifact. -- Subexpression dedup: CAPD's parser already does within-string CSE, so a - Drake-level CSE pass may add little. Would need to confirm CAPD isn't already - capturing the repeated `log(...exp...)` blocks before investing. - -This is the last untried CAPD-side idea and it is speculative; the high-confidence -config/allocation wins are all harvested. - ## Adopted -### 1. Taylor order 20 → 10 (commit pending) - -Lower the CAPD `IOdeSolver` Taylor order from 20 to 10 (`kCapdTaylorOrder`). -Directly attacks the 74% `computeTaylorCoefficients` hotspot — fewer Taylor -coefficients per step on the expensive transcendental/division vector fields. - -**Sweep (fast sub-probe, 16 benchmarks, vs order-20 frozen probe_baseline):** - -| order | net PAR2 | flips | notes | -|---|---|---|---| -| 14 | 0.671 (32.9% faster) | 0 | tacas inverters ~1.85× | -| **10** | **0.517 (48.3% faster)** | **0** | tacas inverters ~3× (0.31–0.33×) | -| 8 | 0.446 (55.4%) | **1** | rejected — prostate SAT→UNSAT | - -**Validation at order 10:** -- Full probe (18, incl. 2 TIMs): net 0.859 (14.1% faster), 0 flips, 0 real - regressions. The 2 TIMs (`quad2-1`, `k13_inverter`) stay TIM — they're ICP/ - SAT-search bound, not CAPD-per-step bound, so order doesn't rescue them. -- 30-set gate: **0 correctness flips**, 7 exceptional. One >1.5× "regression" - (`car-3-single-linear` 267s→TIM) was **parallel-scheduling contention, not an - order effect**: isolated, car-3 solves delta-sat in **184s** at order 10 - (well under the 300s timeout). car-3 is a near-timeout linear benchmark whose - parallel PAR2 is noise-dominated. -- ctest green except the documented flaky trio. - -Soundness: a lower-order Taylor enclosure is wider but still a rigorous -superset — sound, never a false-UNSAT. The order-8 prostate flip is the -delta-sat/unsat boundary ambiguity (different orders give different enclosure -*shapes*); order 10 keeps prostate SAT consistently across orders 10/14/20. - -Current best = order 10. Subsequent experiments measure vs the order-20 frozen -probe_baseline, so their net ratio reflects cumulative gain; compare against -0.859 (full) / 0.517 (fast) to detect incremental regressions. - -### 2. thread_local reuse of the parameter-bound IMap (commit pending) +> **Note (2026-06):** the numbers in §Adopted and §Rejected were measured against the +> *pre-per-slice* coarse-endpoint contractor and are **superseded** — they are being +> re-measured by the "2026-06 re-tuning campaign" section above. Kept as the historical +> record of what was tried and the reasoning. + +### 1. CAPD Taylor order = 20 (order-10 was adopted, then reversed) + +`kCapdTaylorOrder = 20`. An earlier entry lowered the order 20→10 for a 48% fast-probe win, but +that was measured against the **coarse endpoint-narrowing** ODE contractor — which was also +**unsound** (its `run_capd_fwd` intersected the terminal box with only `enclosure(t_ub)`, false- +`unsat`'ing free-time integrals whose solution lands at an interior time `< t_ub`; **proven** on +`github_oct5_0hz_k2_prostate_cancer_*`: coarse → `unsat` 0.03 s, while cav26 and the restored +per-slice form → `delta-sat` with a witness at interior times ≈1.7–4.4 « horizon 20). See +`docs/decisions.md` "Per-slice ODE tube". + +Restoring cav26's per-slice tube filter (sub-grids `kHullGrid=16` enclosures **per step**) fixes +the soundness bug at a cost: the cost model goes from ∝ #steps to ∝ 16 × #steps, so a low +order's many small steps **explode** the slice count. Order-20 is cav26's co-designed partner: +fewer, larger steps + tighter per-step enclosures that also localize interior invariant +violations. The k256 thermostat went 187 s → timeout at order 10, back to 196 s at order 20. +Per-slice verdicts match cav26; on the proven case this build is faster (68 s vs 209 s, both +`delta-sat`). A lower-order enclosure is always a sound superset (never a false-`unsat`), so +order is a speed/precision lever only. The order-10-era sweep tables are superseded. + +*Caveat on attribution:* the per-slice change is **orthogonal** to the +`..._inverter_sigmoid_UNS` UNSAT↔delta-sat flip — that is the #321 ibex-backward +`underflow_saturate` tradeoff (`docs/decisions.md`; do not re-investigate); do not credit/blame +the ODE contractor for it. + +### 2. thread_local reuse of the parameter-bound IMap `with_params` deep-copied the cached IMap (the full automatic-differentiation tree) on every fwd/bwd/trace call to bind parameters without mutating the @@ -126,12 +239,7 @@ Strictly safe / behavior-identical: `setParameter` fully overwrites the named parameters, the cached base maps are immutable and live for the whole process, and thread_local storage means no copy is shared across parallel ICP workers (works for IcpSeq and IcpParallel). No verdict can change — it only removes an -allocation. - -- Fast sub-probe: net 0.499 vs order-10's 0.517 (~3.5% faster), 0 flips. -- Full probe: net 0.847 vs order-10's 0.859 (15.3% cumulative vs order-20), 0 - flips, 0 regressions, TIMs unchanged. -- ctest green except the flaky trio. +allocation. Fast sub-probe ~3.5% faster, 0 flips; ctest green except the flaky trio. ## Rejected @@ -168,15 +276,6 @@ cost, same mechanism) not tested — same prediction. Kept C0Rect2Set. The `CapdC0Set` type alias was added to centralize this knob for the A/B test and is retained (mirrors the order/tolerance centralization). -### Re-profile at order 10 (guides remaining work) - -After order 10, the k22 heavy path shifted: contractor_ode_lohner::Prune 79% -(was 91%), run_capd_fwd 69% (was 85%), backward contractor + Prune overhead -~10% (was ~5%), non-ODE (ibex arithmetic HC4 + fixpoint) ~21% (was ~9%). The -forward Taylor cost is at the order-10 floor and irreducible by config. The -two grown shares — the **backward contractor** (a second full CAPD integration -per ODE constraint) and **non-ODE arithmetic** — are the remaining targets. - ### Backward ODE contractor — no safe focused win (cav26 X_0 narrowing kept) The backward contractor (a one-shot `-f(x)` image narrowing X_0, one per ODE @@ -212,8 +311,7 @@ forward solution curve). vs the order-20 baseline — a correctness flip (halt). The flip is the inherent delta-boundary ambiguity rather than a soundness bug (the enclosure stays a valid superset at any order), but any verdict change vs baseline is -disqualifying. The order knee is between 8 and 10; order 10 is the floor with -zero flips. Not retested below 8. +disqualifying. The order knee is between 8 and 10. Not retested below 8. ### CAPD tolerance 1e-10 → 1e-8 (at order 10) @@ -226,7 +324,184 @@ these benchmarks. `run_capd_fwd`/`run_capd_bwd` compute `n_steps`/`max_step` tolerance-based adaptive control, and for these short/smooth horizons the step count is already near-minimal, so loosening tolerance can't reduce it further. Both the tolerance and n_steps levers are therefore closed for fwd/bwd; the -per-step Taylor-coefficient cost (order) is the only step-cost lever, and it's -at the order-10 floor. Kept tol 1e-10 (tighter = safer, no speed cost). -Follow-up: the dead `n_steps`/`max_step` in fwd/bwd is a cleanup candidate -(also the stale Codac-era file header comment). +per-step Taylor-coefficient cost (order) is the only step-cost lever. Kept tol +1e-10 (tighter = safer, no speed cost). Follow-up: the dead `n_steps`/`max_step` +in fwd/bwd is a cleanup candidate. + +### Vector-field CSE before to_capd_string (CAPD-side, deferred) + +Pre-simplifying / CSE-ing the ODE RHS with Drake's symbolic layer before emitting +`to_capd_string` could cut per-step AD cost (CAPD's `autodiff::Div` ~17% of order-10 runtime). +Medium-high effort, **low confidence**: the `a/c → a*(1/c)` rewrite is N/A (the probe families' +divisions are state-dependent — prostate `(/ z (+ z 2))`, the inverter's sigmoid terms — so the +division AD is inherent, not a constant-fold artifact), and CAPD's parser already does +within-string CSE, so a Drake-level pass may add little. The last untried CAPD-side idea; the +high-confidence config/allocation wins are harvested. + +--- + +## odeexpr (ODE-free QF_NRA) — separate code path + +**Why separate.** The high-priority `ode_expressivity` (odeexpr) family is **pure QF_NRA with +no ODEs** (transcendental-heavy: `sin`/`tanh`/`pow`/`exp`; quantifier-free; each sets +`:precision 5e-4`; Lyapunov positivity/stability/decrease obligations). `sample` confirms **0 +samples** in any `capd*`/`contractor_ode*` frame — the active path is +`IcpSeq → Fixpoint[ ContractorIbexFwdbwd × N, Integer ] → BranchLargestFirst`, single-threaded, +all of polytope/local-opt/pattern-matching off by default. Every §Adopted/§Rejected idea is in +CAPD code that **never runs here** — none can help or backfire. + +**A/B of the shared / default-off levers** (all 50, 600 s timeout, IcpSeq; reference = default): + +| arm | solved | PAR2 vs default | verdict flips | +|---|---|---|---| +| default | 36/50 | 1.00× | — | +| `--worklist-fixpoint` | 34/50 | **5.58× worse** | none | +| `--polytope` | 16/50\* | n/a (errors) | none | + +- **`--worklist-fixpoint`: net negative here too** — the same faster-on-SAT / catastrophic-on- + UNSAT variance as the ODE-side k17/k70 (pushes `tanh_decrease__J1.0` and `kuramoto_doe__N3` + over timeout, −2 solves). The ODE-grounds rejection holds on odeexpr. +- **`--polytope`: not usable in this build.** \*The 16 "solved" are trivial pre-contractor + instances; the rest exit 255 with `LPSolver method called but no LPSolver has been configured` + — IBEX was built without an LP backend (`-DLP_LIB` unset). Would need an LP-enabled IBEX first. +- **`--local-optimization`: provably inert** (exist-forall-only; odeexpr is quantifier-free). + +**The odeexpr hotspots — three mechanical overheads, all addressed.** Self-sample showed ~half +of odeexpr runtime was mechanical (mode switches + exception unwinding), not interval algebra: + +1. **`fesetround` (FPU mode switch), 23–44%.** Two slices. (a) A dReal-side slice: `is_integer` + (called per `pow` in `ExpressionEvaluator::VisitPow`) opened a `NearestRoundingScope` for + uniformity though it is mode-**independent**, forcing a needless `FE_UPWARD↔FE_TONEAREST` + flip per call — **removed** (`util/math.cc`), plus check-before-set in `RoundingModeGuard` + makes redundant nested scopes free (~9% relative on `pow`-dense). (b) The gaol-internal slice + (each interval transcendental toggles the mode around its mathlib call) — addressed in the + **ibex-fork**, levers #9 (inline aarch64 `msr` FPCR write) + #10 (batch the two directed + bounds into one nearest/upward window, halving toggles): **~8% aggregate**, bit-identical + (gated by `gaol_transcendental_bitidentity_test.cc`). See `../ibex-fork/MIGRATION.md`. +2. **C++ exception unwinding, 3–37%.** IBEX `HC4Revise` signalled an emptied domain by throwing + `EmptyBoxException`; UNSAT decrease/positivity proofs prune to empty at extreme frequency, so + `__cxa_throw`/`_Unwind_*` was on the ICP hot path (26.6% on `tanh_decrease__J1.0`). + **Eliminated** in the ibex-fork (patch #11): the whole shared backward engine returns a `bool` + instead of throwing; `Function::backward`'s public signature is unchanged (dReal already reads + `is_empty()`). `__cxa_throw` → **0%**; +2 odeexpr newly solved, 0 flips, `tanh_J1` 311→183 s + (1.7×). Guarded by the Phase-0 soundness net (`hc4_empty_propagation_soundness_test.cc`, + engine-level `empty01/empty02`), all written against the throw-based code first. +3. **Stat timer overhead, 4–16%.** `ContractorIbexFwdbwd::Prune` (and `…Polytope::Prune`) called + `stat.timer_pruning_.resume()/.pause()` unconditionally, so with default log level `off` + (`stat.enabled() = false`) two `steady_clock::now()` calls per `Prune` were computed and + discarded. **Fixed** by gating on `stat.enabled()`. `mach_continuous_time` 11.3% → 0% on + kuramoto__N6 (its short per-Prune work made the fixed overhead relatively large). + +**Post-fix profile (the remaining floor).** With all three addressed, `fesetround` and +`__cxa_throw` read ~0%. Three benchmarks (`sample`, leaf-level): + +| category | xwin1.5 (TIM) | kuramoto__N6 (TIM) | J0.6 (SAT) | +|---|---|---|---| +| gaol transcendentals (atanh/tanh/cos/sin/div_rel/sqrt_rel) | **44.8%** | **30.5%** | **45.2%** | +| HC4 backward | 11.4% | 12.0% | 12.0% | +| HC4 forward | 9.3% | 13.6% | 8.9% | +| ExpressionEvaluator (Drake VisitExpression/VisitPow) | 6.9% | 4.5% | 6.6% | +| Allocation (IntervalVector copies) | 5.4% | 5.2% | 5.2% | +| gaol interval arithmetic | 5.1% | 6.2% | 4.7% | +| fesetround / `__cxa_throw` | **~0%** | **~0%** | **~0%** | + +Gaol transcendentals (30–45%) are the **computational floor** — the actual correctly-rounded +interval math, irreducible without changing the interval library's soundness semantics. +Branching (`FindMaxDiam`) is ~0.4% — no headroom; a branching-heuristic A/B is ruled out. + +--- + +## Open avenues (deferred — post-timer-fix) + +These ideas are not yet attempted. Ordered by estimated confidence × effort. + +### A. ExpressionEvaluator overhead (medium confidence, medium effort) + +**What:** `EvaluateBox` calls dReal's own `ExpressionEvaluator` (the Drake symbolic traversal) +once per formula after every successful `Prune`, to check delta-satisfiability. This costs +4.5–7% of total runtime (profile above). Components: `VisitExpression` dispatch, hash-table +variable-index lookups (`__hash_table::__emplace_unique`, ~1.4%), and the coefficient +accumulate loop in `VisitAddition`. + +**Direction:** The hash-table lookup is a `map` index lookup done per +variable per eval. A flat sorted-vector or pre-built index array could replace it. +Alternatively, if the formula set is stable across ICP iterations (it is — it's set once), +precompiling the formula evaluators into IBEX `Function` objects (which already do CSE and +compile to a flat byte stream) and reusing the HC4 forward-eval path would eliminate the +Drake traversal entirely. That is a larger restructuring (the `FormulaEvaluator` and +`ExpressionEvaluator` classes are the eval layer). + +**Caution:** `EvaluateBox` also determines which formulas are violated (the `DynamicBitset` +returned) — branching uses this. Any replacement must preserve that output. + +### B. Allocation reduction — IntervalVector copies in HC4 (medium confidence, medium effort) + +**What:** `IntervalVector::IntervalVector` (copy constructor) and `_xzm_free` collectively ~5% +of runtime. The copy constructor appears in the HC4 forward pass (allocating the input vector +for each `Eval::eval` call) and in the backward pass's local snapshots. Post-Phase-2, +exception-elimination removed the `try/catch` frame but may not have changed heap turnover in +the backward engine's local allocations. + +**Direction:** Instrument IBEX's `eval` and backward paths with Instruments → Allocations +(or `malloc_count`) to confirm the allocation sites and count. If `IntervalVector` copies are +O(constraints × ICP-iterations), a preallocated workspace (thread-local or per-contractor) +that is resized-once and reused across calls could eliminate the per-call allocation. + +**Note:** This is in IBEX's core (`ibex::Eval`, `CompiledFunction`), so the change would live +in the ibex-fork, following the same pattern as the exception-elimination patches. + +### C. Per-constraint skip-if-unchanged gate (low confidence, medium effort) + +**What:** IBEX's `ContractorFixpoint` iterates all N constraints until no box shrinks. For +odeexpr's Lyapunov formulas, many constraints involve non-overlapping variable clusters; a +narrowing in constraint `i` rarely propagates to constraint `j` unless they share a variable. +A dependency graph that tracks which variables each constraint reads/writes could gate +re-evaluation of constraint `j` until one of its input variables changes. + +**Why low confidence:** The `--worklist-fixpoint` flag (a coarser version of this idea) +was measured net-negative on both ODE and odeexpr families — faster on SAT-easy instances +but catastrophically slow on UNSAT-difficult ones (k17 23 s → 0.85 s; k70 47 s → 7876 s). +A per-constraint graph rather than a global queue reorder might have better variance, but +that distinction is unproven. Profile above shows HC4 forward (13.6%) + backward (12%) = 25% +— so if this idea works, there is meaningful headroom. Worth a targeted A/B only if the +worklist-fixpoint catastrophe can be traced to the global reorder rather than the early-exit +logic. + +### D. Constraint ordering heuristic (low confidence, low effort) + +**What:** IBEX evaluates constraints in declaration order (as they appear in the parsed +`.smt2`). A heuristic that front-loads high-shrinkage constraints might cut fixpoint +iterations. The profile shows `HC4Revise::proj` (the per-constraint iteration entry point) +at ~1.6% leaf — the overhead of cycling through low-yield constraints is embedded in +`CompiledFunction::forward/backward`. Reordering is a one-time setup cost. + +**How to A/B:** Read the current constraint order from `ContractorFixpoint`'s contractor list +at solve start, sort by some heuristic (e.g. number of variables, or by profiling iteration +zero's shrinkage), then run. This is dReal-side and does not require ibex-fork changes. + +### E. Gaol Lever 3 — 1 toggle per transcendental (NO-GO for now) + +After Levers 1+2 (inline FPCR write + batched dn_up pairs → 2 toggles per transcendental), the +remaining gaol `fesetround` cost is the essential **2-per-transcendental** directed-rounding +round-trip, and it cannot be cut bit-identically: + +- The toggle is **structural.** Correctly-rounded transcendentals use double-double internal + arithmetic whose error analysis is valid **only in round-to-nearest**; gaol's ambient is + FE_UPWARD. So every interval transcendental round-trips upward→nearest→upward = 2 `msr fpcr` + writes. Verified dead ends: patching mathlib/libultim to not require nearest (round-to-nearest + is a documented correctness precondition, not a flag — `Init_Lib()` sets `FE_DFL_ENV`); + switching to crlibm (its directed functions are *also* nearest-wrapped); the logged + `lb = -round_up(-f(x))` "Lever 3" (a misconception — that identity flips upward⟷downward for + *arithmetic*; `f` is still the mathlib routine needing nearest). +- The only true eliminations are architectural and **not bit-identical** (verdict-shift risk at + the delta boundary, non-upstreamable): invert the ambient (keep FPU nearest, do interval + arithmetic with `next_float`/`previous_float` ULP bumps) or write custom upward-mode directed + transcendentals. + +**Measured ceiling: ≈13–16% on transcendental-dense benchmarks, ~6–10% aggregate** over the 50 +odeexpr (in-solver redundant-`msr` A/B: inject K extra round-trips between the two mathlib calls +— net mode unchanged, identical search trajectory — and measure the time delta; +11–13% per +added pair on the clean long-runners, a mild under-estimate). That is right at the bar for a +non-bit-identical change for a permanent fork liability — **NO-GO**. The unharvested +bit-identical avenues A–D (ExpressionEvaluator ~5–7%, allocation ~5%) are the better next step; +revisit msr-elimination only if A–D are exhausted and the densest instances remain msr-bound. diff --git a/README.md b/README.md index 0a72c4a0c..ab608f30d 100644 --- a/README.md +++ b/README.md @@ -27,7 +27,7 @@ cat YOUR_QUERY.smt2 | docker run --platform linux/amd64 --rm -i dreal/my_dreal_i Install dependencies via Homebrew: ``` -brew install bison flex gmp cadical eigen cmake +brew install bison flex gmp cadical cmake ``` Then build: @@ -42,7 +42,7 @@ The binary is at `gcc_build/dreal4`. CMakeLists.txt auto-detects Homebrew paths. Install dependencies: ``` -apt-get install -y clang cmake git bison flex libgmp-dev libeigen3-dev +apt-get install -y clang cmake git bison flex libgmp-dev ``` Build CaDiCaL 3.0.0 from source (not yet packaged on Ubuntu): diff --git a/benchmark/aggregate.py b/benchmark/aggregate.py index 5f9b98ce2..e87bf34fe 100755 --- a/benchmark/aggregate.py +++ b/benchmark/aggregate.py @@ -14,13 +14,45 @@ import sys from datetime import datetime, timezone +from odeexpr import family_of, FAMILY_WEIGHTS + SCRIPT_DIR = os.path.dirname(os.path.abspath(__file__)) REGRESSION_RATIO = 1.5 # PAR2 time > 1.5x baseline → regression EXCEPTIONAL_RATIO = 0.6 # PAR2 time < 0.6x baseline → exceptional -SOLVER_TIMEOUT_S = 300 # must match run_batch.sh `timeout 300` -PAR2_PENALTY_S = 2 * SOLVER_TIMEOUT_S # 600 s +SOLVER_TIMEOUT_S = 600 # must match run_batch.sh `timeout 600` +PAR2_PENALTY_S = 2 * SOLVER_TIMEOUT_S # 1200 s + +# Timing resolution / noise floors. gtime reports CPU time to ~0.01 s, so ratios +# below that are meaningless. NEGLIGIBLE_S: when BOTH baseline and current are +# this fast, skip the ratio check entirely (sub-0.1 s jitter on a multi-tenant +# box is noise, not a regression). TIME_FLOOR_S: clamp the divisor so a genuine +# instant→seconds jump still divides (and flags) instead of hitting 0. +NEGLIGIBLE_S = 0.1 +TIME_FLOOR_S = 0.01 + + +def safe_ratio(cur: float, base: float) -> float: + """PAR2 ratio with both operands floored at the measurement resolution.""" + return max(cur, TIME_FLOOR_S) / max(base, TIME_FLOOR_S) + +# odeexpr baseline lives in its own CSV (the other three are in baseline.csv / +# baseline_local.csv); produced by do_baseline_odeexpr.sh. +ODEEXPR_BASELINE = os.path.join(SCRIPT_DIR, "baseline_odeexpr.csv") + + +def row_time(row: dict) -> float | None: + """Primary timing for a result/baseline row: CPU time (cpu_time_s) if + present, else wall_time_s (older baselines predate the cpu_time_s column).""" + for col in ("cpu_time_s", "wall_time_s"): + val = row.get(col, "") + if val not in (None, ""): + try: + return float(val) + except (ValueError, TypeError): + pass + return None def par2_time(result: str, wall_time_s: float | None) -> float: @@ -43,10 +75,7 @@ def load_baseline(baseline_csv: str, column: str = "DRPM_0L") -> dict[str, dict] if not row or not row.get("benchmark_name", "").strip(): continue name = row["benchmark_name"].strip().removesuffix(".smt2") - try: - time_s = float(row.get("wall_time_s", "")) - except (ValueError, TypeError): - time_s = None + time_s = row_time(row) result = row.get("solver_result", "").strip() ground_truth = row.get("ground_truth", "").strip() baseline[name] = {"time_s": time_s, "result": result, @@ -115,25 +144,32 @@ def load_summary(summary_csv: str) -> list[dict]: return list(csv.DictReader(f)) -def family_of(name: str) -> str | None: - if name.startswith("1mhz_"): - return "saradc" - if name.startswith("github_oct5_"): - return "github" - if name.startswith("tacas_c2e2_"): - return "tacas" - return None +# Report ordering: correctness first, then the high-priority odeexpr family, +# then ordinary solve→fail (HIGH) and plain timing regressions. +_PRIORITY_ORDER = ["SOUNDNESS", "ODEEXPR-HIGH", "ODEEXPR", "HIGH", "TIMING"] + + +def priority_rank(priority: str) -> int: + return _PRIORITY_ORDER.index(priority) if priority in _PRIORITY_ORDER else len(_PRIORITY_ORDER) def compute_family_comparison(frozen_csv: str, local_summary: list[dict]) -> dict: """Compare per-family PAR2 averages between frozen baseline and new local run. Every benchmark present in both sets contributes its PAR2 time (actual time - if solved, PAR2_PENALTY_S=600 s if TIM/OOM/ERR). This ensures that + if solved, PAR2_PENALTY_S=1200 s if TIM/OOM/ERR). This ensures that formerly-TIM'd benchmarks that now solve lower the average rather than appearing to raise it. + + Families are weighted (FAMILY_WEIGHTS) into a `weighted_overall` PAR2 so the + high-priority odeexpr family dominates the single-number summary. """ frozen = load_baseline(frozen_csv, "DRPM_0L") + # The odeexpr family is not in the frozen DRPM_0L CSV; pull its reference + # from baseline_odeexpr.csv (new format). + if os.path.exists(ODEEXPR_BASELINE): + for name, entry in load_baseline(ODEEXPR_BASELINE).items(): + frozen.setdefault(name, entry) from collections import defaultdict frozen_par2: dict[str, list[float]] = defaultdict(list) @@ -148,25 +184,41 @@ def compute_family_comparison(frozen_csv: str, local_summary: list[dict]) -> dic if base is None: continue cur_result = row.get("solver_result", "") - cur_time = float(row["wall_time_s"]) if row.get("wall_time_s") else None + cur_time = row_time(row) local_par2[fam].append(par2_time(cur_result, cur_time)) frozen_par2[fam].append(par2_time(base["result"], base["time_s"])) result = {} - for fam in ("saradc", "github", "tacas"): + weighted_local_num = weighted_frozen_num = weight_den = 0.0 + for fam in ("saradc", "github", "tacas", "odeexpr"): lp = local_par2.get(fam, []) fp = frozen_par2.get(fam, []) if lp and fp: local_avg = sum(lp) / len(lp) frozen_avg = sum(fp) / len(fp) + w = FAMILY_WEIGHTS.get(fam, 1) + weighted_local_num += w * local_avg + weighted_frozen_num += w * frozen_avg + weight_den += w result[fam] = { "frozen_avg_par2": round(frozen_avg, 2), "local_avg_par2": round(local_avg, 2), - "ratio": round(local_avg / frozen_avg, 3), + "ratio": round(safe_ratio(local_avg, frozen_avg), 3), "n": len(lp), + "weight": w, } else: - result[fam] = {"frozen_avg_par2": None, "local_avg_par2": None, "ratio": None, "n": 0} + result[fam] = {"frozen_avg_par2": None, "local_avg_par2": None, + "ratio": None, "n": 0, "weight": FAMILY_WEIGHTS.get(fam, 1)} + + if weight_den: + wl = weighted_local_num / weight_den + wf = weighted_frozen_num / weight_den + result["weighted_overall"] = { + "frozen_avg_par2": round(wf, 2), + "local_avg_par2": round(wl, 2), + "ratio": round(wl / wf, 3) if wf else None, + } return result @@ -219,6 +271,13 @@ def main(): # Local baseline lacks ground_truth for this row — fill from frozen. baseline[name]["ground_truth"] = fentry.get("ground_truth", "") + # Merge the odeexpr baseline as a REAL timing reference (same machine, same + # 600 s budget) — unlike the frozen rows above, these carry a usable time_s, + # so the full PAR2 timing comparison applies to odeexpr benchmarks. + if os.path.exists(ODEEXPR_BASELINE): + for name, oentry in load_baseline(ODEEXPR_BASELINE).items(): + baseline[name] = oentry # authoritative for odeexpr rows + summary = load_summary(summary_csv) regressions = [] # {name, reason, baseline_time, current_time, baseline_result, current_result} @@ -236,7 +295,7 @@ def main(): for row in summary: name = row["benchmark_name"] cur_result = row["solver_result"] - cur_time = float(row["wall_time_s"]) if row["wall_time_s"] else None + cur_time = row_time(row) base = baseline.get(name) if base is None: @@ -295,18 +354,28 @@ def main(): # --- PAR2 timing comparison --- # Skipped for from_frozen rows (different machine, timing unreliable) and # correctness flips (already classified above). - # PAR2 time = actual wall time if solved, PAR2_PENALTY_S (600 s) otherwise. + # PAR2 time = actual CPU time if solved, PAR2_PENALTY_S (1200 s) otherwise. # This unifies solve→TIM regressions, TIM→solve improvements, and plain # timing regressions/speedups into a single ratio check. if not from_frozen and not result_flip: par2_base = par2_time(base_result, base_time) par2_cur = par2_time(cur_result, cur_time) - ratio = par2_cur / par2_base raw_note = (f" [raw: {cur_time:.1f}s]" if cur_time is not None else " [TIM/OOM/ERR]") + if par2_cur < NEGLIGIBLE_S and par2_base < NEGLIGIBLE_S: + ratio = 1.0 # both below measurement resolution — not comparable + else: + ratio = safe_ratio(par2_cur, par2_base) + if ratio > REGRESSION_RATIO: - priority = ("HIGH" if base_result in ("SAT", "UNSAT") - and cur_result in ("TIM", "OOM", "ERR") else "TIMING") + solve_to_fail = (base_result in ("SAT", "UNSAT") + and cur_result in ("TIM", "OOM", "ERR")) + # odeexpr is the high-priority target: its regressions outrank + # ordinary ones so the report/skill lead with them. + if family_of(name) == "odeexpr": + priority = "ODEEXPR-HIGH" if solve_to_fail else "ODEEXPR" + else: + priority = "HIGH" if solve_to_fail else "TIMING" regressions.append({ "name": name, "priority": priority, @@ -341,7 +410,7 @@ def main(): if regressions: f.write(f"=== REGRESSIONS ({len(regressions)}) ===\n") - for r in sorted(regressions, key=lambda x: x["priority"]): + for r in sorted(regressions, key=lambda x: priority_rank(x["priority"])): f.write(f" [{r['priority']}] {r['name']}\n") f.write(f" {r['reason']}\n") else: diff --git a/benchmark/baseline.csv b/benchmark/baseline.csv index 0fde72547..6ed851412 100644 --- a/benchmark/baseline.csv +++ b/benchmark/baseline.csv @@ -22,15 +22,11 @@ benchmark_file,,,,,,, 1mhz_k84_saradc_3b_nonlinear_12a_30e.smt2,59.089999999999996,30.1,1440.0,SolverResult.UNS,SolverResult.UNS,SolverResult.UNK, 1mhz_k84_saradc_3b_nonlinear_12a_31e.smt2,84.81,43.300000000000004,1440.0,SolverResult.UNS,SolverResult.UNS,SolverResult.UNK, 1mhz_k90_saradc_4b_box_10a_100000e.smt2,118.32000000000001,39.17,1440.0,SolverResult.UNS,SolverResult.UNS,SolverResult.UNK, -github_oct5_0hz_k1024_planning_one-var.drh.o.smt2,32.120000000000005,32.03,1440.0,SolverResult.UNS,SolverResult.UNS,SolverResult.MEM, -github_oct5_0hz_k1280_planning_one-var.drh.o.smt2,31.290000000000003,31.08,1440.0,SolverResult.UNS,SolverResult.UNS,SolverResult.MEM, github_oct5_0hz_k128_cardomain_car-3-single-linear-no-acc-no-lock.drh.n.smt2,82.49,54.61,1440.0,SolverResult.SAT,SolverResult.SAT,SolverResult.MEM, github_oct5_0hz_k128_quad_quad2-1.drh.o.smt2,37.839999999999996,36.42,1440.0,SolverResult.UNS,SolverResult.UNS,SolverResult.MEM, github_oct5_0hz_k128_water_water-double-network-sat.drh.n.smt2,108.72000000000001,108.95,1440.0,SolverResult.SAT,SolverResult.SAT,SolverResult.TIM, github_oct5_0hz_k128_water_water-double-network.drh.n.smt2,84.68,84.67999999999999,1440.0,SolverResult.SAT,SolverResult.SAT,SolverResult.TIM, -github_oct5_0hz_k1536_planning_one-var.drh.o.smt2,46.980000000000004,45.73,1440.0,SolverResult.UNS,SolverResult.UNS,SolverResult.MEM, github_oct5_0hz_k16_crazyflie_stabilizer.drh.o.smt2,82.74,82.94,118.94,SolverResult.UNS,SolverResult.UNS,SolverResult.UNS, -github_oct5_0hz_k2048_atrial_fibrillation_new_cardiac_stim.drh.o.smt2,39.65,35.14,1440.0,SolverResult.UNS,SolverResult.UNS,SolverResult.MEM, github_oct5_0hz_k256_gen_gen-0-multi-linear.drh.n.smt2,47.91,44.23,1440.0,SolverResult.UNS,SolverResult.UNS,SolverResult.MEM, github_oct5_0hz_k256_gen_gen-0-multi-nonlinear.drh.n.smt2,50.27,46.65,1440.0,SolverResult.UNS,SolverResult.UNS,SolverResult.MEM, github_oct5_0hz_k256_gen_gen-0-single-nonlinear.drh.n.smt2,81.83,73.77,1440.0,SolverResult.UNS,SolverResult.UNS,SolverResult.MEM, diff --git a/benchmark/baseline_local.csv b/benchmark/baseline_local.csv index 166b8a13f..26b496610 100644 --- a/benchmark/baseline_local.csv +++ b/benchmark/baseline_local.csv @@ -1,31 +1,81 @@ -benchmark_name,solver_result,wall_time_s,max_rss_kb,exit_code -1mhz_k20_saradc_2b_box_4a_1e,SAT,13.75,466016,0 -1mhz_k28_saradc_3b_box_4a_-1e,SAT,36.53,798944,0 -1mhz_k40_saradc_2b_box_8a_-1e,SAT,47.52,1341968,0 -1mhz_k70_saradc_3b_nonlinear_10a_100000e,UNSAT,70.72,4143536,0 -1mhz_k70_saradc_3b_nonlinear_10a_14e,UNSAT,71.02,4094576,0 -1mhz_k72_saradc_4b_nonlinear_8a_30e,UNSAT,21.16,4533408,0 -1mhz_k84_saradc_3b_box_12a_14e,UNSAT,78.08,5976352,0 -1mhz_k84_saradc_3b_nonlinear_12a_30e,UNSAT,32.36,5113840,0 -1mhz_k84_saradc_3b_nonlinear_12a_31e,UNSAT,32.40,5104688,0 -1mhz_k90_saradc_4b_box_10a_100000e,TIM,300.16,6182928,124 -github_oct5_0hz_k128_cardomain_car-3-single-linear-no-acc-no-lock.drh.n,SAT,267.86,2302096,0 -github_oct5_0hz_k256_gen_gen-0-multi-nonlinear.drh.n,UNSAT,18.21,1037168,0 -github_oct5_0hz_k32_cardomain_car-10-single-linear-no-acc-no-lock.drh.n,SAT,75.60,936608,0 -github_oct5_0hz_k32_water_water-triple-network.drh.n,SAT,1.91,107232,0 -github_oct5_0hz_k4_cardiac_new_cardiac.drh.o,TIM,300.00,14352,124 -github_oct5_0hz_k4_cardomain_car-1-single-linear-no-acc.drh.n,SAT,0.04,11712,0 -github_oct5_0hz_k4_cardomain_car-1-single-linear.drh.n,SAT,0.05,12528,0 -github_oct5_0hz_k4_cardomain_car-2-single-linear.drh.n,SAT,0.09,15616,0 -github_oct5_0hz_k64_cardomain_car-8-single-linear-no-acc-no-lock.drh.n,SAT,227.25,2305232,0 -github_oct5_0hz_k64_water_water-triple-network-sat.drh.n,SAT,9.13,346960,0 -tacas_c2e2_0hz_k112_20000.0clkhz_hybrid_inverter_sigmoid.hyxml_UNS.drh.o,UNSAT,0.66,122352,0 -tacas_c2e2_0hz_k11_10000.0clkhz_uniform_inverter_ramp.hyxml_SAT.drh.o,SAT,3.37,30128,0 -tacas_c2e2_0hz_k12_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o,SAT,59.77,25360,0 -tacas_c2e2_0hz_k12_50000.0clkhz_uniform_NOR_ramp.hyxml_UNS.drh.o,SAT,29.91,43328,0 -tacas_c2e2_0hz_k13_50000.0clkhz_uniform_NOR__sigmoid.hyxml_UNS.drh.o,SAT,65.04,28368,0 -tacas_c2e2_0hz_k17_50000.0clkhz_uniform_NOR__sigmoid.hyxml_UNS.drh.o,SAT,81.59,37472,0 -tacas_c2e2_0hz_k19_50000.0clkhz_uniform_NOR__sigmoid.hyxml_UNS.drh.o,SAT,92.42,46784,0 -tacas_c2e2_0hz_k20_50000.0clkhz_uniform_NOR__sigmoid.hyxml_UNS.drh.o,SAT,97.53,48656,0 -tacas_c2e2_0hz_k22_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o,SAT,112.38,54944,0 -tacas_c2e2_0hz_k8_50000.0clkhz_uniform_OR_sigmoid.hyxml_SAT.drh.o,SAT,90.63,23184,0 +benchmark_name,solver_result,cpu_time_s,wall_time_s,max_rss_kb,exit_code +1mhz_k20_saradc_2b_box_4a_-1e,SAT,10.94,11.36,396352,0 +1mhz_k28_saradc_3b_box_4a_-1e,SAT,47.09,48.25,791696,0 +1mhz_k30_saradc_2b_box_6a_2e,SAT,29.15,30.16,960960,0 +1mhz_k70_saradc_3b_nonlinear_10a_14e,UNSAT,61.44,62.66,3814880,0 +1mhz_k70_saradc_3b_nonlinear_10a_31e,UNSAT,60.33,61.78,3808400,0 +1mhz_k72_saradc_4b_nonlinear_8a_30e,UNSAT,19.70,21.03,4478192,0 +1mhz_k84_saradc_3b_box_12a_14e,UNSAT,68.48,69.98,5619040,0 +1mhz_k84_saradc_3b_box_12a_31e,UNSAT,67.58,68.96,5654352,0 +1mhz_k84_saradc_3b_nonlinear_12a_100000e,UNSAT,28.68,30.03,4934288,0 +1mhz_k84_saradc_3b_nonlinear_12a_30e,UNSAT,28.05,29.29,4933888,0 +github_oct5_0hz_k2_battery_battery-double-sat.drh.o,SAT,0.22,0.23,8336,0 +github_oct5_0hz_k2_battery_battery-double.drh.o,TIM,594.97,600.01,34368,124 +github_oct5_0hz_k2_prostate_cancer_scaled_prostate_infix.drh.o,SAT,75.87,76.53,14704,0 +github_oct5_0hz_k2_prostate_prostate_h2.drh.o,SAT,33.22,34.13,11376,0 +github_oct5_0hz_k2_prostate_prostate_p10.drh.o,TIM,595.44,600.01,11632,124 +github_oct5_0hz_k32_cardomain_car-10-flat-linear.drh.o,UNSAT,0.55,0.63,99856,0 +github_oct5_0hz_k4_cardomain_car-2-single-nonlinear.drh.n,SAT,13.55,14.02,16496,0 +github_oct5_0hz_k4_cardomain_car-3-single-linear.drh.n,SAT,44.78,45.05,20016,0 +github_oct5_0hz_k64_gen_gen-2-multi-linear.drh.n,UNSAT,145.15,145.98,2269920,0 +github_oct5_0hz_k8_airplane_airplane-single-network-sat.drh.n,SAT,0.94,0.95,28528,0 +odeexpr_box_sweep.ising__phi_7,UNSAT,0.00,0.01,5088,0 +odeexpr_box_sweep.ising__phi_pi,UNSAT,0.00,0.01,5184,0 +odeexpr_box_sweep.ising__phi_pi_2,UNSAT,0.00,0.01,5280,0 +odeexpr_box_sweep.ising__theta_2pi_5,UNSAT,0.00,0.01,5136,0 +odeexpr_box_sweep.ising__theta_pi_2_m0p1,UNSAT,0.00,0.01,5088,0 +odeexpr_box_sweep.tanh_decrease__J0.6,SAT,441.35,444.81,5408,0 +odeexpr_box_sweep.tanh_decrease__J1.0,SAT,176.91,177.38,5392,0 +odeexpr_box_sweep.tanh_decrease__xwin1.5,TIM,592.80,600.01,5312,124 +odeexpr_box_sweep.tanh_decrease__xwin2.0,TIM,592.57,600.01,5408,124 +odeexpr_cs2_lyapunov__corrected_V,UNSAT,0.00,0.01,5136,0 +odeexpr_cs2_overclaim__published_E,SAT,0.00,0.01,5424,0 +odeexpr_cs2b_contraction__local,UNSAT,0.00,0.01,5264,0 +odeexpr_cs2b_dgas__decrease,SAT,0.00,0.01,5472,0 +odeexpr_cs2b_dgas__observation,UNSAT,0.00,0.01,4560,0 +odeexpr_cs2b_dgas__positivity,UNSAT,0.00,0.01,5008,0 +odeexpr_cs3_expressivity__decrease,SAT,0.01,0.02,5392,0 +odeexpr_cs3_expressivity__observation,UNSAT,0.00,0.01,4288,0 +odeexpr_cs3_expressivity__positivity,UNSAT,0.00,0.01,4976,0 +odeexpr_cs4_equivalence__decrease,SAT,0.69,0.69,5520,0 +odeexpr_cs4_equivalence__observation,UNSAT,0.00,0.01,4240,0 +odeexpr_cs4_equivalence__positivity,UNSAT,0.00,0.01,4976,0 +odeexpr_cs5c_sigmoid__decrease,UNSAT,576.12,583.30,5504,0 +odeexpr_cs5c_sigmoid__observation,UNSAT,0.00,0.01,4256,0 +odeexpr_cs5c_sigmoid__positivity,UNSAT,0.00,0.01,4928,0 +odeexpr_ising_chain__stability,UNSAT,0.00,0.01,5216,0 +odeexpr_kuramoto_gradient__stability,UNSAT,0.00,0.01,5232,0 +odeexpr_nbody_momentum__decrease,UNSAT,0.00,0.01,5088,0 +odeexpr_size_sweep.aim_poly_vs_poly2__N2__decrease,SAT,0.01,0.01,6096,0 +odeexpr_size_sweep.aim_poly_vs_poly2__N3__decrease,SAT,0.02,0.02,10304,0 +odeexpr_size_sweep.aim_poly_vs_poly2__N4__decrease,SAT,0.06,0.06,21008,0 +odeexpr_size_sweep.aim_tanh_vs_mlp2__N2__decrease,SAT,0.01,0.01,6464,0 +odeexpr_size_sweep.aim_tanh_vs_mlp2__N3__decrease,SAT,0.01,0.02,7552,0 +odeexpr_size_sweep.aim_tanh_vs_mlp2__N4__decrease,SAT,0.03,0.04,12176,0 +odeexpr_size_sweep.kuramoto__N2,UNSAT,0.00,0.01,5408,0 +odeexpr_size_sweep.kuramoto__N3,UNSAT,0.01,0.02,5760,0 +odeexpr_size_sweep.kuramoto__N4,UNSAT,1.11,1.11,6256,0 +odeexpr_size_sweep.kuramoto__N5,UNSAT,88.51,88.82,6896,0 +odeexpr_size_sweep.kuramoto__N6,TIM,592.27,600.00,7888,124 +odeexpr_size_sweep.kuramoto_doe__N2,UNSAT,0.00,0.01,5344,0 +odeexpr_size_sweep.kuramoto_doe__N3,UNSAT,2.00,2.04,5824,0 +odeexpr_size_sweep.kuramoto_doe__N4,TIM,592.48,600.01,5968,124 +odeexpr_size_sweep.kuramoto_doe__N5,TIM,592.56,600.00,6688,124 +odeexpr_size_sweep.kuramoto_doe__N6,TIM,592.17,600.01,7328,124 +odeexpr_tanh.composite_lipschitz_i0,TIM,592.10,600.00,5184,124 +odeexpr_tanh.composite_lipschitz_i1,TIM,592.48,600.00,5264,124 +odeexpr_tanh.decrease_d_i__tau0.0015,TIM,595.37,600.00,5408,124 +odeexpr_tanh.decrease_d_i__tau0.0025,TIM,595.45,600.01,5456,124 +odeexpr_tanh.decrease_exact__tau0.0015,TIM,595.92,600.01,5376,124 +odeexpr_tanh.decrease_slope__tau0.0015,TIM,598.83,600.01,5312,124 +odeexpr_tanh.lipschitz_lemma_2var,UNSAT,0.04,0.06,5152,0 +tacas_c2e2_0hz_k10_50000.0clkhz_uniform_OR_sigmoid.hyxml_SAT.drh.o,SAT,110.57,111.01,24544,0 +tacas_c2e2_0hz_k11_10000.0clkhz_uniform_inverter_ramp.hyxml_SAT.drh.o,SAT,36.61,36.82,30768,0 +tacas_c2e2_0hz_k12_50000.0clkhz_uniform_OR_sigmoid.hyxml_SAT.drh.o,SAT,133.19,133.78,29088,0 +tacas_c2e2_0hz_k14_50000.0clkhz_uniform_NOR_ramp.hyxml_SAT.drh.o,SAT,43.16,43.41,51856,0 +tacas_c2e2_0hz_k15_50000.0clkhz_uniform_OR_sigmoid.hyxml_UNS.drh.o,SAT,165.08,165.60,42336,0 +tacas_c2e2_0hz_k17_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o,SAT,79.79,80.10,35568,0 +tacas_c2e2_0hz_k19_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o,SAT,89.37,89.72,44368,0 +tacas_c2e2_0hz_k23_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o,SAT,109.17,109.57,55488,0 +tacas_c2e2_0hz_k26_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o,SAT,124.58,125.06,63408,0 +tacas_c2e2_0hz_k6_50000.0clkhz_uniform_OR_sigmoid.hyxml_SAT.drh.o,SAT,66.66,66.95,17120,0 diff --git a/benchmark/baseline_odeexpr_cav26.csv b/benchmark/baseline_odeexpr_cav26.csv new file mode 100644 index 000000000..852839e10 --- /dev/null +++ b/benchmark/baseline_odeexpr_cav26.csv @@ -0,0 +1,44 @@ +benchmark_name,solver_result,cpu_time_s,wall_time_s,max_rss_kb,exit_code +odeexpr_box_sweep.ising__phi_7,UNSAT,0.07,0.09,7808,0 +odeexpr_box_sweep.ising__phi_pi,UNSAT,0.05,0.12,7584,0 +odeexpr_box_sweep.ising__phi_pi_2,UNSAT,0.05,0.12,7580,0 +odeexpr_box_sweep.ising__theta_2pi_5,UNSAT,0.07,0.08,7712,0 +odeexpr_box_sweep.ising__theta_pi_2_m0p1,UNSAT,0.07,0.08,7784,0 +odeexpr_box_sweep.tanh_decrease__J0.6,TIM,598.99,600.01,7956,124 +odeexpr_box_sweep.tanh_decrease__J1.0,SAT,562.71,563.77,8132,0 +odeexpr_box_sweep.tanh_decrease__xwin1.5,TIM,598.91,600.00,7932,124 +odeexpr_box_sweep.tanh_decrease__xwin2.0,TIM,599.03,600.00,7980,124 +odeexpr_cs2_lyapunov__corrected_V,UNSAT,0.05,0.06,7776,0 +odeexpr_cs2_overclaim__published_E,SAT,0.05,0.06,8068,0 +odeexpr_cs3_expressivity__decrease,SAT,0.06,0.08,7872,0 +odeexpr_cs3_expressivity__observation,UNSAT,0.04,0.05,6388,0 +odeexpr_cs3_expressivity__positivity,UNSAT,0.04,0.05,7396,0 +odeexpr_cs4_equivalence__decrease,SAT,2.28,2.29,8144,0 +odeexpr_cs4_equivalence__observation,UNSAT,0.04,0.05,6436,0 +odeexpr_cs4_equivalence__positivity,UNSAT,0.04,0.05,7468,0 +odeexpr_ising_chain__stability,UNSAT,0.04,0.05,7548,0 +odeexpr_kuramoto_gradient__stability,UNSAT,0.04,0.06,7652,0 +odeexpr_nbody_momentum__decrease,UNSAT,0.04,0.06,7304,0 +odeexpr_size_sweep.aim_poly_vs_poly2__N2__decrease,SAT,0.06,0.07,8232,0 +odeexpr_size_sweep.aim_poly_vs_poly2__N3__decrease,SAT,0.10,0.11,12160,0 +odeexpr_size_sweep.aim_poly_vs_poly2__N4__decrease,SAT,0.21,0.23,26228,0 +odeexpr_size_sweep.aim_tanh_vs_mlp2__N2__decrease,SAT,0.05,0.06,8232,0 +odeexpr_size_sweep.aim_tanh_vs_mlp2__N3__decrease,SAT,0.08,0.09,11584,0 +odeexpr_size_sweep.aim_tanh_vs_mlp2__N4__decrease,SAT,0.14,0.15,17528,0 +odeexpr_size_sweep.kuramoto__N2,UNSAT,0.04,0.05,7732,0 +odeexpr_size_sweep.kuramoto__N3,UNSAT,0.08,0.09,7932,0 +odeexpr_size_sweep.kuramoto__N4,UNSAT,3.48,3.50,8820,0 +odeexpr_size_sweep.kuramoto__N5,UNSAT,276.20,277.07,9484,0 +odeexpr_size_sweep.kuramoto__N6,TIM,598.98,600.01,10252,124 +odeexpr_size_sweep.kuramoto_doe__N2,UNSAT,0.04,0.05,7696,0 +odeexpr_size_sweep.kuramoto_doe__N3,UNSAT,6.13,6.14,8264,0 +odeexpr_size_sweep.kuramoto_doe__N4,TIM,599.03,600.01,8556,124 +odeexpr_size_sweep.kuramoto_doe__N5,TIM,598.87,600.01,9040,124 +odeexpr_size_sweep.kuramoto_doe__N6,TIM,599.03,600.01,9728,124 +odeexpr_tanh.composite_lipschitz_i0,TIM,599.02,600.01,7728,124 +odeexpr_tanh.composite_lipschitz_i1,TIM,598.87,600.01,7732,124 +odeexpr_tanh.decrease_d_i__tau0.0015,TIM,598.96,600.01,7956,124 +odeexpr_tanh.decrease_d_i__tau0.0025,TIM,599.72,600.00,7944,124 +odeexpr_tanh.decrease_exact__tau0.0015,TIM,599.92,600.01,7760,124 +odeexpr_tanh.decrease_slope__tau0.0015,TIM,599.93,600.00,7808,124 +odeexpr_tanh.lipschitz_lemma_2var,UNSAT,0.18,0.18,7596,0 diff --git a/benchmark/baseline_odeexpr_dreal3.csv b/benchmark/baseline_odeexpr_dreal3.csv new file mode 100644 index 000000000..8720aaa7a --- /dev/null +++ b/benchmark/baseline_odeexpr_dreal3.csv @@ -0,0 +1,44 @@ +benchmark_name,solver_result,cpu_time_s,wall_time_s,max_rss_kb,exit_code +odeexpr_box_sweep.ising__phi_7,UNSAT,0.07,,,0 +odeexpr_box_sweep.ising__phi_pi,UNSAT,0.07,,,0 +odeexpr_box_sweep.ising__phi_pi_2,UNSAT,0.07,,,0 +odeexpr_box_sweep.ising__theta_2pi_5,UNSAT,0.07,,,0 +odeexpr_box_sweep.ising__theta_pi_2_m0p1,UNSAT,0.07,,,0 +odeexpr_box_sweep.tanh_decrease__J0.6,TIM,599.97,,,124 +odeexpr_box_sweep.tanh_decrease__J1.0,TIM,599.99,,,124 +odeexpr_box_sweep.tanh_decrease__xwin1.5,TIM,600.00,,,124 +odeexpr_box_sweep.tanh_decrease__xwin2.0,TIM,600.01,,,124 +odeexpr_cs2_lyapunov__corrected_V,UNSAT,0.05,,,0 +odeexpr_cs2_overclaim__published_E,SAT,0.07,,,0 +odeexpr_cs3_expressivity__decrease,SAT,0.58,,,0 +odeexpr_cs3_expressivity__observation,UNSAT,0.04,,,0 +odeexpr_cs3_expressivity__positivity,UNSAT,0.05,,,0 +odeexpr_cs4_equivalence__decrease,SAT,81.38,,,0 +odeexpr_cs4_equivalence__observation,UNSAT,0.04,,,0 +odeexpr_cs4_equivalence__positivity,UNSAT,0.06,,,0 +odeexpr_ising_chain__stability,UNSAT,0.06,,,0 +odeexpr_kuramoto_gradient__stability,UNSAT,0.06,,,0 +odeexpr_nbody_momentum__decrease,UNSAT,0.06,,,0 +odeexpr_size_sweep.aim_poly_vs_poly2__N2__decrease,SAT,0.08,,,0 +odeexpr_size_sweep.aim_poly_vs_poly2__N3__decrease,SAT,0.08,,,0 +odeexpr_size_sweep.aim_poly_vs_poly2__N4__decrease,SAT,0.14,,,0 +odeexpr_size_sweep.aim_tanh_vs_mlp2__N2__decrease,SAT,0.06,,,0 +odeexpr_size_sweep.aim_tanh_vs_mlp2__N3__decrease,SAT,0.07,,,0 +odeexpr_size_sweep.aim_tanh_vs_mlp2__N4__decrease,SAT,0.10,,,0 +odeexpr_size_sweep.kuramoto__N2,UNSAT,0.06,,,0 +odeexpr_size_sweep.kuramoto__N3,UNSAT,0.17,,,0 +odeexpr_size_sweep.kuramoto__N4,UNSAT,14.80,,,0 +odeexpr_size_sweep.kuramoto__N5,TIM,600.00,,,124 +odeexpr_size_sweep.kuramoto__N6,TIM,599.96,,,124 +odeexpr_size_sweep.kuramoto_doe__N2,UNSAT,0.06,,,0 +odeexpr_size_sweep.kuramoto_doe__N3,UNSAT,19.91,,,0 +odeexpr_size_sweep.kuramoto_doe__N4,TIM,600.00,,,124 +odeexpr_size_sweep.kuramoto_doe__N5,TIM,599.99,,,124 +odeexpr_size_sweep.kuramoto_doe__N6,TIM,600.00,,,124 +odeexpr_tanh.composite_lipschitz_i0,TIM,600.00,,,124 +odeexpr_tanh.composite_lipschitz_i1,TIM,600.00,,,124 +odeexpr_tanh.decrease_d_i__tau0.0015,TIM,599.96,,,124 +odeexpr_tanh.decrease_d_i__tau0.0025,TIM,600.00,,,124 +odeexpr_tanh.decrease_exact__tau0.0015,TIM,599.99,,,124 +odeexpr_tanh.decrease_slope__tau0.0015,TIM,600.00,,,124 +odeexpr_tanh.lipschitz_lemma_2var,UNSAT,0.30,,,0 diff --git a/benchmark/compare_solvers.py b/benchmark/compare_solvers.py new file mode 100644 index 000000000..02582e463 --- /dev/null +++ b/benchmark/compare_solvers.py @@ -0,0 +1,151 @@ +#!/usr/bin/env python3 +"""Cross-solver comparison over the odeexpr set. + +Joins per-solver summary CSVs (benchmark_name, solver_result, cpu_time_s, ...) +by benchmark and reports: solve counts, per-benchmark verdict/timing, SAT↔UNSAT +disagreements, and CPU-time speedups on commonly-solved benchmarks. + +Usage: + compare_solvers.py HEAD=baseline_odeexpr.csv cav26=baseline_odeexpr_cav26.csv [dreal3=baseline_odeexpr_dreal3.csv] +""" +import csv +import statistics +import sys + +PAR2_PENALTY = 1200.0 # 2 * 600 s timeout +SOLVED = ("SAT", "UNSAT") + + +def load(path: str) -> dict[str, dict]: + out = {} + with open(path) as f: + for row in csv.DictReader(f): + name = row["benchmark_name"].strip().removesuffix(".smt2") + t = row.get("cpu_time_s", "") or row.get("wall_time_s", "") + try: + t = float(t) + except (ValueError, TypeError): + t = None + out[name] = {"result": row["solver_result"].strip(), "cpu": t} + return out + + +def par2(entry: dict) -> float: + return entry["cpu"] if entry["result"] in SOLVED and entry["cpu"] is not None else PAR2_PENALTY + + +def main(): + solvers: dict[str, dict] = {} + order: list[str] = [] + for arg in sys.argv[1:]: + label, path = arg.split("=", 1) + solvers[label] = load(path) + order.append(label) + + names = sorted(set().union(*[set(s) for s in solvers.values()])) + ref = order[0] # first solver is the reference (HEAD) + + # PAR2 is scored ONLY over benchmarks solved by at least one solver. A + # benchmark no solver cracks contributes the same 1200 s penalty to every + # solver — pure constant offset that dilutes real differences and carries no + # comparative information. + def solved_by_any(n): + return any(solvers[lab].get(n, {}).get("result") in SOLVED for lab in order) + scored = [n for n in names if solved_by_any(n)] + never = [n for n in names if not solved_by_any(n)] + + print(f"{'='*78}\nCROSS-SOLVER COMPARISON — {len(names)} benchmarks, reference = {ref}\n{'='*78}\n") + + # Solve counts (over the full set) + print("Solve counts (within 600 s wall, full set):") + for lab in order: + s = solvers[lab] + sat = sum(1 for n in names if s.get(n, {}).get("result") == "SAT") + uns = sum(1 for n in names if s.get(n, {}).get("result") == "UNSAT") + solved = sat + uns + print(f" {lab:8s} solved {solved:2d}/{len(names)} (SAT {sat}, UNSAT {uns}) unsolved {len(names)-solved:2d}") + print() + + # PAR2 table over the scored set (solved by >=1 solver) + print(f"PAR2 score — scored over {len(scored)} benchmarks solved by >=1 solver " + f"(excluded {len(never)} solved by none); penalty {PAR2_PENALTY:.0f}s:") + print(f" {'solver':8s} {'solved':>10s} {'PAR2 sum':>11s} {'PAR2 mean':>11s} {'vs '+ref:>10s}") + ref_mean = None + for lab in order: + s = solvers[lab] + nsolved = sum(1 for n in scored if s.get(n, {}).get("result") in SOLVED) + p2sum = sum(par2(s[n]) if n in s else PAR2_PENALTY for n in scored) + p2mean = p2sum / len(scored) if scored else 0.0 + if ref_mean is None: + ref_mean = p2mean + rel = f"{p2mean/ref_mean:.2f}x" if ref_mean else "—" + print(f" {lab:8s} {nsolved:>7d}/{len(scored):<2d} {p2sum:>10.1f}s {p2mean:>10.1f}s {rel:>10s}") + if never: + print(f"\n excluded (solved by none): {', '.join(n.replace('odeexpr_','') for n in never)}") + print() + + # Verdict disagreements (SAT vs UNSAT between any two solvers — notable) + disagree = [] + for n in names: + verdicts = {lab: solvers[lab].get(n, {}).get("result") for lab in order} + solved_v = {lab: v for lab, v in verdicts.items() if v in SOLVED} + if len(set(solved_v.values())) > 1: + disagree.append((n, verdicts)) + if disagree: + print(f"!! SAT/UNSAT DISAGREEMENTS ({len(disagree)}) — both solved but differ (delta-completeness or bug):") + for n, v in disagree: + print(f" {n}") + print(f" " + " ".join(f"{lab}={v[lab]}" for lab in order)) + print() + else: + print("No SAT/UNSAT disagreements among solved benchmarks.\n") + + # Solve-set deltas vs reference + for lab in order[1:]: + only_ref = [n for n in names + if solvers[ref].get(n, {}).get("result") in SOLVED + and solvers[lab].get(n, {}).get("result") not in SOLVED] + only_lab = [n for n in names + if solvers[lab].get(n, {}).get("result") in SOLVED + and solvers[ref].get(n, {}).get("result") not in SOLVED] + print(f"Solve-set {ref} vs {lab}:") + print(f" solved by {ref} but not {lab} ({len(only_ref)}): " + (", ".join(only_ref) or "—")) + print(f" solved by {lab} but not {ref} ({len(only_lab)}): " + (", ".join(only_lab) or "—")) + print() + + # Speedup on commonly-solved (CPU time) + for lab in order[1:]: + common = [n for n in names + if solvers[ref].get(n, {}).get("result") in SOLVED + and solvers[lab].get(n, {}).get("result") in SOLVED + and solvers[ref][n]["cpu"] and solvers[lab][n]["cpu"]] + if common: + ratios = [solvers[lab][n]["cpu"] / solvers[ref][n]["cpu"] for n in common] + ref_tot = sum(solvers[ref][n]["cpu"] for n in common) + lab_tot = sum(solvers[lab][n]["cpu"] for n in common) + print(f"CPU time on {len(common)} commonly-solved ({lab} / {ref}):") + print(f" total: {ref}={ref_tot:.2f}s {lab}={lab_tot:.2f}s " + f"aggregate ratio {lab_tot/ref_tot:.2f}x") + print(f" per-benchmark ratio: median {statistics.median(ratios):.2f}x " + f"min {min(ratios):.2f}x max {max(ratios):.2f}x " + f"({sum(1 for r in ratios if r>1)} slower / {sum(1 for r in ratios if r<1)} faster than {ref})") + print() + + # Per-benchmark table + print(f"{'-'*78}\nPER-BENCHMARK (result / CPU s):\n{'-'*78}") + hdr = f"{'benchmark':44s}" + "".join(f"{lab:>16s}" for lab in order) + print(hdr) + for n in names: + cells = "" + for lab in order: + e = solvers[lab].get(n) + if e is None: + cells += f"{'—':>16s}" + else: + t = f"{e['cpu']:.2f}" if e["cpu"] is not None else "—" + cells += f"{e['result']+' '+t:>16s}" + print(f"{n:44s}{cells}") + + +if __name__ == "__main__": + main() diff --git a/benchmark/do_ab.sh b/benchmark/do_ab.sh new file mode 100755 index 000000000..2214b0c1b --- /dev/null +++ b/benchmark/do_ab.sh @@ -0,0 +1,63 @@ +#!/usr/bin/env bash +# A/B two dreal4 binaries over the SAME job set, with honest timing. +# +# Usage: do_ab.sh BIN_A BIN_B [jobs_file] +# BIN_A, BIN_B : two dreal4 builds to compare (e.g. a committed-HEAD build vs a +# working-tree build, or /usr/local/bin/dreal4_cav26). +# jobs_file : TSV (csv_name filepath), one per line. Default = the full +# ODE-family corpus (select.py --family github,tacas,saradc --all). +# +# Reuses the standard harness (run_batch.sh honors DREAL_BINARY; parse_results.py; +# compare_solvers.py) instead of a freelance script, so an A/B is reproducible. +# +# The two binaries run SEQUENTIALLY (A fully finishes before B starts), never +# concurrently: run_batch.sh already parallelizes 12-way internally, and the 600 s +# TIM cutoff is WALL-clock — overlapping two batches would starve jobs and turn +# real solves into false TIMs (the measurement artifact this avoids). Timing is +# CPU time (user+sys) per the project methodology; wall is a reference/backup. +set -euo pipefail + +SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" +BIN_A="${1:?usage: do_ab.sh BIN_A BIN_B [jobs_file]}" +BIN_B="${2:?usage: do_ab.sh BIN_A BIN_B [jobs_file]}" +JOBS="${3:-}" + +for b in "$BIN_A" "$BIN_B"; do + [[ -x "$b" ]] || { echo "ERROR: not executable: $b" >&2; exit 1; } +done + +LA="$(basename "$BIN_A")" +LB="$(basename "$BIN_B")" +[[ "$LA" == "$LB" ]] && { LA="A_$LA"; LB="B_$LB"; } # disambiguate identical names + +# oom_killer daemon (SSD-protection; SMT solvers can swap indefinitely). +if ! pgrep -f oom_killer.sh > /dev/null 2>&1; then + nohup /usr/local/bin/oom_killer.sh &>/tmp/oom_killer.log & +fi + +TS=$(date +%Y%m%d_%H%M%S) +OUT="$SCRIPT_DIR/results/ab_${TS}" +mkdir -p "$OUT" + +if [[ -z "$JOBS" ]]; then + JOBS="$OUT/jobs.tsv" + python3 "$SCRIPT_DIR/select.py" --family github,tacas,saradc --all > "$JOBS" +fi +NJOBS=$(grep -c . "$JOBS") +echo "A/B over $NJOBS jobs: A=$LA B=$LB -> $OUT" >&2 + +run_side() { + local label="$1" bin="$2" + local out="$OUT/$label" + echo "=== running $label ($bin) ===" >&2 + DREAL_BINARY="$bin" bash "$SCRIPT_DIR/run_batch.sh" "$out" "$JOBS" + python3 "$SCRIPT_DIR/parse_results.py" "$out" >&2 +} + +run_side "$LA" "$BIN_A" # A fully completes ... +run_side "$LB" "$BIN_B" # ... before B starts (no cross-batch contention) + +python3 "$SCRIPT_DIR/compare_solvers.py" \ + "$LA=$OUT/$LA/summary.csv" "$LB=$OUT/$LB/summary.csv" | tee "$OUT/compare.txt" >&2 + +echo "$OUT" diff --git a/benchmark/do_baseline_odeexpr.sh b/benchmark/do_baseline_odeexpr.sh new file mode 100755 index 000000000..29efc1cf9 --- /dev/null +++ b/benchmark/do_baseline_odeexpr.sh @@ -0,0 +1,38 @@ +#!/usr/bin/env bash +# Establish the ode_expressivity (odeexpr) family baseline: run ALL 43 current +# benchmarks at the 600 s global timeout, under nice, measuring CPU time, and +# write benchmark/baseline_odeexpr.csv (new format with a cpu_time_s column). +# Prints OUT_DIR to stdout on completion; all other output goes to stderr. +# Usage: do_baseline_odeexpr.sh + +set -euo pipefail + +SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" +PROJECT_DIR="$(cd "$SCRIPT_DIR/.." && pwd)" +BINARY="$PROJECT_DIR/gcc_build/dreal4" + +if [[ ! -x "$BINARY" ]]; then + echo "ERROR: dreal4 binary not found at $BINARY" >&2 + exit 1 +fi + +# Check/start oom_killer (SMT solver resource-limit discipline). +if ! pgrep -f oom_killer.sh > /dev/null 2>&1; then + nohup /usr/local/bin/oom_killer.sh &>/tmp/oom_killer.log & +fi + +SHA=$(git -C "$PROJECT_DIR" rev-parse --short HEAD) +TS=$(date +%Y%m%d_%H%M%S) +OUT_DIR="$PROJECT_DIR/benchmark/results/baseline_odeexpr_${SHA}_${TS}" +JOBS_FILE="/tmp/dreal_odeexpr_jobs_${SHA}_${TS}.tsv" + +mkdir -p "$OUT_DIR" + +python3 "$SCRIPT_DIR/odeexpr.py" --all > "$JOBS_FILE" +bash "$SCRIPT_DIR/run_batch.sh" "$OUT_DIR" "$JOBS_FILE" +python3 "$SCRIPT_DIR/parse_results.py" "$OUT_DIR" >&2 + +# Save as the odeexpr baseline reference (aggregate.py loads this hardcoded path). +cp "$OUT_DIR/summary.csv" "$SCRIPT_DIR/baseline_odeexpr.csv" + +echo "$OUT_DIR" diff --git a/benchmark/do_benchmark.sh b/benchmark/do_benchmark.sh index fe65439e5..365fd7fee 100755 --- a/benchmark/do_benchmark.sh +++ b/benchmark/do_benchmark.sh @@ -29,6 +29,6 @@ mkdir -p "$OUT_DIR" python3 "$SCRIPT_DIR/select.py" > "$JOBS_FILE" bash "$SCRIPT_DIR/run_batch.sh" "$OUT_DIR" "$JOBS_FILE" python3 "$SCRIPT_DIR/parse_results.py" "$OUT_DIR" >&2 -python3 "$SCRIPT_DIR/aggregate.py" "$OUT_DIR" > "$OUT_DIR/aggregate.json" +python3 "$SCRIPT_DIR/aggregate.py" "$OUT_DIR" --frozen-baseline "$SCRIPT_DIR/baseline.csv" > "$OUT_DIR/aggregate.json" echo "$OUT_DIR" diff --git a/benchmark/do_sweep.sh b/benchmark/do_sweep.sh new file mode 100755 index 000000000..28534dc96 --- /dev/null +++ b/benchmark/do_sweep.sh @@ -0,0 +1,99 @@ +#!/usr/bin/env bash +# Sweep ONE dreal4 binary over multiple flag configurations on the SAME jobs. +# +# Usage: do_sweep.sh NAME1="" NAME2="" ... +# Each positional arg is label=flagstring (flagstring may be empty for the +# default/baseline point, e.g. base= ). The label names the per-config output +# subdir and the compare_solvers.py column; the flagstring is injected verbatim +# via the per-job flags column, e.g. o12="--ode-taylor-order 12". +# +# JOBS env: TSV jobs file (default = benchmark/probe_odes.tsv, the OFAT +# probe set). Point at select.py --family ... --all output for +# a full-corpus confirmation run. +# DREAL_BINARY env: solver to sweep (default = ../gcc_build/dreal4). +# MAXJOBS env: pool width (default 12, the project's standard concurrency). +# TIMEOUT env: per-job wall cap in seconds (default 600). +# +# POOLED execution: all (config x benchmark) pairs run in ONE shuffled MAXJOBS-way +# queue, NOT one batch per config. This is the fix for the idle-tail waste of +# per-config batches — an 18-job probe drains to its 2-3 long-poles (e.g. a k256 +# thermostat) while 13 cores sit idle; pooling overlaps a slow config's long-pole +# with other configs' fast jobs, so the cores stay full. Crucially this does NOT +# oversubscribe: at most MAXJOBS solver processes run at once, each nice -n 1 on +# its own core, so the per-process CPU-time metric stays accurate (same per-core +# fairness as run_batch's 12-way, just better packed). The shuffle spreads the +# long-poles across the run so the only thin tail is the final ~MAXJOBS jobs. +# Reuses parse_results.py + compare_solvers.py for the table. +set -uo pipefail + +SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" +[[ $# -ge 1 ]] || { echo "usage: do_sweep.sh NAME='flags' NAME='flags' ..." >&2; exit 1; } + +BINARY="${DREAL_BINARY:-$SCRIPT_DIR/../gcc_build/dreal4}" +[[ -x "$BINARY" ]] || { echo "ERROR: solver not executable: $BINARY" >&2; exit 1; } +JOBS="${JOBS:-$SCRIPT_DIR/probe_odes.tsv}" +[[ -f "$JOBS" ]] || { echo "ERROR: jobs file not found: $JOBS" >&2; exit 1; } +MAXJOBS="${MAXJOBS:-12}" +TIMEOUT="${TIMEOUT:-600}" + +# oom_killer daemon (SSD-protection; SMT solvers can swap indefinitely). +if ! pgrep -f oom_killer.sh > /dev/null 2>&1; then + nohup /usr/local/bin/oom_killer.sh &>/tmp/oom_killer.log & +fi + +TS=$(date +%Y%m%d_%H%M%S) +OUT="$SCRIPT_DIR/results/sweep_${TS}" +mkdir -p "$OUT" + +# Build the cartesian (config x benchmark) job list as +# config flags csv path +# Flags for the `base` point are empty; an empty TSV field is collapsed by +# `read` (tab is whitespace-class IFS), which would shift `path` out of range +# and silently drop that config. So empty flags are encoded as the sentinel +# NONE (decoded back to "" in the runner) — every field is then non-empty. +# (bash 3.2 on macOS has no associative arrays, hence a TSV column not a map.) +labels=() +JOBS4="$OUT/_pool_jobs.tsv"; : > "$JOBS4" +for spec in "$@"; do + if [[ "$spec" == *=* ]]; then label="${spec%%=*}"; flags="${spec#*=}"; else label="$spec"; flags=""; fi + labels+=("$label") + [[ -z "$flags" ]] && flags="NONE" + mkdir -p "$OUT/$label" + while IFS=$'\t' read -r csv path; do + [[ -z "$csv" || -z "$path" ]] && continue + printf '%s\t%s\t%s\t%s\n' "$label" "$flags" "$csv" "$path" >> "$JOBS4" + done < "$JOBS" +done +NJOBS=$(grep -c . "$JOBS") +NRUNS=$(grep -c . "$JOBS4") +echo "sweep: ${#labels[@]} configs x $NJOBS jobs = $NRUNS runs, ${MAXJOBS}-way pool, ${TIMEOUT}s cap -> $OUT" >&2 + +# Portable shuffle (no GNU shuf on macOS): prefix a random key, sort, strip it. +SHUF="$OUT/_pool_shuffled.tsv" +awk 'BEGIN{srand()} {print rand()"\t"$0}' "$JOBS4" | sort -n | cut -f2- > "$SHUF" + +# One MAXJOBS-way pool over ALL pairs. +while IFS=$'\t' read -r config flags csv path; do + [[ -z "$config" || -z "$path" ]] && continue + [[ "$flags" == "NONE" ]] && flags="" + label="${csv%.smt2}" + d="$OUT/$config" + while (( $(jobs -r | wc -l) >= MAXJOBS )); do sleep 0.1; done + ( + gtime -v -o "$d/${label}.gtime" nice -n 1 timeout "$TIMEOUT" "$BINARY" $flags "$path" \ + > "$d/${label}.stdout" \ + 2> "$d/${label}.solver_log" + echo $? > "$d/${label}.exit" + ) & +done < "$SHUF" +wait +echo "pool complete." >&2 + +compare_args=() +for label in "${labels[@]}"; do + python3 "$SCRIPT_DIR/parse_results.py" "$OUT/$label" >&2 + compare_args+=("$label=$OUT/$label/summary.csv") +done + +python3 "$SCRIPT_DIR/compare_solvers.py" "${compare_args[@]}" | tee "$OUT/compare.txt" >&2 +echo "$OUT" diff --git a/benchmark/odeexpr.py b/benchmark/odeexpr.py new file mode 100644 index 000000000..8fa1a7165 --- /dev/null +++ b/benchmark/odeexpr.py @@ -0,0 +1,109 @@ +#!/usr/bin/env python3 +"""Shared definitions for the `odeexpr` benchmark family (ode_expressivity set). + +Single source of truth for: where the set lives, per-family selection weights, +family classification, and name<->path resolution. Unlike the other three +families (whose paths are flat directories), odeexpr is content-addressed: each +logical benchmark (`bench_id`) has hashed revision files and a `manifest.json` +that names the *current* revision. We key on the stable `bench_id` and resolve +through the manifest so regeneration (which mints new hashed files, never +overwrites) does not silently change which file a name points at. + +A benchmark name in this family is `odeexpr_`, e.g. +`odeexpr_box_sweep.ising__phi_7`. + +CLI: `python3 odeexpr.py --all` prints TSV (name abspath) for all 43. +""" +import json +import os +import sys + +ODEEXPR_ROOT = "/Users/kunalsheth/Documents/new_dreal/ode_expressivity/benchmarks" +MANIFEST_PATH = os.path.join(ODEEXPR_ROOT, "manifest.json") +PREFIX = "odeexpr_" + +# Per-family selection/severity weights. Encodes the user's equivalence +# "1 odeexpr = 3 github = 2 saradc = 3 tacas": with odeexpr=6, github/tacas=2, +# saradc=3, one odeexpr equals 3 github (3*2), 2 saradc (2*3), 3 tacas (3*2). +FAMILY_WEIGHTS = {"odeexpr": 6, "saradc": 3, "github": 2, "tacas": 2} + + +def family_of(name: str) -> str | None: + """Classify a (possibly .smt2-suffixed) benchmark name into its family.""" + if name.startswith(PREFIX): + return "odeexpr" + if name.startswith("1mhz_"): + return "saradc" + if name.startswith("github_oct5_"): + return "github" + if name.startswith("tacas_c2e2_"): + return "tacas" + return None + + +def weight_of(name: str) -> float: + """Selection weight for a benchmark name (defaults to 1 for unknown families).""" + fam = family_of(name) + return FAMILY_WEIGHTS.get(fam, 1) if fam else 1 + + +def _load_manifest() -> dict: + with open(MANIFEST_PATH) as f: + return json.load(f) + + +def _current_file(entry: dict) -> str | None: + """Relative path of the entry's current revision, or None.""" + for rev in entry.get("revisions", []): + if rev.get("state") == "current": + return rev.get("file") + return None + + +def load_odeexpr_names() -> list[str]: + """All active odeexpr benchmark names whose current file exists on disk.""" + manifest = _load_manifest() + names = [] + for bench_id, entry in manifest.items(): + if entry.get("status") != "active": + continue + rel = _current_file(entry) + if rel and os.path.exists(os.path.join(ODEEXPR_ROOT, rel)): + names.append(PREFIX + bench_id) + return sorted(names) + + +def resolve_odeexpr(name: str) -> str | None: + """Map `odeexpr_` to its current revision's absolute path.""" + if not name.startswith(PREFIX): + return None + bench_id = name[len(PREFIX):].removesuffix(".smt2") + manifest = _load_manifest() + entry = manifest.get(bench_id) + if entry is None: + return None + rel = _current_file(entry) + if not rel: + return None + path = os.path.join(ODEEXPR_ROOT, rel) + return path if os.path.exists(path) else None + + +def main(): + if len(sys.argv) >= 2 and sys.argv[1] == "--all": + n = 0 + for name in load_odeexpr_names(): + path = resolve_odeexpr(name) + if path: + print(f"{name}\t{path}") + n += 1 + else: + print(f"WARN: could not resolve {name}", file=sys.stderr) + print(f"Listed {n} odeexpr benchmarks.", file=sys.stderr) + else: + print("Usage: odeexpr.py --all", file=sys.stderr) + sys.exit(1) + + +if __name__ == "__main__": + main() diff --git a/benchmark/odeexpr_solver_comparison.txt b/benchmark/odeexpr_solver_comparison.txt new file mode 100644 index 000000000..46b9b90cd --- /dev/null +++ b/benchmark/odeexpr_solver_comparison.txt @@ -0,0 +1,82 @@ +============================================================================== +CROSS-SOLVER COMPARISON — 43 benchmarks, reference = HEAD +============================================================================== + +Solve counts (within 600 s wall, full set): + HEAD solved 30/43 (SAT 10, UNSAT 20) unsolved 13 + cav26 solved 30/43 (SAT 10, UNSAT 20) unsolved 13 + dreal3 solved 28/43 (SAT 9, UNSAT 19) unsolved 15 + +PAR2 score — scored over 30 benchmarks solved by >=1 solver (excluded 13 solved by none); penalty 1200s: + solver solved PAR2 sum PAR2 mean vs HEAD + HEAD 30/30 423.5s 14.1s 1.00x + cav26 30/30 852.5s 28.4s 2.01x + dreal3 28/30 2518.6s 84.0s 5.95x + + excluded (solved by none): box_sweep.tanh_decrease__J0.6, box_sweep.tanh_decrease__xwin1.5, box_sweep.tanh_decrease__xwin2.0, size_sweep.kuramoto__N6, size_sweep.kuramoto_doe__N4, size_sweep.kuramoto_doe__N5, size_sweep.kuramoto_doe__N6, tanh.composite_lipschitz_i0, tanh.composite_lipschitz_i1, tanh.decrease_d_i__tau0.0015, tanh.decrease_d_i__tau0.0025, tanh.decrease_exact__tau0.0015, tanh.decrease_slope__tau0.0015 + +No SAT/UNSAT disagreements among solved benchmarks. + +Solve-set HEAD vs cav26: + solved by HEAD but not cav26 (0): — + solved by cav26 but not HEAD (0): — + +Solve-set HEAD vs dreal3: + solved by HEAD but not dreal3 (2): odeexpr_box_sweep.tanh_decrease__J1.0, odeexpr_size_sweep.kuramoto__N5 + solved by dreal3 but not HEAD (0): — + +CPU time on 14 commonly-solved (cav26 / HEAD): + total: HEAD=423.46s cav26=851.76s aggregate ratio 2.01x + per-benchmark ratio: median 2.98x min 1.84x max 6.00x (14 slower / 0 faster than HEAD) + +CPU time on 12 commonly-solved (dreal3 / HEAD): + total: HEAD=5.89s dreal3=117.67s aggregate ratio 19.98x + per-benchmark ratio: median 6.48x min 1.75x max 65.63x (12 slower / 0 faster than HEAD) + +------------------------------------------------------------------------------ +PER-BENCHMARK (result / CPU s): +------------------------------------------------------------------------------ +benchmark HEAD cav26 dreal3 +odeexpr_box_sweep.ising__phi_7 UNSAT 0.00 UNSAT 0.07 UNSAT 0.07 +odeexpr_box_sweep.ising__phi_pi UNSAT 0.00 UNSAT 0.05 UNSAT 0.07 +odeexpr_box_sweep.ising__phi_pi_2 UNSAT 0.00 UNSAT 0.05 UNSAT 0.07 +odeexpr_box_sweep.ising__theta_2pi_5 UNSAT 0.00 UNSAT 0.07 UNSAT 0.07 +odeexpr_box_sweep.ising__theta_pi_2_m0p1 UNSAT 0.00 UNSAT 0.07 UNSAT 0.07 +odeexpr_box_sweep.tanh_decrease__J0.6 TIM 598.62 TIM 598.99 TIM 599.97 +odeexpr_box_sweep.tanh_decrease__J1.0 SAT 298.58 SAT 562.71 TIM 599.99 +odeexpr_box_sweep.tanh_decrease__xwin1.5 TIM 598.63 TIM 598.91 TIM 600.00 +odeexpr_box_sweep.tanh_decrease__xwin2.0 TIM 598.66 TIM 599.03 TIM 600.01 +odeexpr_cs2_lyapunov__corrected_V UNSAT 0.00 UNSAT 0.05 UNSAT 0.05 +odeexpr_cs2_overclaim__published_E SAT 0.00 SAT 0.05 SAT 0.07 +odeexpr_cs3_expressivity__decrease SAT 0.01 SAT 0.06 SAT 0.58 +odeexpr_cs3_expressivity__observation UNSAT 0.00 UNSAT 0.04 UNSAT 0.04 +odeexpr_cs3_expressivity__positivity UNSAT 0.00 UNSAT 0.04 UNSAT 0.05 +odeexpr_cs4_equivalence__decrease SAT 1.24 SAT 2.28 SAT 81.38 +odeexpr_cs4_equivalence__observation UNSAT 0.00 UNSAT 0.04 UNSAT 0.04 +odeexpr_cs4_equivalence__positivity UNSAT 0.00 UNSAT 0.04 UNSAT 0.06 +odeexpr_ising_chain__stability UNSAT 0.00 UNSAT 0.04 UNSAT 0.06 +odeexpr_kuramoto_gradient__stability UNSAT 0.00 UNSAT 0.04 UNSAT 0.06 +odeexpr_nbody_momentum__decrease UNSAT 0.00 UNSAT 0.04 UNSAT 0.06 +odeexpr_size_sweep.aim_poly_vs_poly2__N2__decrease SAT 0.01 SAT 0.06 SAT 0.08 +odeexpr_size_sweep.aim_poly_vs_poly2__N3__decrease SAT 0.03 SAT 0.10 SAT 0.08 +odeexpr_size_sweep.aim_poly_vs_poly2__N4__decrease SAT 0.08 SAT 0.21 SAT 0.14 +odeexpr_size_sweep.aim_tanh_vs_mlp2__N2__decrease SAT 0.01 SAT 0.05 SAT 0.06 +odeexpr_size_sweep.aim_tanh_vs_mlp2__N3__decrease SAT 0.02 SAT 0.08 SAT 0.07 +odeexpr_size_sweep.aim_tanh_vs_mlp2__N4__decrease SAT 0.04 SAT 0.14 SAT 0.10 +odeexpr_size_sweep.kuramoto__N2 UNSAT 0.00 UNSAT 0.04 UNSAT 0.06 +odeexpr_size_sweep.kuramoto__N3 UNSAT 0.02 UNSAT 0.08 UNSAT 0.17 +odeexpr_size_sweep.kuramoto__N4 UNSAT 1.50 UNSAT 3.48 UNSAT 14.80 +odeexpr_size_sweep.kuramoto__N5 UNSAT 118.99 UNSAT 276.20 TIM 600.00 +odeexpr_size_sweep.kuramoto__N6 TIM 598.65 TIM 598.98 TIM 599.96 +odeexpr_size_sweep.kuramoto_doe__N2 UNSAT 0.00 UNSAT 0.04 UNSAT 0.06 +odeexpr_size_sweep.kuramoto_doe__N3 UNSAT 2.86 UNSAT 6.13 UNSAT 19.91 +odeexpr_size_sweep.kuramoto_doe__N4 TIM 598.68 TIM 599.03 TIM 600.00 +odeexpr_size_sweep.kuramoto_doe__N5 TIM 598.68 TIM 598.87 TIM 599.99 +odeexpr_size_sweep.kuramoto_doe__N6 TIM 598.66 TIM 599.03 TIM 600.00 +odeexpr_tanh.composite_lipschitz_i0 TIM 598.63 TIM 599.02 TIM 600.00 +odeexpr_tanh.composite_lipschitz_i1 TIM 598.66 TIM 598.87 TIM 600.00 +odeexpr_tanh.decrease_d_i__tau0.0015 TIM 598.65 TIM 598.96 TIM 599.96 +odeexpr_tanh.decrease_d_i__tau0.0025 TIM 598.72 TIM 599.72 TIM 600.00 +odeexpr_tanh.decrease_exact__tau0.0015 TIM 599.16 TIM 599.92 TIM 599.99 +odeexpr_tanh.decrease_slope__tau0.0015 TIM 599.80 TIM 599.93 TIM 600.00 +odeexpr_tanh.lipschitz_lemma_2var UNSAT 0.07 UNSAT 0.18 UNSAT 0.30 diff --git a/benchmark/parse_results.py b/benchmark/parse_results.py index fb216af6b..3f76c49bd 100755 --- a/benchmark/parse_results.py +++ b/benchmark/parse_results.py @@ -3,7 +3,11 @@ Usage: python3 parse_results.py Produces /summary.csv with columns: - benchmark_name, solver_result, wall_time_s, max_rss_kb, exit_code + benchmark_name, solver_result, cpu_time_s, wall_time_s, max_rss_kb, exit_code + +`cpu_time_s` (User+System time) is the primary timing metric — the machine is +multi-tenant, so wall clock is noisy and unfairly penalizes a descheduled run. +`wall_time_s` is kept for reference and as a TIM backup signal. """ import csv import os @@ -21,6 +25,15 @@ def parse_wall_time(gtime_text: str) -> float | None: return None +def parse_cpu_time(gtime_text: str) -> float | None: + """CPU time = User time + System time (seconds), from gtime -v output.""" + u = re.search(r"User time \(seconds\):\s*([\d.]+)", gtime_text) + s = re.search(r"System time \(seconds\):\s*([\d.]+)", gtime_text) + if u and s: + return float(u.group(1)) + float(s.group(1)) + return None + + def parse_rss(gtime_text: str) -> int | None: m = re.search(r"Maximum resident set size \(kbytes\):\s*(\d+)", gtime_text) return int(m.group(1)) if m else None @@ -29,7 +42,7 @@ def parse_rss(gtime_text: str) -> int | None: def parse_solver_result(stdout_text: str, exit_code: int, wall_time_s: float | None) -> str: if exit_code == 137: return "OOM" - if exit_code == 124 or (wall_time_s is not None and wall_time_s > 295): + if exit_code == 124 or (wall_time_s is not None and wall_time_s > 595): return "TIM" if "delta-sat" in stdout_text: return "SAT" @@ -56,12 +69,14 @@ def parse_results_dir(results_dir: str) -> list[dict]: gtime_text = open(gtime_path).read() if os.path.exists(gtime_path) else "" wall_time = parse_wall_time(gtime_text) + cpu_time = parse_cpu_time(gtime_text) max_rss = parse_rss(gtime_text) result = parse_solver_result(stdout_text, exit_code, wall_time) rows.append({ "benchmark_name": name, "solver_result": result, + "cpu_time_s": f"{cpu_time:.2f}" if cpu_time is not None else "", "wall_time_s": f"{wall_time:.2f}" if wall_time is not None else "", "max_rss_kb": str(max_rss) if max_rss is not None else "", "exit_code": str(exit_code), @@ -79,7 +94,7 @@ def main(): out_path = os.path.join(results_dir, "summary.csv") with open(out_path, "w", newline="") as f: - writer = csv.DictWriter(f, fieldnames=["benchmark_name", "solver_result", "wall_time_s", "max_rss_kb", "exit_code"]) + writer = csv.DictWriter(f, fieldnames=["benchmark_name", "solver_result", "cpu_time_s", "wall_time_s", "max_rss_kb", "exit_code"]) writer.writeheader() writer.writerows(rows) diff --git a/benchmark/probe_baseline.csv b/benchmark/probe_baseline.csv deleted file mode 100644 index fe1d37871..000000000 --- a/benchmark/probe_baseline.csv +++ /dev/null @@ -1,19 +0,0 @@ -benchmark_name,solver_result,wall_time_s,max_rss_kb,exit_code -1mhz_k20_saradc_2b_box_4a_-1e,SAT,5.30,397232,0 -1mhz_k28_saradc_3b_box_4a_-1e,SAT,29.09,814304,0 -1mhz_k40_saradc_2b_box_8a_-1e,SAT,34.19,1369696,0 -1mhz_k70_saradc_3b_nonlinear_10a_15e,UNSAT,55.83,4404176,0 -1mhz_k72_saradc_4b_nonlinear_8a_30e,UNSAT,17.39,4848960,0 -github_oct5_0hz_k128_quad_quad2-1.drh.o,TIM,300.02,4173376,124 -github_oct5_0hz_k2048_atrial_fibrillation_new_cardiac_stim.drh.o,UNSAT,6.94,533664,0 -github_oct5_0hz_k2_prostate_prostate_h2.drh.o,SAT,13.41,9792,0 -github_oct5_0hz_k64_cardomain_car-7-flat-nonlinear.drh.o,UNSAT,0.22,50672,0 -github_oct5_0hz_k64_cardomain_car-9-flat-nonlinear.drh.o,UNSAT,0.30,65984,0 -tacas_c2e2_0hz_k10_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o,SAT,46.42,22240,0 -tacas_c2e2_0hz_k112_20000.0clkhz_hybrid_inverter_sigmoid.hyxml_UNS.drh.o,UNSAT,0.69,122032,0 -tacas_c2e2_0hz_k12_50000.0clkhz_uniform_NOR_ramp.hyxml_SAT.drh.o,SAT,37.31,39232,0 -tacas_c2e2_0hz_k13_10000.0clkhz_uniform_inverter_sigmoid.hyxml_SAT.drh.o,TIM,300.00,20240,124 -tacas_c2e2_0hz_k14_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o,SAT,66.20,29360,0 -tacas_c2e2_0hz_k16_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o,SAT,76.46,32592,0 -tacas_c2e2_0hz_k17_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o,SAT,81.63,36704,0 -tacas_c2e2_0hz_k4_50000.0clkhz_uniform_OR_sigmoid.hyxml_SAT.drh.o,SAT,44.45,17088,0 diff --git a/benchmark/probe_compare.py b/benchmark/probe_compare.py deleted file mode 100644 index 5009a2291..000000000 --- a/benchmark/probe_compare.py +++ /dev/null @@ -1,135 +0,0 @@ -#!/usr/bin/env python3 -"""Compare a probe run against the frozen probe baseline (self-contained). - -The ODE-heavy probe set (probe_odes.tsv) is NOT in baseline_local.csv, so the -gate's aggregate.py/state.json machinery can't score it. This comparator is -self-contained: it diffs a probe run's summary.csv against probe_baseline.csv, -reports per-benchmark PAR2 ratios, the net PAR2 ratio, regressions (>1.5x), -exceptional speedups (<0.6x), and — critically — any SAT/UNSAT correctness -flips (vs the baseline result, and vs ground_truth from baseline.csv where -available). Reuses par2_time + thresholds from aggregate.py so scoring matches -the gate exactly. - -Usage: python3 probe_compare.py [--baseline probe_baseline.csv] -""" -import argparse -import csv -import os -import sys - -SCRIPT_DIR = os.path.dirname(os.path.abspath(__file__)) -sys.path.insert(0, SCRIPT_DIR) -from aggregate import par2_time, REGRESSION_RATIO, EXCEPTIONAL_RATIO # noqa: E402 - - -def load_summary(path: str) -> dict: - out = {} - with open(path) as f: - for row in csv.DictReader(f): - name = row["benchmark_name"].removesuffix(".smt2") - try: - t = float(row["wall_time_s"]) - except (ValueError, KeyError, TypeError): - t = None - out[name] = {"result": row["solver_result"], "time": t} - return out - - -def load_ground_truth(frozen_csv: str) -> dict: - """benchmark name (no .smt2) -> ground_truth string (SAT/UNSAT/'').""" - gt = {} - if not os.path.exists(frozen_csv): - return gt - with open(frozen_csv) as f: - rows = list(csv.reader(f)) - for row in rows[3:]: - if row and row[0].strip(): - name = row[0].strip().removesuffix(".smt2") - gt[name] = (row[7].strip() if len(row) > 7 else "") - return gt - - -SOLVED = ("SAT", "UNSAT") - - -def main(): - ap = argparse.ArgumentParser() - ap.add_argument("run_summary") - ap.add_argument("--baseline", default=os.path.join(SCRIPT_DIR, "probe_baseline.csv")) - ap.add_argument("--frozen", default=os.path.join(SCRIPT_DIR, "baseline.csv")) - args = ap.parse_args() - - base = load_summary(args.baseline) - run = load_summary(args.run_summary) - gt = load_ground_truth(args.frozen) - - rows = [] - flips = [] # (name, base_result, run_result, kind) - regressions = [] # (name, ratio) - exceptional = [] # (name, ratio) - sum_base = sum_run = 0.0 - - for name, b in sorted(base.items()): - r = run.get(name) - if r is None: - rows.append((name, b["result"], "MISSING", b["time"], None, None)) - continue - pb = par2_time(b["result"], b["time"]) - pr = par2_time(r["result"], r["time"]) - sum_base += pb - sum_run += pr - ratio = pr / pb if pb else None - - # correctness flip: SAT<->UNSAT between baseline and run, or a solved - # result that now contradicts ground_truth. - kind = None - if b["result"] in SOLVED and r["result"] in SOLVED and b["result"] != r["result"]: - kind = f"BASELINE-FLIP {b['result']}->{r['result']}" - g = gt.get(name, "") - if g in SOLVED and r["result"] in SOLVED and r["result"] != g: - kind = (kind + "; " if kind else "") + f"CONTRADICTS-GT (gt={g})" - if kind: - flips.append((name, b["result"], r["result"], kind)) - - if ratio is not None and r["result"] in SOLVED and b["result"] in SOLVED: - if ratio > REGRESSION_RATIO: - regressions.append((name, ratio)) - elif ratio < EXCEPTIONAL_RATIO: - exceptional.append((name, ratio)) - rows.append((name, b["result"], r["result"], b["time"], r["time"], ratio)) - - net = sum_run / sum_base if sum_base else None - - print(f"{'benchmark':62s} {'base':6s} {'run':6s} {'base_s':>8s} {'run_s':>8s} {'ratio':>6s}") - for name, br, rr, bt, rt, ratio in rows: - bt_s = f"{bt:8.2f}" if bt is not None else " n/a" - rt_s = f"{rt:8.2f}" if rt is not None else " n/a" - rr_s = f"{ratio:6.2f}" if ratio is not None else " n/a" - flag = "" - if ratio is not None and rr in SOLVED and br in SOLVED: - if ratio > REGRESSION_RATIO: flag = " REGRESSION" - elif ratio < EXCEPTIONAL_RATIO: flag = " exceptional" - if br != rr: flag += " " - print(f"{name[:62]:62s} {br:6s} {rr:6s} {bt_s} {rt_s} {rr_s}{flag}") - - print("\n" + "=" * 72) - if flips: - print("*** CORRECTNESS FLIPS (HALT) ***") - for name, br, rr, kind in flips: - print(f" {name}: {kind}") - else: - print("No correctness flips.") - print(f"net PAR2 ratio (run/base): {net:.3f}" if net else "net PAR2: n/a") - if net is not None: - pct = (1 - net) * 100 - verb = "FASTER" if pct >= 0 else "SLOWER" - print(f" -> {abs(pct):.1f}% {verb} overall") - print(f"regressions (>1.5x): {len(regressions)} {[f'{n}:{r:.2f}' for n,r in regressions]}") - print(f"exceptional (<0.6x): {len(exceptional)} {[f'{n}:{r:.2f}' for n,r in exceptional]}") - - # exit non-zero on any correctness flip so callers can gate on it. - sys.exit(2 if flips else 0) - - -if __name__ == "__main__": - main() diff --git a/benchmark/probe_fast.tsv b/benchmark/probe_fast.tsv deleted file mode 100644 index 41ca14d44..000000000 --- a/benchmark/probe_fast.tsv +++ /dev/null @@ -1,16 +0,0 @@ -tacas_c2e2_0hz_k4_50000.0clkhz_uniform_OR_sigmoid.hyxml_SAT.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/VNAMSCwI_satoct11/rolled/0hz_k4_50000.0clkhz_uniform_OR_sigmoid.hyxml_SAT.drh.o.smt2 -tacas_c2e2_0hz_k10_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/VNAMSCwI_satoct11/rolled/0hz_k10_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o.smt2 -tacas_c2e2_0hz_k112_20000.0clkhz_hybrid_inverter_sigmoid.hyxml_UNS.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/VNAMSCwI_satoct11/rolled/0hz_k112_20000.0clkhz_hybrid_inverter_sigmoid.hyxml_UNS.drh.o.smt2 -tacas_c2e2_0hz_k14_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/VNAMSCwI_satoct11/rolled/0hz_k14_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o.smt2 -tacas_c2e2_0hz_k16_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/VNAMSCwI_satoct11/rolled/0hz_k16_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o.smt2 -tacas_c2e2_0hz_k12_50000.0clkhz_uniform_NOR_ramp.hyxml_SAT.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/VNAMSCwI_satoct11/rolled/0hz_k12_50000.0clkhz_uniform_NOR_ramp.hyxml_SAT.drh.o.smt2 -tacas_c2e2_0hz_k17_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/VNAMSCwI_satoct11/rolled/0hz_k17_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o.smt2 -1mhz_k70_saradc_3b_nonlinear_10a_15e.smt2 /Users/kunalsheth/Documents/new_dreal/AMS-verification-bundle-of-sticks/saradc/rolled/1mhz_k70_saradc_3b_nonlinear_10a_15e.smt2 -1mhz_k72_saradc_4b_nonlinear_8a_30e.smt2 /Users/kunalsheth/Documents/new_dreal/AMS-verification-bundle-of-sticks/saradc/rolled/1mhz_k72_saradc_4b_nonlinear_8a_30e.smt2 -1mhz_k28_saradc_3b_box_4a_-1e.smt2 /Users/kunalsheth/Documents/new_dreal/AMS-verification-bundle-of-sticks/saradc/rolled/1mhz_k28_saradc_3b_box_4a_-1e.smt2 -1mhz_k20_saradc_2b_box_4a_-1e.smt2 /Users/kunalsheth/Documents/new_dreal/AMS-verification-bundle-of-sticks/saradc/rolled/1mhz_k20_saradc_2b_box_4a_-1e.smt2 -1mhz_k40_saradc_2b_box_8a_-1e.smt2 /Users/kunalsheth/Documents/new_dreal/AMS-verification-bundle-of-sticks/saradc/rolled/1mhz_k40_saradc_2b_box_8a_-1e.smt2 -github_oct5_0hz_k64_cardomain_car-9-flat-nonlinear.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/drealgithub_sunoct5/rolled/0hz_k64_cardomain_car-9-flat-nonlinear.drh.o.smt2 -github_oct5_0hz_k2_prostate_prostate_h2.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/drealgithub_sunoct5/rolled/0hz_k2_prostate_prostate_h2.drh.o.smt2 -github_oct5_0hz_k2048_atrial_fibrillation_new_cardiac_stim.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/drealgithub_sunoct5/rolled/0hz_k2048_atrial_fibrillation_new_cardiac_stim.drh.o.smt2 -github_oct5_0hz_k64_cardomain_car-7-flat-nonlinear.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/drealgithub_sunoct5/rolled/0hz_k64_cardomain_car-7-flat-nonlinear.drh.o.smt2 diff --git a/benchmark/probe_odes.tsv b/benchmark/probe_odes.tsv index a41955b09..dff950038 100644 --- a/benchmark/probe_odes.tsv +++ b/benchmark/probe_odes.tsv @@ -1,18 +1,18 @@ -tacas_c2e2_0hz_k4_50000.0clkhz_uniform_OR_sigmoid.hyxml_SAT.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/VNAMSCwI_satoct11/rolled/0hz_k4_50000.0clkhz_uniform_OR_sigmoid.hyxml_SAT.drh.o.smt2 -tacas_c2e2_0hz_k10_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/VNAMSCwI_satoct11/rolled/0hz_k10_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o.smt2 -tacas_c2e2_0hz_k112_20000.0clkhz_hybrid_inverter_sigmoid.hyxml_UNS.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/VNAMSCwI_satoct11/rolled/0hz_k112_20000.0clkhz_hybrid_inverter_sigmoid.hyxml_UNS.drh.o.smt2 +tacas_c2e2_0hz_k11_10000.0clkhz_uniform_inverter_ramp.hyxml_SAT.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/VNAMSCwI_satoct11/rolled/0hz_k11_10000.0clkhz_uniform_inverter_ramp.hyxml_SAT.drh.o.smt2 tacas_c2e2_0hz_k13_10000.0clkhz_uniform_inverter_sigmoid.hyxml_SAT.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/VNAMSCwI_satoct11/rolled/0hz_k13_10000.0clkhz_uniform_inverter_sigmoid.hyxml_SAT.drh.o.smt2 -tacas_c2e2_0hz_k14_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/VNAMSCwI_satoct11/rolled/0hz_k14_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o.smt2 -tacas_c2e2_0hz_k16_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/VNAMSCwI_satoct11/rolled/0hz_k16_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o.smt2 -tacas_c2e2_0hz_k12_50000.0clkhz_uniform_NOR_ramp.hyxml_SAT.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/VNAMSCwI_satoct11/rolled/0hz_k12_50000.0clkhz_uniform_NOR_ramp.hyxml_SAT.drh.o.smt2 tacas_c2e2_0hz_k17_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/VNAMSCwI_satoct11/rolled/0hz_k17_50000.0clkhz_uniform_NOR__sigmoid.hyxml_SAT.drh.o.smt2 -1mhz_k70_saradc_3b_nonlinear_10a_15e.smt2 /Users/kunalsheth/Documents/new_dreal/AMS-verification-bundle-of-sticks/saradc/rolled/1mhz_k70_saradc_3b_nonlinear_10a_15e.smt2 -1mhz_k72_saradc_4b_nonlinear_8a_30e.smt2 /Users/kunalsheth/Documents/new_dreal/AMS-verification-bundle-of-sticks/saradc/rolled/1mhz_k72_saradc_4b_nonlinear_8a_30e.smt2 -1mhz_k28_saradc_3b_box_4a_-1e.smt2 /Users/kunalsheth/Documents/new_dreal/AMS-verification-bundle-of-sticks/saradc/rolled/1mhz_k28_saradc_3b_box_4a_-1e.smt2 -1mhz_k20_saradc_2b_box_4a_-1e.smt2 /Users/kunalsheth/Documents/new_dreal/AMS-verification-bundle-of-sticks/saradc/rolled/1mhz_k20_saradc_2b_box_4a_-1e.smt2 -1mhz_k40_saradc_2b_box_8a_-1e.smt2 /Users/kunalsheth/Documents/new_dreal/AMS-verification-bundle-of-sticks/saradc/rolled/1mhz_k40_saradc_2b_box_8a_-1e.smt2 -github_oct5_0hz_k64_cardomain_car-9-flat-nonlinear.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/drealgithub_sunoct5/rolled/0hz_k64_cardomain_car-9-flat-nonlinear.drh.o.smt2 +tacas_c2e2_0hz_k112_20000.0clkhz_hybrid_inverter_sigmoid.hyxml_UNS.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/VNAMSCwI_satoct11/rolled/0hz_k112_20000.0clkhz_hybrid_inverter_sigmoid.hyxml_UNS.drh.o.smt2 +tacas_c2e2_0hz_k12_50000.0clkhz_uniform_OR_sigmoid.hyxml_UNS.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/VNAMSCwI_satoct11/rolled/0hz_k12_50000.0clkhz_uniform_OR_sigmoid.hyxml_UNS.drh.o.smt2 github_oct5_0hz_k2_prostate_prostate_h2.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/drealgithub_sunoct5/rolled/0hz_k2_prostate_prostate_h2.drh.o.smt2 +github_oct5_0hz_k2_prostate_cancer_scaled_prostate_infix.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/drealgithub_sunoct5/rolled/0hz_k2_prostate_cancer_scaled_prostate_infix.drh.o.smt2 +github_oct5_0hz_k256_thermostat_thermostat-double-network-sat.drh.n.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/drealgithub_sunoct5/rolled/0hz_k256_thermostat_thermostat-double-network-sat.drh.n.smt2 github_oct5_0hz_k128_quad_quad2-1.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/drealgithub_sunoct5/rolled/0hz_k128_quad_quad2-1.drh.o.smt2 +github_oct5_0hz_k16_crazyflie_stabilizer.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/drealgithub_sunoct5/rolled/0hz_k16_crazyflie_stabilizer.drh.o.smt2 github_oct5_0hz_k2048_atrial_fibrillation_new_cardiac_stim.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/drealgithub_sunoct5/rolled/0hz_k2048_atrial_fibrillation_new_cardiac_stim.drh.o.smt2 -github_oct5_0hz_k64_cardomain_car-7-flat-nonlinear.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/drealgithub_sunoct5/rolled/0hz_k64_cardomain_car-7-flat-nonlinear.drh.o.smt2 +github_oct5_0hz_k128_water_water-double-network.drh.n.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/drealgithub_sunoct5/rolled/0hz_k128_water_water-double-network.drh.n.smt2 +github_oct5_0hz_k256_glucose_control_large_variance.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/drealgithub_sunoct5/rolled/0hz_k256_glucose_control_large_variance.drh.o.smt2 +1mhz_k20_saradc_2b_box_4a_1e.smt2 /Users/kunalsheth/Documents/new_dreal/AMS-verification-bundle-of-sticks/saradc/rolled/1mhz_k20_saradc_2b_box_4a_1e.smt2 +1mhz_k70_saradc_3b_nonlinear_10a_14e.smt2 /Users/kunalsheth/Documents/new_dreal/AMS-verification-bundle-of-sticks/saradc/rolled/1mhz_k70_saradc_3b_nonlinear_10a_14e.smt2 +1mhz_k72_saradc_4b_nonlinear_8a_30e.smt2 /Users/kunalsheth/Documents/new_dreal/AMS-verification-bundle-of-sticks/saradc/rolled/1mhz_k72_saradc_4b_nonlinear_8a_30e.smt2 +1mhz_k40_saradc_2b_box_8a_-1e.smt2 /Users/kunalsheth/Documents/new_dreal/AMS-verification-bundle-of-sticks/saradc/rolled/1mhz_k40_saradc_2b_box_8a_-1e.smt2 +tacas_c2e2_0hz_k10_50000.0clkhz_uniform_OR_sigmoid.hyxml_SAT.drh.o.smt2 /Users/kunalsheth/Documents/new_dreal/nraode_to_nra/VNAMSCwI_satoct11/rolled/0hz_k10_50000.0clkhz_uniform_OR_sigmoid.hyxml_SAT.drh.o.smt2 diff --git a/benchmark/run_batch.sh b/benchmark/run_batch.sh index fdebd4560..16cd0a09f 100755 --- a/benchmark/run_batch.sh +++ b/benchmark/run_batch.sh @@ -1,11 +1,24 @@ #!/usr/bin/env bash # Usage: run_batch.sh [jobs_file] # Reads TSV pairs (csv_name filepath) from stdin or jobs_file, one per line. -# Runs each benchmark in parallel with gtime -v and a 300s timeout. +# Runs each benchmark in parallel with gtime -v, nice -n 1, and a 600s timeout. +# Timing metric is CPU time (User+System) from gtime, not wall clock — the +# machine is multi-tenant, so wall clock is noisy; `timeout` stays wall-clock. # Outputs per-benchmark using csv_name (minus .smt2) as the label: #