Struct ProofSearcher 

pub struct ProofSearcher {
    pub strategy: SearchStrategy,
    pub heuristic: HeuristicFn,
    pub max_depth: usize,
}

Systematic proof searcher with backtracking.

Fields

strategy: SearchStrategy

The search strategy.

heuristic: HeuristicFn

The heuristic function (used by A* and MCTS).

max_depth: usize

Maximum search depth.

Implementations

impl ProofSearcher

pub fn new(strategy: SearchStrategy, max_depth: usize) -> Self

Create a new proof searcher.

pub fn search( &self, goal: impl Into<String>, tactics: &[&str], ) -> Option<ProofState>

Attempt to search for a proof of goal using tactics. Returns the proof state if a complete proof is found.

Trait Implementations

impl Clone for ProofSearcher

fn clone(&self) -> ProofSearcher

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofSearcher

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

Formats the value using the given formatter.