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, ) -> CexGenerationResult

Generate counterexamples for a quantifier.

Returns a CexGenerationResult containing the counterexamples found and a flag indicating whether all evaluations resolved to concrete booleans.

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

Set generation bound for candidate selection

pub fn inject_extra_candidates( &mut self, extras: &FxHashMap<SortId, Vec<TermId>>, )

Inject extra candidates from outside (e.g. Skolem function applications).

These are merged into the per-sort candidate cache so they appear in every subsequent build_candidate_lists call.

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.