Struct Btor2ChannelPropertyObservabilityTool 

pub struct Btor2ChannelPropertyObservabilityTool { /* private fields */ }

Additive phase-observed client for BTOR2 channel-property CLI v1.

Implementations

impl Btor2ChannelPropertyObservabilityTool

pub fn capabilities(&self) -> &Btor2ChannelPropertyObservabilityCapabilities

pub fn execution_policy(&self) -> ExecutionPolicy

pub fn with_execution_policy(self, policy: ExecutionPolicy) -> Self

pub fn certify( &self, files: &Btor2ChannelPropertyFiles<'_>, artifact: &Path, ) -> Result<Btor2ChannelPropertyPhaseObservedSummary, PredicateApiError>

pub fn certify_observed( &self, files: &Btor2ChannelPropertyFiles<'_>, artifact: &Path, ) -> Result<Observed<Btor2ChannelPropertyPhaseObservedSummary>, PredicateOperationError>

pub fn verify( &self, files: &Btor2ChannelPropertyFiles<'_>, artifact: &Path, ) -> Result<Btor2ChannelPropertyPhaseObservedSummary, PredicateApiError>

pub fn verify_observed( &self, files: &Btor2ChannelPropertyFiles<'_>, artifact: &Path, ) -> Result<Observed<Btor2ChannelPropertyPhaseObservedSummary>, PredicateOperationError>

Trait Implementations

impl Clone for Btor2ChannelPropertyObservabilityTool

fn clone(&self) -> Btor2ChannelPropertyObservabilityTool

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Btor2ChannelPropertyObservabilityTool

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.