Простое введение в z3

Изучение мира решателей ограничений на простых примерах.

Что такое решатели?

Решатели — это инструменты, которые принимают правила и ограничения, а затем находят решение. Они не всегда быстрее специальных алгоритмов, но гораздо гибче при изменении условий. Применяются для планирования, распределения ресурсов и других задач.

Терминология

В документации z3 много жаргона. Например, «Sort» означает тип, а «constants» — это переменные, которыми оперирует решатель. Solver работает со своим языком SMT-LIB2, а библиотеки переводят код в этот язык.

Простое уравнение

Решим уравнение x + 4 = 7. Вот код на Rust:

use z3::{Solver, ast::Int};
fn main() {
    let solver = Solver::new();
    let x = Int::new_const("x");
    solver.assert(&(x + 4).eq(&7));
    assert_eq!(solver.check(), SatResult::Sat);
    let model = solver.get_model().unwrap();
    println!("x = {}", model.eval(&x, true).unwrap());
}

Решатель находит x = 3. Это базовый пример, но он показывает принцип работы.