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 (requires std feature)
• no_std Support: Core solver compiles for bare-metal targets (RISC-V, zkVM)

Module Overview

Core Infrastructure (always available)

Module	Description
core	Term management, sorts, and SMT-LIB2 parsing
math	Mathematical utilities (polynomials, rationals, CAD)
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 (require std)

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.2.0"  # Default: std + core solver

For no_std (e.g., zkVM):

[dependencies]
oxiz = { version = "0.2.0", default-features = false }

With additional features:

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

Or use all features:

[dependencies]
oxiz = { version = "0.2.0", 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
std	Standard library support	Yes
nlsat	Nonlinear real arithmetic (implies std)
optimization	MaxSMT and optimization (implies std)
spacer	CHC solver (implies std)
proof	Proof generation (implies std)
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

Re-exports

pub use oxiz_core as core;

pub use oxiz_math as math;

pub use oxiz_sat as sat;

pub use oxiz_solver as solver;

pub use oxiz_theories as theories;

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

Modules

easystd

Simplified high-level API for common SMT solving use cases.

resource_limits

Resource limits and monitoring for the SMT solver.

Structs

Solver

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

SolverResult

Result of SMT solving

Constants

VERSION

Current version of OxiZ