Skip to main content

SymbolicSolver

foundry_evm_symbolic::runtime::solver

Trait SymbolicSolver 

Source 
pub(crate) trait SymbolicSolver {
    // Required methods
    fn stats(&self) -> SymbolicStats;
    fn set_query_observer(
        &mut self,
        observer: Option<Box<dyn Fn(usize) + Send + Sync + 'static>>,
    );
    fn portfolio_diagnostics(&self) -> Option<&PortfolioDiagnostics>;
    fn capture_diagnostics(&mut self);
    fn take_diagnostics(&mut self) -> Option<String>;
    fn check_available(&self) -> Result<(), SymbolicError>;
    fn is_sat(
        &mut self,
        constraints: &[BoolExpr],
    ) -> Result<bool, SymbolicError>;
    fn model(
        &mut self,
        constraints: &[BoolExpr],
    ) -> Result<BTreeMap<String, U256>, SymbolicError>;

    // Provided method
    fn heuristic_witnesses(&self) -> usize { ... }
}
Expand description

Minimal solver backend interface used by the symbolic executor.

Implementations are responsible for translating accumulated symbolic constraints into solver queries, enforcing query budgets, and extracting concrete model values for counterexample replay. The trait is intentionally small so alternate SMT backends can be added without changing the executor entrypoints.

Required Methods§

Source

fn stats(&self) -> SymbolicStats

Returns solver counters collected by this backend.

Source

fn set_query_observer( &mut self, observer: Option<Box<dyn Fn(usize) + Send + Sync + 'static>>, )

Registers a callback invoked after each logical solver query is reserved.

Source

fn portfolio_diagnostics(&self) -> Option<&PortfolioDiagnostics>

Returns aggregate staged-portfolio diagnostics collected by this backend.

Source

fn capture_diagnostics(&mut self)

Captures verbose diagnostics for later rendering instead of writing them live.

Source

fn take_diagnostics(&mut self) -> Option<String>

Takes any captured verbose diagnostics collected by this backend.

Source

fn check_available(&self) -> Result<(), SymbolicError>

Verifies that the configured solver can be invoked before exploration starts.

Backends should keep this check lightweight and return a SymbolicError with a stable stop reason when the solver executable or service is unavailable.

Source

fn is_sat(&mut self, constraints: &[BoolExpr]) -> Result<bool, SymbolicError>

Returns whether the supplied path constraints are satisfiable.

Implementations should count this as one solver query and map solver unknown or timeout responses into SymbolicError::SolverUnknown or SymbolicError::Solver, as appropriate.

Source

fn model( &mut self, constraints: &[BoolExpr], ) -> Result<BTreeMap<String, U256>, SymbolicError>

Returns a concrete model for all symbolic variables constrained by the path.

The executor uses the returned variable assignments to materialize ABI arguments, calldata, and invariant sequences for concrete replay.

Provided Methods§

Source

fn heuristic_witnesses(&self) -> usize

Returns the number of satisfiable witnesses produced by local hard-arithmetic search.

Dyn Compatibility§

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors§