Crate oxiz_solver 

OxiZ Solver - Main CDCL(T) SMT Solver

This crate provides the main solver API that orchestrates:

• SAT core (CDCL)
• Theory solvers (EUF, LRA, LIA, BV)
• Tactic framework
• Parallel portfolio solving

Examples

Basic Boolean Satisfiability

use oxiz_solver::{Solver, SolverResult};
use oxiz_core::ast::TermManager;

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

// Create boolean variables
let p = tm.mk_var("p", tm.sorts.bool_sort);
let q = tm.mk_var("q", tm.sorts.bool_sort);

// Assert p AND q
let formula = tm.mk_and(vec![p, q]);
solver.assert(formula, &mut tm);

// Check satisfiability
match solver.check(&mut tm) {
    SolverResult::Sat => println!("Satisfiable!"),
    SolverResult::Unsat => println!("Unsatisfiable!"),
    SolverResult::Unknown => println!("Unknown"),
}

Integer Arithmetic

use oxiz_solver::{Solver, SolverResult};
use oxiz_core::ast::TermManager;
use num_bigint::BigInt;

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

solver.set_logic("QF_LIA");

// Create integer variable
let x = tm.mk_var("x", tm.sorts.int_sort);

// Assert: x >= 5 AND x <= 10
let five = tm.mk_int(BigInt::from(5));
let ten = tm.mk_int(BigInt::from(10));
solver.assert(tm.mk_ge(x, five), &mut tm);
solver.assert(tm.mk_le(x, ten), &mut tm);

// Should be satisfiable
assert_eq!(solver.check(&mut tm), SolverResult::Sat);

Incremental Solving with Push/Pop

use oxiz_solver::{Solver, SolverResult};
use oxiz_core::ast::TermManager;

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

let p = tm.mk_var("p", tm.sorts.bool_sort);
solver.assert(p, &mut tm);

// Push a new scope
solver.push();
let q = tm.mk_var("q", tm.sorts.bool_sort);
solver.assert(q, &mut tm);
assert_eq!(solver.check(&mut tm), SolverResult::Sat);

// Pop back to previous scope
solver.pop();
assert_eq!(solver.check(&mut tm), SolverResult::Sat);

Modules

combination

Theory Combination.

conflict

Conflict Analysis and Minimization.

delayed_combination

Delayed Theory Combination.

mbqi

Model-Based Quantifier Instantiation (MBQI)

model

Model Building for SMT Solvers.

propagation

Propagation subsystem.

propagation_pipeline

Multi-Level Propagation Pipeline.

shared_terms

Shared Terms Management for Theory Combination.

Macros

completion_error

Macro for creating a model completion error

finder_error

Macro for creating a finder error

instantiation

Macro for creating an instantiation

mbqi_debug

Macro for debugging MBQI state

mbqi_time

Macro for timing MBQI operations

mbqi_trace

Macro for MBQI tracing

quantifier

Macro for creating a quantified formula with default parameters

Structs

Context

Solver context for managing the solving process

EqualityNotification

Equality notification for Nelson-Oppen theory combination When one theory derives that two terms are equal, it notifies other theories

Model

A model (assignment to variables)

NelsonOppenCombiner

Nelson-Oppen theory combination engine.

NelsonOppenStats

Nelson-Oppen statistics

Objective

An optimization objective

Optimizer

Optimizer for SMT formulas with objectives

ParetoPoint

A Pareto-optimal solution (for multi-objective optimization)

Proof

A proof of unsatisfiability

Solver

Main CDCL(T) SMT Solver

SolverConfig

Solver configuration

SolverStats

Statistics for the solver

TheoryId

Theory identifier

Enums

ObjectiveKind

Optimization objective type

OptimizationResult

Result of optimization

ProofStep

Proof step for resolution-based proofs

RestartStrategy

Restart strategy

SolverResult

Result of SMT solving

TheoryMode

Theory checking mode

Traits

TheoryCombination

Interface for theory combination via Nelson-Oppen Theories implement this to participate in equality sharing