Feature/solver profiler impl

README.md

@@ -8,6 +8,7 @@ Get the most out of SMT solving with KSMT features:
 * Utilities to [simplify and transform](#utilities-to-simplify-and-transform-expressions) your expressions
 * Switching between solvers and support for [portfolio mode](#using-multiple-solvers--portfolio-mode-)
 * Running solvers in a [separate process](#running-solvers-in-separate-processes) to reduce timeout-related crashes
+* Observation-only contracts for profiling incremental solver workloads through the optional [`ksmt-profiling`](docs/solver-profiling.md) module
 * Streamlined [solver delivery](#ksmt-distribution) with no need for building a solver or implementing JVM bindings
 
 [![KSMT: build](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml/badge.svg)](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml)

docs/solver-profiling.md

@@ -0,0 +1,58 @@
+# Solver workload profiling contracts
+
+The optional `ksmt-profiling` module defines an observation-only, interface
+boundary for incremental solver workloads. It does not contain a profiler
+implementation, configuration recommender, model training, configuration
+search, ONNX Runtime, or a model.
+
+## Profile model
+
+`KSolverProfile` describes one solver session from profiler construction
+through the corresponding solver `close` call. A snapshot may be taken while
+the session is still active:
+
+- stable profile/run identifiers and session state;
+- solver name, version, and attributes;
+- native-default or unknown base configuration plus observed overrides;
+- ordered solver events timed with `kotlin.time.Duration`;
+- asserted KSMT formulas and per-check assumptions;
+- `push` and `pop` operations needed to reconstruct the active formula;
+- check timeout and status, plus explicit access to a backend-specific reason
+  for `UNKNOWN`;
+- active and total assertion counts, task context, and failures.
+
+Failed solver calls are retained because a profile is an observation and must
+not silently rewrite workload history. They are not configurations to tune.
+Result-access events explicitly reference the check that produced the accessed
+result when such a check exists.
+
+Configuration values are observational data only. The initial snapshot is
+needed to determine whether a workload can be reproduced from native defaults;
+it is not a recommendation. KSMT does not define patch
+application, recommendation decisions, or a tuner lifecycle.
+
+Expressions stay as in-memory `KExpr<KBoolSort>` objects. Serializing formulas
+or producing consumer-specific feature tensors is intentionally outside the
+KSMT contract.
+
+## Extension point
+
+`KSolverProfilerFactory` wraps an existing solver using explicit session IDs,
+solver metadata, initial configuration, attributes, and an event limit.
+`KSolverProfiler<Config>` extends `KSolver<Config>` and specifies the future
+transparent decorator. It exposes a structurally independent `snapshot` and
+optional application task context. Recording may continue after a snapshot,
+but the returned collections must remain stable. Profiling must not turn a
+successful delegate call into a failure. KSMT does not yet provide an
+implementation.
+
+The event limit bounds retained AST references. A profile retains the ordered
+event prefix up to that limit, continues forwarding every solver call, and
+increments `droppedEventCount` for each later event. Session state and observed
+duration continue to advance. Consumers must treat `isTruncated` profiles as
+ineligible for exact replay.
+
+Consumers may use a profile for diagnostics, benchmarking, or external tuning,
+but those policies and their output types belong to the consumer. In
+particular, cvc5 option whitelists, configuration patches, feature projection,
+ONNX adapters, decoding, and fallback do not belong in KSMT.

ksmt-profiling/README.md

@@ -0,0 +1,115 @@
+# ksmt-profiling
+
+Solver-agnostic profiling for KSMT. The module records the chronology of calls made to a
+`KSolver` (`configure`, `assert`, `push`, `pop`, `check`, `model`, `unsatCore`, ...) and exposes it
+as an immutable `KSolverProfile`.
+
+`KRecordingSolverProfiler` is the implementation. It wraps any `KSolver` and does not depend on a
+specific solver. cvc5 is the primary target.
+
+## Requirements
+
+- JDK 17 (the version the module was built and tested with).
+- No separate Gradle installation: use the `gradlew` wrapper from the repository root.
+- Internet access on the first build to download dependencies.
+- No cvc5 build is needed. The cvc5 jar and native libraries are stored in `ksmt-cvc5/dist`.
+  See [`ksmt-cvc5/dist/build.md`](../ksmt-cvc5/dist/build.md) for their origin.
+
+Make sure `JAVA_HOME` points to JDK 17. Run all commands from the repository root.
+
+| OS | Wrapper |
+| --- | --- |
+| Linux / macOS | `./gradlew` |
+| Windows (PowerShell) | `.\gradlew.bat` |
+
+The examples below use `./gradlew`.
+
+## Build and test
+
+```bash
+# Compile the module
+./gradlew :ksmt-profiling:build
+
+# Unit tests and static analysis
+./gradlew :ksmt-profiling:test :ksmt-profiling:detekt
+```
+
+Expected result: `BUILD SUCCESSFUL`, 20 unit tests pass, 2 benchmark tests are skipped.
+
+Test reports are written to `ksmt-profiling/build/test-results/test/`. If Gradle reports
+`UP-TO-DATE` and does not run the tests again, add `:ksmt-profiling:cleanTest` before
+`:ksmt-profiling:test`.
+
+## Usage
+
+```kotlin
+val solver = KCvc5Solver(ctx)
+val profiler = KRecordingSolverProfiler(
+    delegate = solver,
+    solver = KSolverDescriptor(name = "cvc5"),
+    maxRecordedEvents = 1_000_000,
+)
+
+profiler.push()
+profiler.assert(formula)
+profiler.check()
+profiler.pop(1u)
+
+val profile = profiler.snapshot() // immutable chronology of the calls
+profiler.close()
+```
+
+Use the profiler as a regular `KSolver`. Notes:
+
+- Exceptions thrown by the wrapped solver are rethrown as the same object and are recorded in the
+  profile.
+- `configure` is recorded as an opaque event (`overrides = null`) because the contents of the
+  lambda cannot be inspected. Options that must be visible in the profile should be passed through
+  `KSolverProfilerRequest.initialConfiguration`.
+- Events are stored in strict order. When `maxRecordedEvents` is reached, the profile keeps the
+  first events and reports that it was truncated.
+- `interrupt()` can be called from another thread while `check` is running.
+- `model`, `unsatCore` and `reasonOfUnknown` accesses are linked to the last successful check.
+
+## Overhead benchmark
+
+`ProfilerOverheadBenchmark` compares a bare cvc5 solver with the same solver under the profiler
+and estimates memory per recorded event. It is **disabled by default** so that it does not slow
+down regular test runs. Enable it with the environment variable `KSMT_PROFILING_BENCHMARK=true`.
+
+```bash
+# Linux / macOS
+KSMT_PROFILING_BENCHMARK=true ./gradlew :ksmt-profiling:cleanTest :ksmt-profiling:test \
+    --tests "*ProfilerOverheadBenchmark*"
+```
+
+```powershell
+# Windows (PowerShell)
+$env:KSMT_PROFILING_BENCHMARK = 'true'
+.\gradlew.bat :ksmt-profiling:cleanTest :ksmt-profiling:test --tests "*ProfilerOverheadBenchmark*"
+Remove-Item Env:KSMT_PROFILING_BENCHMARK   # do not leave it enabled
+```
+
+Gradle does not print the test output by default. Add `-i` or read the `system-out` section of
+`ksmt-profiling/build/test-results/test/TEST-io.ksmt.profiling.ProfilerOverheadBenchmark.xml`.
+
+Reference numbers from one development machine (synthetic workload on cvc5, median of 7 runs):
+
+| Workload | Without profiler | With profiler |
+| --- | --- | --- |
+| 20 000 x `push/assert/pop` | 41.9 ms | 51.1 ms (x1.22) |
+| 2 000 x `push/assert/check/pop` | 94.6 ms | 109.1 ms (x1.15, high variance) |
+
+Memory: about 100 bytes per recorded event. Absolute numbers depend on the machine, so compare the
+two configurations only within a single run. The workload is synthetic and does not replace a
+measurement on real TSA workloads.
+
+## Known limitations
+
+- The overhead was not measured on real TSA workloads or with several threads.
+- Serialization of `KSolverProfile` is outside of KSMT.
+
+## Troubleshooting
+
+- **Gradle fails with a Java version error.** Check `JAVA_HOME` and `java -version`: JDK 17.
+- **The benchmark runs on every test run.** `KSMT_PROFILING_BENCHMARK` is still set in your shell.

ksmt-profiling/build.gradle.kts

@@ -0,0 +1,23 @@
+plugins {
+    id("io.ksmt.ksmt-base")
+}
+
+dependencies {
+    api(project(":ksmt-core"))
+
+    // cvc5 is the primary real solver; it is used only by the opt-in overhead benchmark.
+    testImplementation(project(":ksmt-cvc5:ksmt-cvc5-core"))
+    testImplementation(project(":ksmt-cvc5:ksmt-cvc5-native"))
+}
+
+publishing {
+    publications {
+        create<MavenPublication>("maven") {
+            from(components["java"])
+
+            addKsmtPom()
+            addSourcesAndJavadoc(project)
+            signKsmtPublication(project)
+        }
+    }
+}