Struct CounterExampleGuidedRefinement 

pub struct CounterExampleGuidedRefinement {
    pub domain: AbstractDomain,
    pub iterations: usize,
    pub verified: bool,
}

CEGAR loop: counterexample-guided abstraction refinement.

Fields

domain: AbstractDomain

Current abstract domain.

iterations: usize

Number of refinement iterations performed.

verified: bool

Whether a proof has been found.

Implementations

impl CounterExampleGuidedRefinement

pub fn new(domain: AbstractDomain) -> Self

Create a CEGAR instance with the given initial abstraction.

pub fn abstract_states(&self, states: &[usize]) -> AbstractDomain

Map concrete states to their abstract representation.

pub fn refine_abstraction(&mut self, spurious: &SpuriousCounterexample)

Refine the abstraction using a spurious counterexample.

pub fn check_feasibility(&self, cex: &CounterExample) -> bool

Check whether a counterexample is feasible (true = feasible, false = spurious).

Trait Implementations

impl Clone for CounterExampleGuidedRefinement

fn clone(&self) -> CounterExampleGuidedRefinement

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CounterExampleGuidedRefinement

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

Formats the value using the given formatter.