feat(symbolic): show query progress

crates/evm/symbolic/src/executor.rs

@@ -28,6 +28,11 @@ impl SymbolicExecutor {
         self.solver.take_diagnostics()
     }
 
+    /// Registers a callback invoked after each solver query for live progress rendering.
+    pub fn set_query_observer(&mut self, observer: impl Fn(usize) + Send + Sync + 'static) {
+        self.solver.set_query_observer(Some(Box::new(observer)));
+    }
+
     /// 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/runtime/solver.rs

@@ -47,6 +47,8 @@ impl fmt::Display for SolverOutcome {
     }
 }
 
+pub(crate) type QueryObserver = Box<dyn Fn(usize) + Send + Sync + 'static>;
+
 /// Minimal solver backend interface used by the symbolic executor.
 ///
 /// Implementations are responsible for translating accumulated symbolic constraints
@@ -57,6 +59,9 @@ pub(crate) trait SymbolicSolver {
     /// Returns solver counters collected by this backend.
     fn stats(&self) -> SymbolicStats;
 
+    /// Registers a callback invoked after each logical solver query is reserved.
+    fn set_query_observer(&mut self, observer: Option<QueryObserver>);
+
     /// Returns aggregate staged-portfolio diagnostics collected by this backend.
     fn portfolio_diagnostics(&self) -> Option<&PortfolioDiagnostics>;
 
@@ -115,6 +120,7 @@ pub(crate) struct SmtLibSubprocessSolver {
     pub(crate) timeout: Option<u32>,
     pub(crate) max_queries: usize,
     pub(crate) queries: usize,
+    query_observer: Option<QueryObserver>,
     pub(crate) dump_smt: bool,
     portfolio_diagnostics: PortfolioDiagnostics,
     captured_diagnostics: Option<String>,
@@ -133,6 +139,7 @@ impl SmtLibSubprocessSolver {
             timeout,
             max_queries,
             queries: 0,
+            query_observer: None,
             dump_smt,
             portfolio_diagnostics: PortfolioDiagnostics::default(),
             captured_diagnostics: None,
@@ -156,6 +163,11 @@ impl SymbolicSolver for SmtLibSubprocessSolver {
         SymbolicStats { paths: 0, solver_queries: self.queries }
     }
 
+    /// Registers a live query observer for progress rendering.
+    fn set_query_observer(&mut self, observer: Option<QueryObserver>) {
+        self.query_observer = observer;
+    }
+
     /// Returns staged-portfolio diagnostics collected by this solver.
     fn portfolio_diagnostics(&self) -> Option<&PortfolioDiagnostics> {
         (!self.portfolio_diagnostics.is_empty()).then_some(&self.portfolio_diagnostics)
@@ -194,7 +206,7 @@ impl SymbolicSolver for SmtLibSubprocessSolver {
     /// Returns whether `is_sat` holds.
     fn is_sat(&mut self, constraints: &[BoolExpr]) -> Result<bool, SymbolicError> {
         self.reserve_query()?;
-        self.queries += 1;
+        self.record_query();
         if constraints_prefer_fallback_first(constraints)
             && fallback_single_var_model(constraints).is_some()
         {
@@ -214,7 +226,7 @@ impl SymbolicSolver for SmtLibSubprocessSolver {
     /// Implements the `model` solver helper.
     fn model(&mut self, constraints: &[BoolExpr]) -> Result<BTreeMap<String, U256>, SymbolicError> {
         self.reserve_query()?;
-        self.queries += 1;
+        self.record_query();
         if constraints_prefer_fallback_first(constraints)
             && let Some(model) = fallback_single_var_model(constraints)
         {
@@ -255,6 +267,14 @@ impl SmtLibSubprocessSolver {
         Ok(())
     }
 
+    /// Records one logical solver query and notifies the live observer, if any.
+    fn record_query(&mut self) {
+        self.queries += 1;
+        if let Some(observer) = &self.query_observer {
+            observer(self.queries);
+        }
+    }
+
     /// Implements the `query` solver helper.
     pub(crate) fn query(
         &mut self,

crates/forge/src/progress.rs

@@ -90,6 +90,31 @@ impl TestsProgressState {
         }
     }
 
+    /// Creates progress entry for symbolic tests.
+    pub fn start_symbolic_progress(
+        &mut self,
+        suite_name: &str,
+        test_name: &str,
+        max_queries: u32,
+    ) -> Option<ProgressBar> {
+        if let Some(suite_progress) = self.suites_progress.get(suite_name) {
+            let symbolic_progress =
+                self.multi.insert_after(suite_progress, ProgressBar::new(max_queries as u64));
+            symbolic_progress.set_style(
+                indicatif::ProgressStyle::with_template(
+                    "    ↪ {prefix:.bold.dim}: [{pos}/{len}] SMT queries {msg}",
+                )
+                .unwrap()
+                .tick_chars("⠁⠂⠄⡀⢀⠠⠐⠈ "),
+            );
+            symbolic_progress.set_prefix(test_name.to_owned());
+            symbolic_progress.enable_steady_tick(Duration::from_millis(100));
+            Some(symbolic_progress)
+        } else {
+            None
+        }
+    }
+
     /// Removes overall test progress.
     pub fn clear(&mut self) {
         self.multi.clear().unwrap();
@@ -122,3 +147,17 @@ pub fn start_fuzz_progress(
         None
     }
 }
+
+/// Helper function for creating symbolic test progress bar.
+pub fn start_symbolic_progress(
+    tests_progress: Option<&TestsProgress>,
+    suite_name: &str,
+    test_name: &str,
+    max_queries: u32,
+) -> Option<ProgressBar> {
+    if let Some(progress) = tests_progress {
+        progress.inner.lock().start_symbolic_progress(suite_name, test_name, max_queries)
+    } else {
+        None
+    }
+}

crates/forge/src/runner.rs

@@ -5,7 +5,7 @@ use crate::{
     coverage::HitMaps,
     fuzz::{BaseCounterExample, FuzzTestResult},
     multi_runner::{TestContract, TestRunnerConfig},
-    progress::{TestsProgress, start_fuzz_progress},
+    progress::{TestsProgress, start_fuzz_progress, start_symbolic_progress},
     result::{InvariantFailure, SuiteResult, TestResult, TestSetup},
 };
 use alloy_dyn_abi::{DynSolValue, JsonAbiExt};
@@ -749,6 +749,16 @@ impl<'a, FEN: FoundryEvmNetwork> FunctionRunner<'a, FEN> {
         if self.should_defer_symbolic_diagnostics() {
             symbolic.capture_diagnostics();
         }
+        let progress = start_symbolic_progress(
+            self.cr.progress,
+            self.cr.name,
+            &func.name,
+            self.config.symbolic.max_solver_queries,
+        );
+        if let Some(progress) = progress.as_ref() {
+            let progress = progress.clone();
+            symbolic.set_query_observer(move |queries| progress.set_position(queries as u64));
+        }
         let result = symbolic.run(SymbolicRunInput {
             executor: self.executor.as_ref(),
             target: self.address,
@@ -757,6 +767,9 @@ impl<'a, FEN: FoundryEvmNetwork> FunctionRunner<'a, FEN> {
             value: U256::ZERO,
             ffi_enabled: self.config.ffi,
         });
+        if let Some(progress) = progress {
+            progress.finish_and_clear();
+        }
         let portfolio_diagnostics = symbolic.portfolio_diagnostics();
         let symbolic_diagnostics = symbolic.take_diagnostics();
 
@@ -901,6 +914,16 @@ impl<'a, FEN: FoundryEvmNetwork> FunctionRunner<'a, FEN> {
         if self.should_defer_symbolic_diagnostics() {
             symbolic.capture_diagnostics();
         }
+        let progress = start_symbolic_progress(
+            self.cr.progress,
+            self.cr.name,
+            &func.name,
+            self.config.symbolic.max_solver_queries,
+        );
+        if let Some(progress) = progress.as_ref() {
+            let progress = progress.clone();
+            symbolic.set_query_observer(move |queries| progress.set_position(queries as u64));
+        }
         let result = symbolic.run_invariant(SymbolicInvariantRunInput {
             executor: self.executor.as_ref(),
             invariant_address: self.address,
@@ -913,6 +936,9 @@ impl<'a, FEN: FoundryEvmNetwork> FunctionRunner<'a, FEN> {
             fail_on_revert,
             ffi_enabled: self.config.ffi,
         });
+        if let Some(progress) = progress {
+            progress.finish_and_clear();
+        }
         let portfolio_diagnostics = symbolic.portfolio_diagnostics();
         let symbolic_diagnostics = symbolic.take_diagnostics();