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

use rz3::parser::Parser;
use std::collections::hash_map::DefaultHasher;
use std::hash::{Hash, Hasher};

#[test]
fn test_parser_determinism() {
    let input = "(define-fun h ((x Real)) Real (ite (<= x 0.0) 0.0 x))";
    let mut outputs = Vec::new();

    for _ in 0..30 {
        let mut parser = Parser::new(input);
        let cmd = parser.parse_command().unwrap();
        // Since Command doesn't implement Hash, we hash its Debug representation
        let output_str = format!("{:?}", cmd);
        let mut hasher = DefaultHasher::new();
        output_str.hash(&mut hasher);
        outputs.push(hasher.finish());
    }

    // Check all are identical
    let first = outputs[0];
    for &o in &outputs[1..] {
        assert_eq!(first, o, "Parser output is not deterministic");
    }
}