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
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 minimize::{MinimizeConfig, MinimizeResult, ProofMinimizer};
122pub use mmap::{MmapConfig, MmapProof, MmapProofStorage};
123pub use normalize::{canonicalize_conclusions, normalize_proof};
124pub use parallel::{ParallelCheckResult, ParallelConfig, ParallelProcessor, ParallelStatsComputer};
125pub use pattern::{LemmaPattern, PatternExtractor, PatternStructure};
126pub use pcc::{CodeLocation, PccBuilder, ProofCarryingCode, SafetyProperty, VerificationCondition};
127pub use proof::{Proof, ProofNode, ProofNodeId, ProofStats, ProofStep};
128#[cfg(feature = "arena")]
129pub use recorder::ArenaProofStepId;
130pub use recorder::Recorder;
131pub use rules::{
132    Clause, CnfValidator, Literal, ResolutionValidator, RuleValidation, TheoryLemmaValidator,
133    UnitPropagationValidator,
134};
135#[cfg(feature = "sat-integration")]
136pub use sat_integration::{
137    ProofRecordingSolver, drat_clause_to_sat, drat_lit_to_sat, sat_clause_to_drat, sat_lit_to_drat,
138};
139pub use simplify::{ProofSimplifier, SimplificationConfig, SimplificationStats, simplify_proof};
140pub use stats::{DetailedProofStats, ProofQuality, TheoryProofStats};
141pub use streaming::{
142    ProofChunk, ProofChunkIterator, ProofStreamer, StreamConfig, StreamingProofBuilder,
143};
144pub use template::{ProofTemplate, TemplateIdentifier, TemplateStep};
145pub use theory::{
146    ArithProofRecorder, ArrayProofRecorder, EufProofRecorder, ProofTerm, TheoryProof,
147    TheoryProofProducer, TheoryRule, TheoryStep, TheoryStepId,
148};
149pub use theory_combination::{
150    CombinationStep, NelsonOppenCertificate, TheoryId as CombinationTheoryId,
151};
152pub use unsat_core::{UnsatCore, extract_minimal_unsat_core, extract_unsat_core, get_core_labels};
153pub use validation::{FormatValidator, ValidationError, ValidationResult};
154pub use visualization::{ProofVisualizer, VisualizationFormat};
155
156// Craig interpolation
157pub use craig::{
158    ArrayInterpolator, CraigInterpolator, EufInterpolator, InterpolantColor, InterpolantPartition,
159    InterpolantTerm, InterpolationAlgorithm, InterpolationConfig, InterpolationError,
160    InterpolationStats, LiaInterpolator, SequenceInterpolator, Symbol, TheoryInterpolator,
161    TreeInterpolator, TreeNode,
162};
oxiz_proof/lib.rs

oxiz_proof/
lib.rs
