oxiz_proof/
lib.rs

1//! # oxiz-proof
2//!
3//! Proof generation and checking for the OxiZ SMT solver.
4//!
5//! This crate provides machine-checkable proof output in various formats,
6//! enabling verification of solver results by external proof checkers.
7//!
8//! ## Beyond Z3
9//!
10//! While Z3 supports generic proofs, OxiZ aims to generate **machine-checkable
11//! proofs** (Alethe, LFSC) by default, making it more suitable for certified
12//! verification workflows.
13//!
14//! ## Supported Formats
15//!
16//! - **DRAT**: For SAT core proofs
17//! - **Alethe**: SMT-LIB proof format
18//! - **Carcara**: Proof checker compatibility for Alethe format
19//! - **LFSC**: Logical Framework with Side Conditions
20//! - **Coq**: Export to Coq proof assistant
21//! - **Lean**: Export to Lean theorem prover (Lean 3 & 4)
22//! - **Isabelle**: Export to Isabelle/HOL
23//! - **Theory**: Theory-specific proof steps
24//! - **Checker**: Proof validation infrastructure
25//! - **PCC**: Proof-carrying code generation
26//! - **Merge**: Proof merging and slicing utilities
27//! - **Diff**: Proof comparison and similarity metrics
28//! - **Normalize**: Proof normalization for canonical representation
29
30pub mod alethe;
31pub mod carcara;
32pub mod checker;
33pub mod compress;
34pub mod conversion;
35pub mod coq;
36pub mod coq_enhanced;
37pub mod craig;
38pub mod diff;
39pub mod drat;
40pub mod explanation;
41pub mod fingerprint;
42pub mod format;
43pub mod heuristic;
44pub mod incremental;
45pub mod interpolant;
46pub mod isabelle;
47pub mod isabelle_enhanced;
48pub mod lazy;
49pub mod lean;
50pub mod lean_enhanced;
51pub mod lfsc;
52pub mod merge;
53pub mod metadata;
54pub mod minimize;
55pub mod mmap;
56pub mod normalize;
57pub mod parallel;
58pub mod pattern;
59pub mod pcc;
60pub mod proof;
61pub mod recorder;
62pub mod rules;
63pub mod sat_integration;
64pub mod simplify;
65pub mod streaming;
66pub mod template;
67pub mod theory;
68pub mod theory_combination;
69pub mod unsat_core;
70pub mod validation;
71pub mod visualization;
72
73// Internal modules
74mod builder;
75mod cnf;
76mod convert;
77mod premise;
78mod quantifier;
79mod resolution;
80
81// Public modules with useful analysis and utility tools
82pub mod stats;
83pub mod traversal;
84// TODO: Fix API compatibility with new ProofNode structure
85// pub mod transform;
86// pub mod compression;
87
88// Proof logging and replay (binary format for offline verification)
89pub mod logging;
90pub mod replay;
91
92// Re-exports
93pub use alethe::{AletheProof, AletheProofProducer, AletheRule, AletheStep};
94pub use carcara::{CarcaraProof, to_carcara_format, validate_for_carcara};
95pub use checker::{CheckError, CheckResult, Checkable, CheckerConfig, ErrorSeverity, ProofChecker};
96pub use compress::{
97    CompressionConfig, CompressionResult, ProofCompressor, get_dependency_cone, trim_to_conclusion,
98};
99pub use conversion::{ConversionError, ConversionResult, FormatConverter};
100pub use coq::{CoqExporter, export_theory_to_coq, export_to_coq};
101pub use coq_enhanced::{CoqProofTerm, CoqType, EnhancedCoqExporter, export_to_coq_enhanced};
102pub use diff::{ProofDiff, ProofSimilarity, compute_similarity, diff_proofs};
103pub use drat::{DratProof, DratProofProducer, DratStep};
104pub use explanation::{ExplainedStep, ProofComplexity, ProofExplainer, Verbosity};
105pub use fingerprint::{FingerprintDatabase, FingerprintGenerator, ProofFingerprint, SizeFeatures};
106pub use format::ProofFormat;
107pub use heuristic::{HeuristicType, ProofHeuristic, StrategyLearner};
108pub use incremental::{IncrementalProofBuilder, IncrementalStats, ProofRecorder};
109pub use interpolant::{Color, Interpolant, InterpolantExtractor, Partition};
110pub use isabelle::{IsabelleExporter, export_theory_to_isabelle, export_to_isabelle};
111pub use isabelle_enhanced::{
112    EnhancedIsabelleExporter, IsabelleMethod, IsabelleProof, IsabelleType, IsarProofBody,
113    export_to_isabelle_apply_style, export_to_isabelle_enhanced,
114};
115pub use lazy::{LazyDependencyResolver, LazyNode, LazyProof, LazyStats};
116pub use lean::{LeanExporter, export_theory_to_lean, export_to_lean, export_to_lean3};
117pub use lean_enhanced::{
118    EnhancedLeanExporter, LeanProofTerm, LeanTactic, LeanType, export_to_lean_enhanced,
119    export_to_lean_term_mode,
120};
121pub use lfsc::{LfscDecl, LfscProof, LfscProofProducer, LfscSort, LfscTerm};
122pub use merge::{merge_proofs, slice_proof, slice_proof_multi};
123pub use metadata::{Difficulty, Priority, ProofMetadata, Strategy};
124pub use minimize::{MinimizeConfig, MinimizeResult, ProofMinimizer};
125pub use mmap::{MmapConfig, MmapProof, MmapProofStorage};
126pub use normalize::{canonicalize_conclusions, normalize_proof};
127pub use parallel::{ParallelCheckResult, ParallelConfig, ParallelProcessor, ParallelStatsComputer};
128pub use pattern::{LemmaPattern, PatternExtractor, PatternStructure};
129pub use pcc::{CodeLocation, PccBuilder, ProofCarryingCode, SafetyProperty, VerificationCondition};
130pub use proof::{Proof, ProofNode, ProofNodeId, ProofStats, ProofStep};
131#[cfg(feature = "arena")]
132pub use recorder::ArenaProofStepId;
133pub use recorder::Recorder;
134pub use rules::{
135    Clause, CnfValidator, Literal, ResolutionValidator, RuleValidation, TheoryLemmaValidator,
136    UnitPropagationValidator,
137};
138#[cfg(feature = "sat-integration")]
139pub use sat_integration::{
140    ProofRecordingSolver, drat_clause_to_sat, drat_lit_to_sat, sat_clause_to_drat, sat_lit_to_drat,
141};
142pub use simplify::{ProofSimplifier, SimplificationConfig, SimplificationStats, simplify_proof};
143pub use stats::{DetailedProofStats, ProofQuality, TheoryProofStats};
144pub use streaming::{
145    ProofChunk, ProofChunkIterator, ProofStreamer, StreamConfig, StreamingProofBuilder,
146};
147pub use template::{ProofTemplate, TemplateIdentifier, TemplateStep};
148pub use theory::{
149    ArithProofRecorder, ArrayProofRecorder, EufProofRecorder, ProofTerm, TheoryProof,
150    TheoryProofProducer, TheoryRule, TheoryStep, TheoryStepId,
151};
152pub use theory_combination::{
153    CombinationStep, NelsonOppenCertificate, TheoryId as CombinationTheoryId,
154};
155pub use unsat_core::{UnsatCore, extract_minimal_unsat_core, extract_unsat_core, get_core_labels};
156pub use validation::{FormatValidator, ValidationError, ValidationResult};
157pub use visualization::{ProofVisualizer, VisualizationFormat};
158
159// Craig interpolation
160pub use craig::{
161    ArrayInterpolator, CraigInterpolator, EufInterpolator, InterpolantColor, InterpolantPartition,
162    InterpolantTerm, InterpolationAlgorithm, InterpolationConfig, InterpolationError,
163    InterpolationStats, LiaInterpolator, SequenceInterpolator, Symbol, TheoryInterpolator,
164    TreeInterpolator, TreeNode,
165};
oxiz_proof/lib.rs

oxiz_proof/
lib.rs
