安装

1. 安装 Rust: Rust
2. 安装 clang

    xxx@XXX:~$ sudo apt install clang
   

3. 安装 SMT-Language

    xxx@XXX:~$ cargo install smt-lang
   

运行 SMT-language

xxx@XXX:~$ smt-lang --file problem_file.sl

示例

问题

let b: Bool
let i: 1..100
let r: Real

constraint C1 = (
    i >= 10
)
constraint C2 = (
    r <= 20.0 and b
)

解决

xxx@XXX:~$ smt-lang --file example.sl

解决方案

let b: Bool = true
let i: 1..100 = 10
let r: Real = 20

选项

详细

• --verbose 0 : 只显示结果
• --verbose 1 : 显示分析结果
• --verbose 2 : 显示加载的问题
• --verbose 3 : 如果找到解决方案，显示 SMT 问题和 SMT 模型

语法

• 文档