rz3 0.1.3

Deterministic, exact-rational SMT solver in pure Rust (DPLL(T)/CDCL) with an exact linear-arithmetic core. Zero C dependencies, WASM-deployable, reproducible run-to-run.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43

use rz3::ast::Expr;
use rz3::parser::Command;
use rz3::parser::Parser;

#[test]
fn test_parse_nested() {
    let mut parser = Parser::new("(<= (+ x (* y 2)) 10)");
    let expr = parser.parse_expr().unwrap();
    assert!(matches!(expr, Expr::Le(_, _)));
    let Expr::Le(lhs, rhs) = expr else {
        return;
    };
    assert!(matches!(*lhs, Expr::Add(_)));
    assert!(matches!(*rhs, Expr::Int(10)));
}

#[test]
fn test_parse_basic() {
    let mut parser = Parser::new("(<= (+ x y) 10)");
    let expr = parser.parse_expr().unwrap();
    assert!(matches!(expr, Expr::Le(_, _)));
    let Expr::Le(lhs, rhs) = expr else {
        return;
    };
    assert!(matches!(*lhs, Expr::Add(_)));
    let Expr::Add(args) = *lhs else {
        return;
    };
    assert_eq!(args.len(), 2);
    assert!(matches!(*rhs, Expr::Int(10)));
}

#[test]
fn test_parse_set_info() {
    let mut parser = Parser::new("(set-info :smt-lib-version 2.6)");
    let cmd = parser.parse_command().unwrap();
    assert!(matches!(cmd, Command::SetInfo(_, _)));
    let Command::SetInfo(key, value) = cmd else {
        return;
    };
    assert_eq!(key, ":smt-lib-version");
    assert_eq!(value, "2.6");
}