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);

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

Instantiation

An instantiation of a quantified formula

MBQISolver

Model-Based Quantifier Instantiation solver

MBQIStats

Statistics about MBQI

Model

A model (assignment to variables)

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

QuantifiedFormula

A quantified formula tracked by MBQI

Solver

Main CDCL(T) SMT Solver

SolverConfig

Solver configuration

SolverStats

Statistics for the solver

Enums

MBQIResult

Result of MBQI check

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