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,
        cx: &mut SymCx,
        constraints: &[SymBoolExpr],
    ) -> Result<bool, SymbolicError>;
    fn model(
        &mut self,
        cx: &mut SymCx,
        constraints: &[SymBoolExpr],
    ) -> Result<HashMap<Symbol, U256>, SymbolicError>;

    // Provided methods
    fn clear_context_caches(&mut self) { ... }
    fn heuristic_witnesses(&self) -> usize { ... }
    fn is_sat_branch(
        &mut self,
        cx: &mut SymCx,
        constraints: &[SymBoolExpr],
    ) -> Result<bool, SymbolicError> { ... }
}
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, cx: &mut SymCx, constraints: &[SymBoolExpr], ) -> 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, cx: &mut SymCx, constraints: &[SymBoolExpr], ) -> Result<HashMap<Symbol, 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 clear_context_caches(&mut self)

Clears cached expression keys tied to a previous symbolic context.

Source

fn heuristic_witnesses(&self) -> usize

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

Source

fn is_sat_branch( &mut self, cx: &mut SymCx, constraints: &[SymBoolExpr], ) -> Result<bool, SymbolicError>

Returns branch satisfiability, allowing branch-only hard-arithmetic shortcuts.

Dyn Compatibility§

This trait is dyn compatible.

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

Implementors§