Lib.rs

› 开发工具 › 过程宏
#z3 #solver #smt-solver #smt #satisfiability #api-bindings

nightly macro z3d

Z3 DSL接口用于Rust

作者：Alex Chew

1个不稳定版本

0.1.0 2019年10月7日

611 在 过程宏 中

MIT 许可证

41KB
1K SLoC

Z3D — Rust的Z3 DSL接口

Z3D (简称"Z3 DSL") 是一个Rust接口，用于Z3定理证明器。它提供了两个宏 — dec! 和 exp! — 分别允许用户以自然DSL编写Z3常量（变量）声明和断言表达式。

由于Rust宏将源代码（在DSL中）展开为源代码（在普通Z3代码中），并且宏展开为与Z3D相同的不带Z3D的普通Z3代码，因此Z3D具有零运行时开销。

免责声明： Z3D是一个实验性项目，尚未经过充分测试。它应被视为alpha级软件。

示例

在这里，我们将演示Z3D的使用，将其API与z3包（提供底层高级Z3绑定）的API进行比较。以下每个示例中，我们将假设以下设置

use z3::{Config, Context, Solver};  // basic Z3 interfaces from the z3 package
use z3d::{dec, exp};                // Z3D declaration and expression macros, respectively

let ctx = &Context::new(&Config::default());   // we declare constants in a Context
let solver = Solver::new(ctx);                 // we make assertions in a Solver

（以下示例及其实现改编自Dennis Yurichev关于实用SMT求解器使用的优秀文档，题为“通过示例的SAT/SMT”。其最新版本可在此处找到）。

数独

让我们解决一个数独谜题。首先，我们将声明常量来表示棋盘的cells，并约束任何known_values。

let cells: [[z3::ast::BV; 9]; 9] = ...;
for rr in 0..9 {
    for cc in 0..9 {
        // using z3d
        cells[rr][cc] = dec!($("cell_{}_{}", rr, cc): bitvec<16> in ctx);
        //                   ^^^^^^^^^^^^^^^^^^^^^^^
        //                   ^ format constant names using $(...)

        // using z3
        cells[rr][cc] = z3::ast::BV::new_const(ctx, format!("cell_{}_{}", rr, cc), 16));

        if let Some(val) = known_values[rr][cc] {
            // using z3d
            solver.assert(&exp!({cells[rr][cc]} == (val as bitvec<16>) in ctx));
            //                   ^^^^^^^^^^^^^      ^^^^^^^^^^^^^^^^^
            //     arbitrary Rust expression ^      ^ cast to bitvector

            // using z3
            solver.assert(&cells[rr][cc]._eq(&ctx.bitvector_sort(16).from_i64(val)));
        }
    }
}

接下来，我们强制每个行、列和3x3方块的单元格值唯一（这里我们只展示行i中的唯一性，为了简洁）。注意使用变长bvor运算符，否则需要重复调用.bvor(...)。

// using z3d
let one = exp!(1 as bitvec<16> in ctx);
let mask = exp!(0b11_1111_1110 as bitvec<16> in ctx);
solver.assert(&exp!(bvor(    // variadic bvor
    one << {cells[i][0]},
    one << {cells[i][1]},
    one << {cells[i][2]},
    one << {cells[i][3]},
    one << {cells[i][4]},
    one << {cells[i][5]},
    one << {cells[i][6]},
    one << {cells[i][7]},
    one << {cells[i][8]}) == mask
in ctx));

// using z3
let one = z3::ast::BV::from_i64(ctx, 1, 16);
let mask = z3::ast::BV::from_i64(ctx, 0b11_1111_1110, 16);
solver.assert(
    &one.bvshl(&cells[i][0])
        .bvor(&one.bvshl(&cells[i][1]))     // repeated .bvor(...)
        .bvor(&one.bvshl(&cells[i][2]))
        .bvor(&one.bvshl(&cells[i][3]))
        .bvor(&one.bvshl(&cells[i][4]))
        .bvor(&one.bvshl(&cells[i][5]))
        .bvor(&one.bvshl(&cells[i][6]))
        .bvor(&one.bvshl(&cells[i][7]))
        .bvor(&one.bvshl(&cells[i][8]))
        ._eq(&mask),
);

然后，解决方案只需一个solver.get_model()即可。数独示例的完整源代码可在z3d-examples/src/bin/sudoku.rs中找到。

文字算术

让我们解决以下文字算术问题

  V I O L I N
  V I O L I N
