feat(symbolic): summarize portfolio diagnostics (#14849)

* feat(symbolic): summarize portfolio diagnostics

Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a
Co-authored-by: Amp <amp@ampcode.com>

* Address symbolic portfolio diagnostics review

Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694
Co-authored-by: Amp <amp@ampcode.com>

* Fix transaction request clippy warning

Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694
Co-authored-by: Amp <amp@ampcode.com>

* Revert "Fix transaction request clippy warning"

This reverts commit 884799d.

* Allow transaction request enum size lint

Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694
Co-authored-by: Amp <amp@ampcode.com>

* Disambiguate portfolio diagnostics re-export

Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694
Co-authored-by: Amp <amp@ampcode.com>

* Use enum for solver outcomes

Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694
Co-authored-by: Amp <amp@ampcode.com>

---------

Co-authored-by: Amp <amp@ampcode.com>

Author: figtracer

crates/evm/symbolic/README.md

@@ -231,7 +231,31 @@ For latency-sensitive local runs, start with a small portfolio such as
 can still use more CPU and be slower when one fast solver already handles most
 queries. `--symbolic-dump-smt` prints each solver's configured order and launch
 delay with the per-query portfolio outcomes so solver mixes can be compared
-without changing execution semantics.
+without changing execution semantics. It also prints an aggregate portfolio
+summary at the end of the run, for example:
+
+```text
+--- symbolic solver portfolio summary ---
+queries: 48
+solver runs: 64
+rescue solver runs: 0
+not-started solver runs: 32
+non-primary wins: 0
+rescue wins: 0
+cancelled after winner: 0
+invalid models: 0
+solver errors: 0
+winner counts:
+  yices-smt2 --bvconst-in-decimal: 48
+launch counts:
+  yices-smt2 --bvconst-in-decimal: 48
+  z3 -in -smt2: 16
+outcome counts:
+  not-started: 32
+  sat-valid: 32
+  unsat: 32
+```
+
 Forge warns when a configured portfolio is degraded because one or more solver
 entries are not available, but it still uses the entries that can be invoked.
 

crates/evm/symbolic/src/executor.rs

@@ -13,6 +13,11 @@ impl SymbolicExecutor {
         Self { config, solver: Box::new(solver) }
     }
 
+    /// Returns staged solver portfolio diagnostics collected by this executor.
+    pub fn portfolio_diagnostics(&self) -> Option<PortfolioDiagnostics> {
+        self.solver.portfolio_diagnostics().cloned()
+    }
+
     /// Executes one function symbolically against an already-deployed test contract.
     ///
     /// The input executor supplies the deployed bytecode, storage backend, caller, and

crates/evm/symbolic/src/lib.rs

@@ -55,7 +55,7 @@ mod abi;
 mod executor;
 mod runtime;
 
-pub use runtime::{SymbolicError, SymbolicRunInput};
+pub use runtime::{PortfolioDiagnostics, SymbolicError, SymbolicRunInput};
 
 /// Symbolic solver names with built-in command-line mappings.
 pub const BUILTIN_SYMBOLIC_SOLVERS: &[&str] =

crates/evm/symbolic/src/runtime.rs

@@ -19,7 +19,16 @@ pub(crate) use evm::*;
 pub(crate) use expressions::*;
 pub(crate) use memory::*;
 pub(crate) use precompiles::*;
-pub(crate) use solver::*;
+pub use solver::PortfolioDiagnostics;
+pub(crate) use solver::{
+    SmtLibSubprocessSolver, SymbolicSolver, solver_portfolio_availability_warning,
+};
+#[cfg(test)]
+pub(crate) use solver::{
+    SolverCommand, SolverOutcome, SolverRunSummary, fallback_single_var_model,
+    named_solver_command, parse_model, solver_commands_for_config, split_solver_command,
+    validate_solver_model_output,
+};
 pub(crate) use state::*;
 
 pub struct SymbolicRunInput<'a, FEN: FoundryEvmNetwork> {