Struct BoundedModelChecker 

pub struct BoundedModelChecker { /* private fields */ }

Bounded model checker for quantified formulas

Implementations

impl BoundedModelChecker

pub fn new() -> Self

Create a new bounded model checker

pub fn check( &mut self, _quantifiers: &[QuantifiedFormula], _model: &CompletedModel, _manager: &TermManager, ) -> CheckResult

Check if quantifiers are satisfiable within bound

pub fn increase_bound(&mut self)

Increment depth bound

pub fn at_max_depth(&self) -> bool

Check if at max depth

Trait Implementations

impl Debug for BoundedModelChecker

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

Formats the value using the given formatter.

impl Default for BoundedModelChecker

fn default() -> Self

Returns the “default value” for a type.