+   V I O L A
-------------
  S O N A T A
+     T R I O

其中每个字母对应一个唯一的0-9数字，并且每个词的首位数字不为零。我们首先为每个字母和词声明常量

// using z3d
let num_a = dec!(a: int in ctx);
let num_i = dec!(i: int in ctx);
...
let num_v = dec!(v: int in ctx);
let violin = dec!(violin: int in ctx);
let viola = dec!(viola: int in ctx);
let sonata = dec!(sonata: int in ctx);
let trio = dec!(trio: int in ctx);

// using z3
let num_a = z3::ast::Int::new_const(ctx, "a");
let num_i = z3::ast::Int::new_const(ctx, "i");
...
let num_v = z3::ast::Int::new_const(ctx, "v");
let violin = z3::ast::Int::new_const(ctx, "violin");
let viola = z3::ast::Int::new_const(ctx, "viola");
let sonata = z3::ast::Int::new_const(ctx, "sonata");
let trio = z3::ast::Int::new_const(ctx, "trio");

然后我们断言字母编码了不同的0-9数字

// using z3d
solver.assert(&exp!(
    distinct(num_a, num_i, num_l, num_n, num_o, num_r, num_s, num_t, num_v) in ctx));
for num in &[&num_a, &num_i, &num_l, &num_n, &num_o, &num_r, &num_s, &num_t, &num_v] {
    solver.assert(&exp!((num >= 0) & (num <= 9) in ctx));
}

// using z3
solver.assert(&num_a.distinct(&[
    &num_i, &num_l, &num_n, &num_o, &num_r, &num_s, &num_t, &num_v,
]));
for num in &[&num_a, &num_i, &num_l, &num_n, &num_o, &num_r, &num_s, &num_t, &num_v] {
    solver.assert(
        &num.ge(&ast::Int::from_i64(ctx, 0))
            .and(&[&num.le(&ast::Int::from_i64(ctx, 9))]),
    );
}

然后我们断言字母形成了词（在算术意义上）

// using z3d
solver.assert(&exp!(
    add(
        num_v * 100000,
        num_i * 10000,
        num_o * 1000,
        num_l * 100,
        num_i * 10,
        num_n
    ) == violin
in ctx));
...

// using z3
solver.assert(
    &(num_v.mul(&[&ast::Int::from_i64(ctx, 100000)]))
        .add(&[
            &num_i.mul(&[&ast::Int::from_i64(ctx, 10000)]),
            &num_o.mul(&[&ast::Int::from_i64(ctx, 1000)]),
            &num_l.mul(&[&ast::Int::from_i64(ctx, 100)]),
            &num_i.mul(&[&ast::Int::from_i64(ctx, 10)]),
            &num_n,
        ])
        ._eq(&violin),
);
...

最后，我们断言词方程成立

// using z3d
solver.assert(&exp!(add(violin, violin, viola) == (trio + sonata) in ctx));

// using z3
solver.assert(&violin.add(&[&violin, &viola])._eq(&trio.add(&[&sonata])));

这个言语算术示例的完整源代码可在z3d-examples/src/bin/trio.rs中找到。

用法

Z3D已经使用nightly-x86_64-unknown-linux-gnu工具链进行了测试，特别是rustc 1.40.0-nightly (032a53a06 2019-10-03)。

本项目的唯一外部依赖是Z3；该项目已经与Ubuntu存储库中的libz3-dev版本4.4.0-5进行了测试。所有Rust依赖项均已在Cargo.toml中指定，并会使用以下列出的适当命令自动安装。

$ cargo build                               # install dependencies and build
$ cargo run --bin sudoku [ z3d | plain ]    # run the Sudoku example
$ cargo run --bin trio [ z3d | plain ]      # run the Trio example

每个示例都需要一个参数，即z3d或plain，以指示使用哪个实现（使用Z3D API或plain Z3绑定）。因此，很容易验证这两个实现的功能和性能是等效的。

路线图

dec!

  • 布尔、整数和位向量类型
  • 命名常量，具有名称格式化
  • 支持更多类型：实数、关系、函数、量词、ADT
  • 未命名常量

exp!

  • 原子：整数字符串、布尔字面量、Rust标识符
  • 常见的单目、双目和多目表达式
  • 接受AST迭代器的多目表达式
  • 运算符优先级和/或结合性

其他

  • 基本测试套件
  • 宏中的隐式ctx

依赖关系

~21MB
~465K SLoC