oxiz_spacer/
lib.rs

1//! # oxiz-spacer
2//!
3//! Property Directed Reachability (PDR/IC3) engine for OxiZ.
4//!
5//! This crate implements Spacer, a solver for Constrained Horn Clauses (CHC),
6//! which is essential for software verification tasks like loop invariant inference.
7//!
8//! ## Key Differentiator
9//!
10//! Spacer is **missing in most Z3 clones**. Having a Pure Rust implementation
11//! makes OxiZ uniquely suitable for verification toolchains.
12//!
13//! ## Reference
14//!
15//! Z3's `muz/spacer/` directory.
16//!
17//! ## Use Cases
18//!
19//! - **Loop Invariant Inference**: Automatically find loop invariants
20//! - **Safety Verification**: Prove program safety properties
21//! - **Model Checking**: Bounded and unbounded verification
22//! - **Interpolation**: Generate Craig interpolants
23//!
24//! ## Example
25//!
26//! ```rust,no_run
27//! use oxiz_spacer::chc::{ChcSystem, PredicateApp};
28//! use oxiz_spacer::pdr::{Spacer, SpacerResult};
29//! use oxiz_core::TermManager;
30//!
31//! let mut terms = TermManager::new();
32//! let mut system = ChcSystem::new();
33//!
34//! // Declare a predicate Inv(x: Int)
35//! let inv = system.declare_predicate("Inv", [terms.sorts.int_sort]);
36//!
37//! // Add init rule: x = 0 => Inv(x)
38//! let x = terms.mk_var("x", terms.sorts.int_sort);
39//! let zero = terms.mk_int(0);
40//! let init_constraint = terms.mk_eq(x, zero);
41//! system.add_init_rule(
42//!     [("x".to_string(), terms.sorts.int_sort)],
43//!     init_constraint,
44//!     inv,
45//!     [x],
46//! );
47//!
48//! // Add query: Inv(x) /\ x < 0 => false
49//! let neg_constraint = terms.mk_lt(x, zero);
50//! system.add_query(
51//!     [("x".to_string(), terms.sorts.int_sort)],
52//!     [PredicateApp::new(inv, [x])],
53//!     neg_constraint,
54//! );
55//!
56//! // Solve
57//! let mut spacer = Spacer::new(&mut terms, &system);
58//! let result = spacer.solve();
59//! assert!(matches!(result, Ok(SpacerResult::Safe)));
60//! ```
61
62pub mod abduction;
63pub mod bmc;
64pub mod chc;
65pub mod chccomp;
66pub mod ctg;
67pub mod diagnostics;
68pub mod distributed;
69pub mod existential;
70pub mod frames;
71pub mod generalize;
72pub mod interp;
73pub mod invariant;
74pub mod nonlinear;
75pub mod parallel;
76pub mod parser;
77pub mod pdr;
78pub mod pob;
79pub mod portfolio;
80pub mod proof;
81pub mod reach;
82pub mod recursive;
83pub mod smt;
84pub mod theory;
85
86// Re-exports for convenience
87pub use abduction::{
88    AbductionError, AbductionResult, AbductiveSolver, Hypothesis, HypothesisGenerator,
89    HypothesisOrigin, HypothesisTemplate, InvariantSynthesizer, PreconditionSynthesizer,
90    TemplateParamKind, TemplateStructure,
91};
92pub use bmc::{Bmc, BmcConfig, BmcError, BmcResult, BmcStats, HybridSolver};
93pub use chc::{ChcSystem, PredId, Predicate, PredicateApp, Rule, RuleBody, RuleHead, RuleId};
94pub use chccomp::{ChcCompError, ChcCompParser};
95pub use ctg::{CtgError, CtgResult, CtgStrengthener};
96pub use diagnostics::{InvariantFormatter, StatsReporter, TraceBuffer, TraceEvent, TraceLevel};
97pub use distributed::{
98    DistributedConfig, DistributedCoordinator, DistributedError, DistributedStats, SharedState,
99    WorkItem as DistributedWorkItem, Worker, WorkerMessage,
100};
101pub use existential::{
102    ExistentialError, ExistentialHandler, ExistentialInfo, ExistentialProjector, ExistentialResult,
103    SkolemContext, WitnessExtractor,
104};
105pub use frames::{FrameManager, INFTY_LEVEL, Lemma, LemmaId, PredicateFrames};
106pub use generalize::{GeneralizationError, GeneralizationResult, Generalizer};
107pub use interp::{Interpolant, InterpolationError, InterpolationResult, Interpolator};
108pub use invariant::{
109    Candidate, CandidateSource, InferenceResult, InferenceStats, InvariantConfig,
110    InvariantInference, TemplateKind,
111};
112pub use nonlinear::{
113    InterpolantTree, NonLinearAnalyzer, NonLinearError, NonLinearLemmaCombiner, NonLinearResult,
114    NonLinearRuleAnalysis, NonLinearStats, TreeInterpolant,
115};
116pub use parallel::{
117    ParallelConfig, ParallelError, ParallelFrameSolver, ParallelPropagator, WorkItem, WorkResult,
118};
119pub use parser::{ChcParser, ParseError};
120pub use pdr::{Spacer, SpacerConfig, SpacerError, SpacerResult, SpacerStats};
121pub use pob::{Pob, PobId, PobManager, PobQueue};
122pub use portfolio::{PortfolioError, PortfolioResult, PortfolioSolver, Strategy};
123pub use proof::{ProofBuilder, ProofStep, SafetyProof};
124pub use reach::{
125    CexState, ConcreteState, ConcreteValue, ConcreteWitness, ConcreteWitnessExtractor,
126    Counterexample, Generalization, OverApproximation, Projection, ReachFact, ReachFactId,
127    ReachFactStore, ReachabilityChecker, UnderApproximation, WitnessError,
128};
129pub use recursive::{RecursionKind, RecursiveAnalyzer, RecursiveError, RecursiveInfo};
130pub use smt::{MbpResult, Model, SmtError, SmtSolver, SmtStats};
131pub use theory::TheoryIntegration;
oxiz_spacer/lib.rs

oxiz_spacer/
lib.rs
