Struct HoudiniInvariantSynth 

pub struct HoudiniInvariantSynth {
    pub candidates: Vec<String>,
    pub iterations: usize,
}

An inductive loop invariant synthesiser using Houdini-style fixpoint.

Fields

candidates: Vec<String>

Candidate invariant predicates to try.

iterations: usize

Iterations of the Houdini fixpoint computation.

Implementations

impl HoudiniInvariantSynth

pub fn new(candidates: Vec<String>) -> Self

Create a Houdini synthesiser with an initial set of candidates.

use oxilean_std::program_synthesis::HoudiniInvariantSynth;
let h = HoudiniInvariantSynth::new(vec!["x >= 0".into(), "x <= n".into()]);
assert_eq!(h.candidates.len(), 2);

pub fn add_candidate(&mut self, pred: impl Into<String>)

Add a candidate invariant predicate.

pub fn step(&mut self) -> usize

Simulate one Houdini iteration: remove candidates falsified by pre-image.

In a real implementation, each candidate would be checked against the loop body; here we just count the iteration.

pub fn current_invariants(&self) -> &[String]

Return the current invariant candidate set.

pub fn is_fixpoint(&self) -> bool

Check whether a fixpoint has been reached (placeholder heuristic).

Trait Implementations

impl Clone for HoudiniInvariantSynth

fn clone(&self) -> HoudiniInvariantSynth

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for HoudiniInvariantSynth

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

Formats the value using the given formatter.