关于

easy-smt 是一个用于与 SMT 求解器子进程交互的 crate。此 crate 提供了以下 API：

• 使用 SMT-LIB 2 语言 构建表达式和断言，
• 查询 SMT 求解器以获取这些断言的解，
• 并检查求解器的结果。

easy-smt 可以与任何求解器一起工作，只要求解器有交互式 REPL 模式。您只需告诉 easy-smt 如何启动子进程。

示例

use easy_smt::{ContextBuilder, Response};

fn main() -> std::io::Result<()> {
    // Create a new context, backed by a Z3 subprocess.
    let mut ctx = ContextBuilder::new()
        .solver("z3", ["-smt2", "-in"])
        .build()?;

    // Declare `x` and `y` variables that are bitvectors of width 32.
    let bv32 = ctx.bit_vec_sort(ctx.numeral(32));
    let x = ctx.declare_const("x", bv32)?;
    let y = ctx.declare_const("y", bv32)?;

    // Assert that `x * y = 18`.
    ctx.assert(ctx.eq(
        ctx.bvmul(x, y),
        ctx.binary(32, 18),
    ))?;

    // And assert that neither `x` nor `y` is 1.
    ctx.assert(ctx.not(ctx.eq(x, ctx.binary(32, 1))))?;
    ctx.assert(ctx.not(ctx.eq(y, ctx.binary(32, 1))))?;

    // Check whether the assertions are satisfiable. They should be in this example.
    assert_eq!(ctx.check()?, Response::Sat);

    // Print the solution!
    let solution = ctx.get_value(vec![x, y])?;
    for (variable, value) in solution {
        println!("{} = {}", ctx.display(variable), ctx.display(value));
    }
    // There are many solutions, but the one I get from Z3 is:
    //
    //     x = #x10000012
    //     y = #x38000001
    //
    // Solvers are great at finding edge cases and surprising-to-humans results! In
    // this case, I would have naively expected something like `x = 2, y = 9` or
    // `x = 3, y = 6`, but the solver found a solution where the multiplication
    // wraps around. Neat!
    Ok(())
}

调试

显示 S-表达式

想要显示您构建的 S-表达式以确保它是您期望的内容？您可以使用 easy_smt::Context::display 方法

use easy_smt::ContextBuilder;

let ctx = ContextBuilder::new().build().unwrap();

let my_s_expr = ctx.list(vec![
    ctx.atom("hi"),
    ctx.atom("hello"),
    ctx.numeral(42),
]);

let string = format!("{}", ctx.display(my_s_expr));
assert_eq!(string, "(hi hello 42)");

记录求解器交互

需要调试底层求解器收到的确切内容？easy-smt 使用 log crate 并在 TRACE 日志级别记录与求解器的所有通信。

例如，您可以使用 env_logger 来查看日志消息。在 main 的开始处初始化日志记录器

fn main() {
    env_logger::init();

    // ...
}

然后运行您的程序，将环境变量 RUST_LOG="easy_smt=trace" 设置为查看 TRACE 日志

$ RUST_LOG="easy_smt=trace" cargo run --example sudoku
[2023-01-09T23:41:05Z TRACE easy_smt::solver] -> (set-option :print-success true)
[2023-01-09T23:41:05Z TRACE easy_smt::solver] <- success
[2023-01-09T23:41:05Z TRACE easy_smt::solver] -> (set-option :produce-models true)
[2023-01-09T23:41:05Z TRACE easy_smt::solver] <- success
[2023-01-09T23:41:05Z TRACE easy_smt::solver] -> (set-option :produce-unsat-cores true)
[2023-01-09T23:41:05Z TRACE easy_smt::solver] <- success
[2023-01-09T23:41:05Z TRACE easy_smt::solver] -> (declare-fun cell_0_0 () Int)
[2023-01-09T23:41:05Z TRACE easy_smt::solver] <- success
[2023-01-09T23:41:05Z TRACE easy_smt::solver] -> (assert (and (> cell_0_0 0) (<= cell_0_0 9)))
[2023-01-09T23:41:05Z TRACE easy_smt::solver] <- success
[2023-01-09T23:41:05Z TRACE easy_smt::solver] -> (declare-fun cell_0_1 () Int)
[2023-01-09T23:41:05Z TRACE easy_smt::solver] <- success
[2023-01-09T23:41:05Z TRACE easy_smt::solver] -> (assert (and (> cell_0_1 0) (<= cell_0_1 9)))
[2023-01-09T23:41:05Z TRACE easy_smt::solver] <- success
...

use easy_smt::ContextBuilder;

fn main() -> std::io::Result<()> {
    let ctx = ContextBuilder::new()
        // Everything needed to replay the solver session will be written
        // to `replay.smt2`.
        .replay_file(Some(std::fs::File::create("replay.smt2")?))
        .solver("z3", ["-smt2", "-in"])
        .build()?;

    // ...

    Ok(())
}