Trait FiniteStateTransitionSystemProver 

pub trait FiniteStateTransitionSystemProver {
    // Required methods
    fn new(fin_state: &FiniteStateTransitionSystem) -> Self;
    fn prove(&mut self) -> ProofResult;
}

Required Methods

fn new(fin_state: &FiniteStateTransitionSystem) -> Self

fn prove(&mut self) -> ProofResult

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors

impl<T: StatefulSatSolver> FiniteStateTransitionSystemProver for IC3Stateful<T>

impl<T: StatefulSatSolver> FiniteStateTransitionSystemProver for PDR<T>

impl<T: StatelessSatSolver> FiniteStateTransitionSystemProver for IC3Stateless<T>