Struct AxiomValidator 

pub struct AxiomValidator { /* private fields */ }

Axiom validator for checking axiom consistency and tracking dependencies.

Implementations

impl AxiomValidator

pub fn new() -> Self

Create a new axiom validator.

pub fn register(&mut self, name: Name)

Register an axiom.

pub fn mark_unsafe(&mut self, name: Name)

Mark an axiom as unsafe.

pub fn mark_safe(&mut self, name: Name)

Mark an axiom as safe.

pub fn is_axiom(&self, name: &Name) -> bool

Check if a name is a registered axiom.

pub fn is_unsafe(&self, name: &Name) -> bool

Check if an axiom is marked as unsafe.

pub fn is_classical(&self, name: &Name) -> bool

Check if an axiom is classical.

pub fn all_axioms(&self) -> Vec<&Name>

Get all registered axioms.

pub fn unsafe_axioms(&self) -> Vec<&Name>

Get all unsafe axioms.

pub fn classify(&self, name: &Name) -> AxiomSafety

Classify an axiom’s safety.

pub fn check_dependencies(&self, expr: &Expr) -> HashSet<Name>

Extract all constant dependencies from an expression.

pub fn axiom_dependencies(&self, expr: &Expr) -> HashSet<Name>

Extract only axiom dependencies from an expression.

pub fn is_constructive(&self, expr: &Expr) -> bool

Check if an expression is constructive (uses no classical axioms).

Trait Implementations

impl Default for AxiomValidator

fn default() -> Self

Returns the “default value” for a type.