Struct RuleSet 

pub struct RuleSet { /* private fields */ }

An extensible collection of search rules.

Implementations

impl RuleSet

pub fn new() -> Self

pub fn register(&mut self, rule: Rule)

pub fn len(&self) -> usize

pub fn is_empty(&self) -> bool

pub fn search(&self, st: &mut ProofState) -> SearchStats

Best-first search from st. Applies safe rules eagerly at each node, then forks on unsafe rules in priority order. Succeeds (leaving st at a closed proof state) when some branch drives the open goals to zero.

pub fn search_bounded(&self, st: &mut ProofState, budget: usize) -> SearchStats

Trait Implementations

impl Default for RuleSet

fn default() -> RuleSet

Returns the “default value” for a type.