Struct VerificationContext 

pub struct VerificationContext { /* private fields */ }

A verification context for building constraints incrementally.

Provides direct access to Z3 types for constructing custom proofs. For most use cases, prefer VerificationSession which works with the higher-level VerifyExpr IR.

Implementations

impl VerificationContext

pub fn solver(&self) -> Solver

Create a new solver for this context.

The solver accumulates assertions and can check their satisfiability.

pub fn bool_val(&self, value: bool) -> Bool

Create a boolean constant.

pub fn int_val(&self, value: i64) -> Int

Create an integer constant.

pub fn bool_var(&self, name: &str) -> Bool

Create a named boolean variable.

pub fn int_var(&self, name: &str) -> Int

Create a named integer variable.

pub fn check_valid( &self, solver: &Solver, assertion: &Bool, ) -> VerificationResult

Check if an assertion is valid (always true).

Uses the standard validity check: P is valid iff ¬P is unsatisfiable. The solver state is preserved using push/pop.