Struct cop::lean::search::Search

pub struct Search<'t, P, C> {
    pub sub: Sub<'t, C>,
    /* private fields */
}

State of the proof search.

Fields

sub: Sub<'t, C>

substitution

Implementations

impl<'t, P, C> Search<'t, P, C>

pub fn new( cl: &'t Clause<&Lit<P, C, usize>>, db: &'t Db<'_, P, C, usize>, opt: Opt ) -> Self

Initialise a new proof search.

impl<'t, P, C> Search<'t, P, C>where P: Clone + Display + Eq + Hash + Neg<Output = P>, C: Clone + Display + Eq,

pub fn prove(&mut self) -> Option<&Vec<Action<'t, P, C>>>

Perform proof search, returning Some(proof) if you are lucky. :)

This function should eventually terminate.

pub fn inferences(&self) -> usize

Return the number of inferences performed so far.