Struct CounterExampleGenerator 

pub struct CounterExampleGenerator { /* private fields */ }

Counter-example generator

Implementations

impl CounterExampleGenerator

pub fn new() -> Self

Create a new counterexample generator

pub fn with_limits( max_cex: usize, max_candidates: usize, max_time: Duration, ) -> Self

Create with custom limits

pub fn generate( &mut self, quantifier: &QuantifiedFormula, model: &CompletedModel, manager: &mut TermManager, ) -> Vec<CounterExample>

Generate counterexamples for a quantifier

pub fn set_generation_bound(&mut self, bound: u32)

Set generation bound for candidate selection

pub fn clear_cache(&mut self)

Clear the candidate cache

pub fn stats(&self) -> &CexStats

Get statistics

Trait Implementations

impl Debug for CounterExampleGenerator

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

Formats the value using the given formatter.

impl Default for CounterExampleGenerator

fn default() -> Self

Returns the “default value” for a type.