Crate foras 

Rust re-implementation scaffolding for the Foras theorem prover.

The crate is organized into foundational modules that mirror the original Foras C layout while embracing Rust’s type system. Each module will grow to encapsulate a cohesive portion of the prover as we port more logic.

Re-exports

pub use config::Flag;

pub use config::FlagSet;

pub use config::ParameterSet;

pub use config::ParameterValue;

pub use config::Statistics;

pub use data::Clause;

pub use data::ClauseArena;

pub use data::ClauseAttribute;

pub use data::ClauseAttributeValue;

pub use data::ClauseId;

pub use data::ClauseList;

pub use data::Context;

pub use data::ContextStatus;

pub use data::ImdBfs;

pub use data::ImdNode;

pub use data::ImdNodeKind;

pub use data::IsNode;

pub use data::Literal;

pub use data::MAX_VARS;

pub use data::ParentList;

pub use data::Symbol;

pub use data::SymbolId;

pub use data::SymbolKind;

pub use data::SymbolTable;

pub use data::Term;

pub use data::TermKind;

pub use data::VariableId;

pub use parser::ListSection;

pub use parser::ForasFile;

pub use parser::ParseError;

pub use parser::Parser;

pub use inference::all_resolvents;

pub use inference::apply_to_clause;

pub use inference::apply_to_literal;

pub use inference::binary_resolve;

pub use inference::rename_variables;

pub use inference::ProofResult;

pub use inference::Prover;

pub use inference::ProverBuilder;

pub use inference::Resolvent;

pub use inference::Substitution;

pub use inference::UnificationError;

pub use inference::Unifier;

pub use regression::ExampleCase;

pub use regression::ExampleSuite;

pub use regression::ProverMetrics;

pub use regression::RegressionExecutor;

pub use regression::RegressionGroupSummary;

pub use regression::RegressionResult;

pub use regression::RegressionSummary;

Modules

config

Configuration types describing flags, parameters, statistics, and related state.

data

Core data structures used throughout the prover.

inference

Inference engine components for the theorem prover.

parser

Simplified parser for Foras input files.

regression

Helpers for working with the legacy Foras example suite.