rz3 0.1.2

Deterministic, exact-rational SMT solver in pure Rust (DPLL(T)/CDCL) with a complete 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


use rz3::parser::Parser;

#[test]
fn test_parse_declare_fun_params() {
    let input = "(declare-fun f ((x Real) (y Real)) Real)";
    let mut parser = Parser::new(input);
    let _cmd = parser.parse_command().unwrap();
    // This should work with the current implementation if it parses 
    // but we need to check if it properly handles the parameters.
    // Currently, it only handles empty params () and ignores them.
    // I should assert what it should do, but for now, let's see if it parses.
}