Struct ProofState 

pub struct ProofState {
    pub goals: Vec<String>,
    pub applied_tactics: Vec<String>,
    pub budget: usize,
}

Current state of a proof search.

Fields

goals: Vec<String>

Remaining goals as formula strings.

applied_tactics: Vec<String>

Tactics applied so far.

budget: usize

Remaining computational budget (steps).

Implementations

impl ProofState

pub fn new(goal: impl Into<String>, budget: usize) -> Self

Create a proof state with a single goal and a budget.

pub fn is_complete(&self) -> bool

Returns true if all goals have been discharged.

pub fn apply_tactic(&mut self, tactic: impl Into<String>) -> bool

Apply a tactic name: removes the first goal and decrements budget.

Trait Implementations

impl Clone for ProofState

fn clone(&self) -> ProofState

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofState

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

Formats the value using the given formatter.