Struct Optimizer 

pub struct Optimizer { /* private fields */ }

Optimizer for SMT formulas with objectives

The optimizer extends the basic SMT solver with optimization capabilities, allowing you to minimize or maximize objectives subject to constraints.

Examples

Basic Minimization

use oxiz_solver::{Optimizer, OptimizationResult};
use oxiz_core::ast::TermManager;
use num_bigint::BigInt;

let mut opt = Optimizer::new();
let mut tm = TermManager::new();

opt.set_logic("QF_LIA");

let x = tm.mk_var("x", tm.sorts.int_sort);
let five = tm.mk_int(BigInt::from(5));
opt.assert(tm.mk_ge(x, five));

// Minimize x (should be 5)
opt.minimize(x);
let result = opt.optimize(&mut tm);

match result {
    OptimizationResult::Optimal { .. } => println!("Found optimal solution"),
    _ => println!("No optimal solution"),
}

Lexicographic Optimization

use oxiz_solver::{Optimizer, OptimizationResult};
use oxiz_core::ast::TermManager;
use num_bigint::BigInt;

let mut opt = Optimizer::new();
let mut tm = TermManager::new();

opt.set_logic("QF_LIA");

let x = tm.mk_var("x", tm.sorts.int_sort);
let y = tm.mk_var("y", tm.sorts.int_sort);
let zero = tm.mk_int(BigInt::from(0));
let ten = tm.mk_int(BigInt::from(10));

opt.assert(tm.mk_ge(x, zero));
let zero_y = tm.mk_int(BigInt::from(0));
opt.assert(tm.mk_ge(y, zero_y));
let sum = tm.mk_add(vec![x, y]);
opt.assert(tm.mk_ge(sum, ten));

// Minimize x first, then y
opt.minimize(x);
opt.minimize(y);

let _result = opt.optimize(&mut tm);

Implementations

impl Optimizer

pub fn new() -> Self

Create a new optimizer

pub fn assert(&mut self, term: TermId)

Add an assertion

pub fn minimize(&mut self, term: TermId)

Add a minimization objective

pub fn maximize(&mut self, term: TermId)

Add a maximization objective

pub fn set_logic(&mut self, logic: &str)

Set logic

pub fn push(&mut self)

Push a scope

pub fn pop(&mut self)

Pop a scope

pub fn optimize(&mut self, term_manager: &mut TermManager) -> OptimizationResult

Check satisfiability and optimize objectives

Uses linear search with binary search refinement for integer objectives. For lexicographic optimization, processes objectives in priority order.

impl Optimizer

pub fn pareto_optimize( &mut self, term_manager: &mut TermManager, ) -> Vec<ParetoPoint>

Find Pareto-optimal solutions for multi-objective optimization

This implements a simple iterative approach:

1. Find an initial solution
2. Add constraints to exclude dominated solutions
3. Repeat until no more solutions exist

Note: This can be expensive for problems with many Pareto-optimal points

Trait Implementations

impl Debug for Optimizer

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for Optimizer

fn default() -> Self

Returns the “default value” for a type.