smtlib

与 SMT 求解器交互的高级 API

如果您需要更多控制和更少的人机工程学，请查看用于构建 SMT-LIB 代码和直接与 SMT 求解器通信的低级 crate smtlib-lowlevel。

背景

模理论可满足性 (SMT) 是确定数学公式是否可满足的问题。SMT 求解器（如 Z3 和 cvc5）是自动化此过程的程序。这些是功能强大的工具，可以高效地解决复杂问题。

为了与求解器通信，已经制定了 SMT-LIB 规范，以标准化所有求解器的输入/输出语言。

手动编写此格式（或“手动编程”）有时会很繁琐且容易出错。更不用说解释求解器产生的结果了。

因此，smtlib（以及 smtlib-lowlevel）的目标是提供与求解器通信的便捷 API，独立于具体的求解器。

用法

使用 smtlib 的主要方式是通过构建一个 smtlib::Solver。求解器接受一个 smtlib::Backend 作为参数。要查看库中提供的后端，请查看 smtlib::backend 模块。某些后端可能隐藏在功能标志之后，例如，要使用 Z3 静态后端，请通过运行 cargo add smtlib -F z3-static 安装 smtlib，否则通过运行

cargo add smtlib

现在您可以在您的项目中使用此库。

use smtlib::{backend::z3_binary::Z3Binary, Int, SatResultWithModel, Solver, Sort};

fn main() -> Result<(), Box<dyn std::error::Error>> {
    // Initialize the solver with the Z3 backend. The "z3" string refers the
    // to location of the already installed `z3` binary. In this case, the
    // binary is in the path.
    let mut solver = Solver::new(Z3Binary::new("z3")?)?;

    // Declare two new variables
    let x = Int::from_name("x");
    let y = Int::from_name("y");

    // Assert some constraints. This tells the solver that these expressions
    // must be true, so any solution will satisfy these.
    solver.assert(x._eq(y + 25))?;
    solver.assert(x._eq(204))?;
    // The constraints are thus:
    // - x == y + 25
    // - x == 204
    // Note that we use `a._eq(b)` rather than `a == b`, since we want to
    // express the mathematical relation of `a` and `b`, while `a == b` checks
    // that the two **expressions** are structurally the same.

    // Check for validity
    match solver.check_sat_with_model()? {
        SatResultWithModel::Sat(model) => {
            // Since it is valid, we can extract the possible values of the
            // variables using a model
            println!("x = {}", model.eval(x).unwrap());
            println!("y = {}", model.eval(y).unwrap());
        }
        SatResultWithModel::Unsat => println!("No valid solutions found!"),
        SatResultWithModel::Unknown => println!("Satisfaction remains unknown..."),
    }

    Ok(())
}