Struct CegisState 

pub struct CegisState {
    pub spec: Spec,
    pub counterexamples: Vec<Vec<String>>,
    pub candidate: Option<Candidate>,
    pub iterations: usize,
    pub max_iterations: usize,
}

The CEGIS synthesis loop state.

Fields

spec: Spec

The specification to satisfy.

counterexamples: Vec<Vec<String>>

Counterexamples accumulated across iterations.

candidate: Option<Candidate>

Current candidate (if any).

iterations: usize

Number of CEGIS iterations performed.

max_iterations: usize

Maximum allowed iterations before giving up.

Implementations

impl CegisState

pub fn new(spec: Spec, max_iterations: usize) -> Self

Initialise a CEGIS loop for the given spec.

use oxilean_std::program_synthesis::{CegisState, Spec};
let state = CegisState::new(Spec::logic("y = x + 1"), 100);
assert_eq!(state.iterations, 0);

pub fn propose(&mut self, candidate: Candidate)

Propose a candidate (synthesiser step).

pub fn add_counterexample(&mut self, ce: Vec<String>)

Record a counterexample returned by the verifier.

pub fn is_solved(&self) -> bool

Check whether the synthesis loop has terminated successfully.

pub fn is_exhausted(&self) -> bool

Check whether the loop has exceeded its iteration budget.

Trait Implementations

impl Clone for CegisState

fn clone(&self) -> CegisState

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CegisState

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

Formats the value using the given formatter.