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 mmap;
55pub mod normalize;
56pub mod parallel;
57pub mod pattern;
58pub mod pcc;
59pub mod proof;
60pub mod rules;
61pub mod sat_integration;
62pub mod simplify;
63pub mod streaming;
64pub mod template;
65pub mod theory;
66pub mod unsat_core;
67pub mod validation;
68pub mod visualization;
69
70// Internal modules
71mod builder;
72mod cnf;
73mod convert;
74mod premise;
75mod quantifier;
76mod resolution;
77
78// Public modules with useful analysis and utility tools
79pub mod stats;
80pub mod traversal;
81// TODO: Fix API compatibility with new ProofNode structure
82// pub mod transform;
83// pub mod compression;
84
85// Proof logging and replay (binary format for offline verification)
86pub mod logging;
87pub mod replay;
88
89// Re-exports
90pub use alethe::{AletheProof, AletheProofProducer, AletheRule, AletheStep};
91pub use carcara::{CarcaraProof, to_carcara_format, validate_for_carcara};
92pub use checker::{CheckError, CheckResult, Checkable, CheckerConfig, ErrorSeverity, ProofChecker};
93pub use compress::{
94    CompressionConfig, CompressionResult, ProofCompressor, get_dependency_cone, trim_to_conclusion,
95};
96pub use conversion::{ConversionError, ConversionResult, FormatConverter};
97pub use coq::{CoqExporter, export_theory_to_coq, export_to_coq};
98pub use coq_enhanced::{CoqProofTerm, CoqType, EnhancedCoqExporter, export_to_coq_enhanced};
99pub use diff::{ProofDiff, ProofSimilarity, compute_similarity, diff_proofs};
100pub use drat::{DratProof, DratProofProducer, DratStep};
101pub use explanation::{ExplainedStep, ProofComplexity, ProofExplainer, Verbosity};
102pub use fingerprint::{FingerprintDatabase, FingerprintGenerator, ProofFingerprint, SizeFeatures};
103pub use format::ProofFormat;
104pub use heuristic::{HeuristicType, ProofHeuristic, StrategyLearner};
105pub use incremental::{IncrementalProofBuilder, IncrementalStats, ProofRecorder};
106pub use interpolant::{Color, Interpolant, InterpolantExtractor, Partition};
107pub use isabelle::{IsabelleExporter, export_theory_to_isabelle, export_to_isabelle};
108pub use isabelle_enhanced::{
109    EnhancedIsabelleExporter, IsabelleMethod, IsabelleProof, IsabelleType, IsarProofBody,
110    export_to_isabelle_apply_style, export_to_isabelle_enhanced,
111};
112pub use lazy::{LazyDependencyResolver, LazyNode, LazyProof, LazyStats};
113pub use lean::{LeanExporter, export_theory_to_lean, export_to_lean, export_to_lean3};
114pub use lean_enhanced::{
115    EnhancedLeanExporter, LeanProofTerm, LeanTactic, LeanType, export_to_lean_enhanced,
116    export_to_lean_term_mode,
117};
118pub use lfsc::{LfscDecl, LfscProof, LfscProofProducer, LfscSort, LfscTerm};
119pub use merge::{merge_proofs, slice_proof, slice_proof_multi};
120pub use metadata::{Difficulty, Priority, ProofMetadata, Strategy};
121pub use mmap::{MmapConfig, MmapProof, MmapProofStorage};
122pub use normalize::{canonicalize_conclusions, normalize_proof};
123pub use parallel::{ParallelCheckResult, ParallelConfig, ParallelProcessor, ParallelStatsComputer};
124pub use pattern::{LemmaPattern, PatternExtractor, PatternStructure};
125pub use pcc::{CodeLocation, PccBuilder, ProofCarryingCode, SafetyProperty, VerificationCondition};
126pub use proof::{Proof, ProofNode, ProofNodeId, ProofStats, ProofStep};
127pub use rules::{
128    Clause, CnfValidator, Literal, ResolutionValidator, RuleValidation, TheoryLemmaValidator,
129    UnitPropagationValidator,
130};
131#[cfg(feature = "sat-integration")]
132pub use sat_integration::{
133    ProofRecordingSolver, drat_clause_to_sat, drat_lit_to_sat, sat_clause_to_drat, sat_lit_to_drat,
134};
135pub use simplify::{ProofSimplifier, SimplificationConfig, SimplificationStats, simplify_proof};
136pub use stats::{DetailedProofStats, ProofQuality, TheoryProofStats};
137pub use streaming::{
138    ProofChunk, ProofChunkIterator, ProofStreamer, StreamConfig, StreamingProofBuilder,
139};
140pub use template::{ProofTemplate, TemplateIdentifier, TemplateStep};
141pub use theory::{
142    ArithProofRecorder, ArrayProofRecorder, EufProofRecorder, ProofTerm, TheoryProof,
143    TheoryProofProducer, TheoryRule, TheoryStep, TheoryStepId,
144};
145pub use unsat_core::{UnsatCore, extract_minimal_unsat_core, extract_unsat_core, get_core_labels};
146pub use validation::{FormatValidator, ValidationError, ValidationResult};
147pub use visualization::{ProofVisualizer, VisualizationFormat};
148
149// Craig interpolation
150pub use craig::{
151    ArrayInterpolator, CraigInterpolator, EufInterpolator, InterpolantColor, InterpolantPartition,
152    InterpolantTerm, InterpolationAlgorithm, InterpolationConfig, InterpolationError,
153    InterpolationStats, LiaInterpolator, SequenceInterpolator, Symbol, TheoryInterpolator,
154    TreeInterpolator, TreeNode,
155};
oxiz_proof/lib.rs

oxiz_proof/
lib.rs
