nibli_types/
arithmetic.rs

1//! Built-in arithmetic for the engine's three native compute predicates.
2//!
3//! `pilji` (multiply), `sumji` (add), and `dilcu` (divide) each assert the
4//! relation `x1 = x2 op x3`. This is the SINGLE shared evaluation used by both
5//! the nibli-reason engine fast path (compiled into the WASM guest) and the nibli-host host
6//! fast path — `nibli-types` is the one crate both depend on. The Python
7//! reference backend (`python/nibli_backend.py`) mirrors the same semantics.
8
9/// Evaluate a built-in arithmetic predicate `x1 = x2 op x3` over three numbers.
10///
11/// Returns `Some(true|false)` for `pilji`/`sumji`/`dilcu` given at least three
12/// arguments, and `None` otherwise (unknown relation or too few args) so the
13/// caller falls through to the external compute backend.
14///
15/// Equality is TOLERANT (`isclose`, rel_tol `1e-9`), so decimal queries such as
16/// `0.3 = 0.1 + 0.2` answer TRUE despite IEEE-754 rounding — the engine, the
17/// host, and the Python backend all agree. The `dilcu` divide-by-zero check is an
18/// exact `== 0.0` guard (a guard, not a result comparison).
19pub fn eval_arithmetic(relation: &str, args: &[f64]) -> Option<bool> {
20    let (&x1, &x2, &x3) = (args.first()?, args.get(1)?, args.get(2)?);
21    // A non-finite operand (a literal too large for an f64 overflows to ±inf) makes the
22    // relation meaningless — DECLINE (None) rather than return a confident TRUE/FALSE.
23    // nibli-reason turns this into `Unknown(NonFinite)`; the nibli-host host fast path declines too.
24    let nonfinite_operand = !x1.is_finite() || !x2.is_finite() || !x3.is_finite();
25    let result = match relation {
26        "product" => x2 * x3,
27        "sum" => x2 + x3,
28        "quotient" => {
29            if x3 == 0.0 {
30                // Divide-by-zero (exact guard): never equal — but only DECIDE that for
31                // finite operands; with a non-finite operand it is the undetermined case.
32                return if nonfinite_operand { None } else { Some(false) };
33            }
34            x2 / x3
35        }
36        _ => return None,
37    };
38    // Even finite operands can overflow (e.g. `1e200 * 1e200 -> inf`); an out-of-range
39    // result is equally undetermined.
40    if nonfinite_operand || !result.is_finite() {
41        return None;
42    }
43    Some(isclose(x1, result))
44}
45
46/// Tolerant float equality, mirroring Python `math.isclose(a, b, rel_tol=1e-9,
47/// abs_tol=0.0)`: `|a - b| <= 1e-9 * max(|a|, |b|)`. (With `abs_tol = 0`, `0.0`
48/// is close only to exactly `0.0`, matching the reference.)
49fn isclose(a: f64, b: f64) -> bool {
50    (a - b).abs() <= 1e-9 * a.abs().max(b.abs())
51}
52
53#[cfg(test)]
54mod tests {
55    use super::eval_arithmetic;
56
57    #[test]
58    fn integer_cases_exact() {
59        // Conformance: the evaluator's domain is exactly relations::BUILTIN_ARITHMETIC
60        // (the single-source name sets) — comparisons are NOT tolerant arithmetic.
61        for r in crate::relations::BUILTIN_ARITHMETIC {
62            assert!(
63                eval_arithmetic(r, &[6.0, 2.0, 3.0]).is_some(),
64                "{r} must be evaluable"
65            );
66        }
67        for r in crate::relations::NUMERIC_COMPARISONS {
68            assert!(
69                eval_arithmetic(r, &[6.0, 2.0, 3.0]).is_none(),
70                "{r} must not be tolerant arithmetic"
71            );
72        }
73        assert_eq!(eval_arithmetic("product", &[6.0, 2.0, 3.0]), Some(true)); // 6 = 2*3
74        assert_eq!(eval_arithmetic("product", &[7.0, 2.0, 3.0]), Some(false));
75        assert_eq!(eval_arithmetic("sum", &[5.0, 2.0, 3.0]), Some(true)); // 5 = 2+3
76        assert_eq!(eval_arithmetic("sum", &[4.0, 2.0, 3.0]), Some(false));
77        assert_eq!(eval_arithmetic("quotient", &[3.0, 6.0, 2.0]), Some(true)); // 3 = 6/2
78    }
79
80    #[test]
81    fn float_tolerance_headline() {
82        // 0.1 + 0.2 = 0.30000000000000004 in IEEE-754; exact `==` would say
83        // FALSE, but the user means 0.3 — isclose makes it TRUE.
84        assert_eq!(eval_arithmetic("sum", &[0.3, 0.1, 0.2]), Some(true));
85        // A genuinely-wrong claim is still FALSE (the tolerance is tiny).
86        assert_eq!(eval_arithmetic("sum", &[0.4, 0.1, 0.2]), Some(false));
87        // Product with rounding: 0.1 * 0.1 = 0.010000000000000002.
88        assert_eq!(eval_arithmetic("product", &[0.01, 0.1, 0.1]), Some(true));
89    }
90
91    #[test]
92    fn dilcu_divide_by_zero_is_false_not_none() {
93        assert_eq!(eval_arithmetic("quotient", &[0.0, 5.0, 0.0]), Some(false));
94    }
95
96    #[test]
97    fn non_finite_operand_or_result_declines() {
98        let inf = f64::INFINITY;
99        // A non-finite operand makes the relation undetermined → None (nibli-reason surfaces
100        // Unknown(NonFinite)); never a confident TRUE/FALSE.
101        assert_eq!(eval_arithmetic("sum", &[inf, inf, 1.0]), None);
102        assert_eq!(eval_arithmetic("product", &[1.0, inf, 2.0]), None);
103        assert_eq!(eval_arithmetic("quotient", &[1.0, inf, 2.0]), None);
104        assert_eq!(eval_arithmetic("sum", &[f64::NAN, 1.0, 2.0]), None);
105        // Finite operands whose product overflows to ±inf are equally undetermined.
106        assert_eq!(eval_arithmetic("product", &[1.0, 1e200, 1e200]), None);
107        // A divide-by-zero with FINITE operands is still a decided false (not None).
108        assert_eq!(eval_arithmetic("quotient", &[0.0, 5.0, 0.0]), Some(false));
109        // A non-finite operand on a divide-by-zero is undetermined, not a decided false.
110        assert_eq!(eval_arithmetic("quotient", &[inf, 5.0, 0.0]), None);
111    }
112
113    #[test]
114    fn unknown_relation_and_short_args_are_none() {
115        assert_eq!(eval_arithmetic("exponential", &[8.0, 2.0, 3.0]), None);
116        assert_eq!(eval_arithmetic("sum", &[5.0, 2.0]), None);
117    }
118}
nibli_types/arithmetic.rs

nibli_types/
arithmetic.rs
