Expand description
§oxiz-spacer
Property Directed Reachability (PDR/IC3) engine for OxiZ.
This crate implements Spacer, a solver for Constrained Horn Clauses (CHC), which is essential for software verification tasks like loop invariant inference.
§Key Differentiator
Spacer is missing in most Z3 clones. Having a Pure Rust implementation makes OxiZ uniquely suitable for verification toolchains.
§Reference
Z3’s muz/spacer/ directory.
§Use Cases
- Loop Invariant Inference: Automatically find loop invariants
- Safety Verification: Prove program safety properties
- Model Checking: Bounded and unbounded verification
- Interpolation: Generate Craig interpolants
§Example
use oxiz_spacer::chc::{ChcSystem, PredicateApp};
use oxiz_spacer::pdr::{Spacer, SpacerResult};
use oxiz_core::TermManager;
let mut terms = TermManager::new();
let mut system = ChcSystem::new();
// Declare a predicate Inv(x: Int)
let inv = system.declare_predicate("Inv", [terms.sorts.int_sort]);
// Add init rule: x = 0 => Inv(x)
let x = terms.mk_var("x", terms.sorts.int_sort);
let zero = terms.mk_int(0);
let init_constraint = terms.mk_eq(x, zero);
system.add_init_rule(
[("x".to_string(), terms.sorts.int_sort)],
init_constraint,
inv,
[x],
);
// Add query: Inv(x) /\ x < 0 => false
let neg_constraint = terms.mk_lt(x, zero);
system.add_query(
[("x".to_string(), terms.sorts.int_sort)],
[PredicateApp::new(inv, [x])],
neg_constraint,
);
// Solve
let mut spacer = Spacer::new(&mut terms, &system);
let result = spacer.solve();
assert!(matches!(result, Ok(SpacerResult::Safe)));Re-exports§
pub use abduction::AbductionError;pub use abduction::AbductionResult;pub use abduction::AbductiveSolver;pub use abduction::Hypothesis;pub use abduction::HypothesisGenerator;pub use abduction::HypothesisOrigin;pub use abduction::HypothesisTemplate;pub use abduction::InvariantSynthesizer;pub use abduction::PreconditionSynthesizer;pub use abduction::TemplateParamKind;pub use abduction::TemplateStructure;pub use bmc::Bmc;pub use bmc::BmcConfig;pub use bmc::BmcError;pub use bmc::BmcResult;pub use bmc::BmcStats;pub use bmc::HybridSolver;pub use chc::ChcSystem;pub use chc::PredId;pub use chc::Predicate;pub use chc::PredicateApp;pub use chc::Rule;pub use chc::RuleBody;pub use chc::RuleHead;pub use chc::RuleId;pub use chccomp::ChcCompError;pub use chccomp::ChcCompParser;pub use ctg::CtgError;pub use ctg::CtgResult;pub use ctg::CtgStrengthener;pub use diagnostics::InvariantFormatter;pub use diagnostics::StatsReporter;pub use diagnostics::TraceBuffer;pub use diagnostics::TraceEvent;pub use diagnostics::TraceLevel;pub use distributed::DistributedConfig;pub use distributed::DistributedCoordinator;pub use distributed::DistributedError;pub use distributed::DistributedStats;pub use distributed::WorkItem as DistributedWorkItem;pub use distributed::Worker;pub use distributed::WorkerMessage;pub use existential::ExistentialError;pub use existential::ExistentialHandler;pub use existential::ExistentialInfo;pub use existential::ExistentialProjector;pub use existential::ExistentialResult;pub use existential::SkolemContext;pub use existential::WitnessExtractor;pub use frames::FrameManager;pub use frames::INFTY_LEVEL;pub use frames::Lemma;pub use frames::LemmaId;pub use frames::PredicateFrames;pub use generalize::GeneralizationError;pub use generalize::GeneralizationResult;pub use generalize::Generalizer;pub use interp::Interpolant;pub use interp::InterpolationError;pub use interp::InterpolationResult;pub use interp::Interpolator;pub use invariant::Candidate;pub use invariant::CandidateSource;pub use invariant::InferenceResult;pub use invariant::InferenceStats;pub use invariant::InvariantConfig;pub use invariant::InvariantInference;pub use invariant::TemplateKind;pub use nonlinear::InterpolantTree;pub use nonlinear::NonLinearAnalyzer;pub use nonlinear::NonLinearError;pub use nonlinear::NonLinearLemmaCombiner;pub use nonlinear::NonLinearResult;pub use nonlinear::NonLinearRuleAnalysis;pub use nonlinear::NonLinearStats;pub use nonlinear::TreeInterpolant;pub use parallel::ParallelConfig;pub use parallel::ParallelError;pub use parallel::ParallelFrameSolver;pub use parallel::ParallelPropagator;pub use parallel::WorkItem;pub use parallel::WorkResult;pub use parser::ChcParser;pub use parser::ParseError;pub use pdr::Spacer;pub use pdr::SpacerConfig;pub use pdr::SpacerError;pub use pdr::SpacerResult;pub use pdr::SpacerStats;pub use pob::Pob;pub use pob::PobId;pub use pob::PobManager;pub use pob::PobQueue;pub use portfolio::PortfolioError;pub use portfolio::PortfolioResult;pub use portfolio::PortfolioSolver;pub use portfolio::Strategy;pub use proof::ProofBuilder;pub use proof::ProofStep;pub use proof::SafetyProof;pub use reach::CexState;pub use reach::ConcreteState;pub use reach::ConcreteValue;pub use reach::ConcreteWitness;pub use reach::ConcreteWitnessExtractor;pub use reach::Counterexample;pub use reach::Generalization;pub use reach::OverApproximation;pub use reach::Projection;pub use reach::ReachFact;pub use reach::ReachFactId;pub use reach::ReachFactStore;pub use reach::ReachabilityChecker;pub use reach::UnderApproximation;pub use reach::WitnessError;pub use recursive::RecursionKind;pub use recursive::RecursiveAnalyzer;pub use recursive::RecursiveError;pub use recursive::RecursiveInfo;pub use smt::MbpResult;pub use smt::Model;pub use smt::SmtError;pub use smt::SmtSolver;pub use smt::SmtStats;pub use theory::TheoryIntegration;
Modules§
- abduction
- Abduction support for hypothesis generation.
- bmc
- Bounded Model Checking (BMC) for CHC systems.
- chc
- Constrained Horn Clause (CHC) representation.
- chccomp
- CHC-COMP format parser
- ctg
- Counterexample-Guided (CTG) strengthening with conflict analysis.
- diagnostics
- Diagnostics, statistics, and tracing for Spacer.
- distributed
- Distributed PDR for solving large CHC systems across multiple workers.
- existential
- Existential quantifier handling for CHCs.
- frames
- Frame management for PDR (Property Directed Reachability).
- generalize
- Generalization algorithms for lemma strengthening
- interp
- Interpolation utilities for Spacer.
- invariant
- Loop Invariant Inference
- nonlinear
- Non-linear CHC constraint handling.
- parallel
- Parallel frame solving for Spacer.
- parser
- CHC-COMP format parser
- pdr
- Property Directed Reachability (PDR/IC3) algorithm.
- pob
- Proof Obligation (POB) management.
- portfolio
- Portfolio solver for running multiple Spacer strategies.
- proof
- Proof generation and validation for Spacer.
- reach
- Reachability analysis utilities.
- recursive
- Recursive CHC support and analysis.
- smt
- SMT solver integration for Spacer
- theory
- Theory-aware operations for Spacer.