Crate oxiz 

OxiZ - Next-Generation SMT Solver in Pure Rust

OxiZ is a high-performance SMT (Satisfiability Modulo Theories) solver written entirely in Pure Rust, designed to achieve feature parity with Z3 while leveraging Rust’s safety, performance, and concurrency features.

🎯 Key Features

• Pure Rust Implementation: No C/C++ dependencies, no FFI, complete memory safety
• Z3-Compatible: Extensive theory support and familiar API patterns
• High Performance: Optimized SAT core with advanced heuristics (VSIDS, LRB, CHB)
• Modular Design: Use only what you need via feature flags
• SMT-LIB2 Support: Full parser and printer for standard format

📦 Module Overview

Core Infrastructure

Module	Description
core	Term management, sorts, and SMT-LIB2 parsing
math	Mathematical utilities (polynomials, rationals, CAD)

Solver Components (enabled by solver feature)

Module	Description
sat	CDCL SAT solver with advanced heuristics
theories	Theory solvers (EUF, LRA, LIA, Arrays, BV, etc.)
solver	Main SMT solver with DPLL(T)

Advanced Features

Module	Feature Flag	Description
nlsat	nlsat	Nonlinear real arithmetic solver
opt	optimization	MaxSMT and optimization
spacer	spacer	CHC solver for program verification
proof	proof	Proof generation and checking

🚀 Quick Start

Installation

Add OxiZ to your Cargo.toml:

[dependencies]
oxiz = "0.1.3"  # Default: solver feature

With additional features:

[dependencies]
oxiz = { version = "0.1.3", features = ["nlsat", "optimization"] }

Or use all features:

[dependencies]
oxiz = { version = "0.1.3", features = ["full"] }

Basic SMT Solving

use oxiz::{Solver, TermManager, SolverResult};
use num_bigint::BigInt;

let mut solver = Solver::new();
let mut tm = TermManager::new();

// Create variables
let x = tm.mk_var("x", tm.sorts.int_sort);
let y = tm.mk_var("y", tm.sorts.int_sort);

// x + y = 10
let sum = tm.mk_add([x, y]);
let ten = tm.mk_int(BigInt::from(10));
let eq1 = tm.mk_eq(sum, ten);

// x > 5
let five = tm.mk_int(BigInt::from(5));
let gt = tm.mk_gt(x, five);

// Assert constraints
solver.assert(eq1, &mut tm);
solver.assert(gt, &mut tm);

// Check satisfiability
match solver.check(&mut tm) {
    SolverResult::Sat => {
        println!("SAT");
        if let Some(model) = solver.model() {
            println!("Model: {:?}", model);
        }
    }
    SolverResult::Unsat => println!("UNSAT"),
    SolverResult::Unknown => println!("Unknown"),
}

SMT-LIB2 Format

use oxiz::{Solver, TermManager};

let mut solver = Solver::new();
let mut tm = TermManager::new();

// Parse SMT-LIB2 script
let script = r#"
    (declare-const x Int)
    (declare-const y Int)
    (assert (= (+ x y) 10))
    (assert (> x 5))
    (check-sat)
"#;

// Execute commands
// solver.execute_script(script, &mut tm)?;

🔧 Feature Flags

Feature	Description	Default
solver	Core SMT solver (SAT + theories)	✓
nlsat	Nonlinear real arithmetic
optimization	MaxSMT and optimization
spacer	CHC solver
proof	Proof generation
standard	All common features except SPACER
full	All features

📚 Theory Support

• EUF: Equality and uninterpreted functions
• LRA: Linear real arithmetic (simplex)
• LIA: Linear integer arithmetic (branch-and-bound, cuts)
• NRA: Nonlinear real arithmetic (NLSAT, CAD)
• Arrays: Theory of arrays with extensionality
• BitVectors: Bit-precise reasoning
• Strings: String operations with regex
• Datatypes: Algebraic data types
• Floating-Point: IEEE 754 semantics

🎓 Examples

See the examples directory for more:

• Basic constraint solving
• Program verification
• Optimization problems
• Theory combinations

🔗 Related Projects

• oxiz-cli: Command-line interface
• oxiz-wasm: WebAssembly bindings

📖 More Information

• GitHub Repository
• Documentation
• SMT-LIB Standard

Re-exports

pub use oxiz_core as core;

pub use oxiz_math as math;

pub use oxiz_sat as sat;solver

pub use oxiz_theories as theories;solver

pub use oxiz_solver as solver;solver

pub use oxiz_nlsat as nlsat;nlsat

pub use oxiz_opt as opt;optimization

pub use oxiz_spacer as spacer;spacer

pub use oxiz_proof as proof;proof

Structs

Solversolver

Main CDCL(T) SMT Solver

Sort

A sort in the SMT-LIB2 sense

SortId

Unique identifier for a sort

Term

A term in the SMT-LIB2 sense

TermId

Unique identifier for a term in the arena

TermManager

Manager for term allocation and interning

Enums

SolverResultsolver

Result of SMT solving

Constants

VERSION

Current version of OxiZ