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
44
45
46
47
48
49
50
51
52
53
54
55
56

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

#[test]
fn test_define_fun_basic() {
    let input = "(define-fun f () Int 1)";
    let mut parser = Parser::new(input);
    let cmd = parser.parse_command().unwrap();

    assert!(matches!(cmd, Command::DefineFun(_, _, _, _)));
    let Command::DefineFun(name, params, ret_type, body) = cmd else {
        return;
    };
    assert_eq!(name, "f");
    assert_eq!(params.len(), 0);
    assert_eq!(ret_type, Type::Int);
    assert_eq!(body, Expr::Int(1));
}

#[test]
fn test_define_fun_with_params() {
    let input = "(define-fun g ((x Int) (y Int)) Int (+ x y))";
    let mut parser = Parser::new(input);
    let cmd = parser.parse_command().unwrap();

    assert!(matches!(cmd, Command::DefineFun(_, _, _, _)));
    let Command::DefineFun(name, params, ret_type, _body) = cmd else {
        return;
    };
    assert_eq!(name, "g");
    assert_eq!(params.len(), 2);
    assert_eq!(params[0].0, "x");
    assert_eq!(params[0].1, Type::Int);
    assert_eq!(params[1].0, "y");
    assert_eq!(params[1].1, Type::Int);
    assert_eq!(ret_type, Type::Int);
}

#[test]
fn test_define_fun_complex() {
    let input = "(define-fun h ((x Real)) Real (ite (<= x 0.0) 0.0 x))";
    let mut parser = Parser::new(input);
    let cmd = parser.parse_command().unwrap();

    assert!(matches!(cmd, Command::DefineFun(_, _, _, _)));
    let Command::DefineFun(name, params, ret_type, _body) = cmd else {
        return;
    };
    assert_eq!(name, "h");
    assert_eq!(params.len(), 1);
    assert_eq!(params[0].0, "x");
    assert_eq!(params[0].1, Type::Real);
    assert_eq!(ret_type, Type::Real);
}