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

oxiz_proof/
lib.rs
