litex/verify/verify_builtin_rules/
number_compare_div_elimination.rs

1use crate::prelude::*;
2use crate::rational_expression::mul_signed_decimal_str;
3
4use super::number_compare::{compare_number_strings, NumberCompareResult};
5
6fn decimal_str_sign_vs_zero(number_value: &str) -> NumberCompareResult {
7    compare_number_strings(number_value.trim(), "0")
8}
9
10// None if denominator is zero; Some(false) positive; Some(true) negative (flip inequality).
11fn nonzero_denominator_requires_flip(denominator_normalized: &str) -> Option<bool> {
12    match decimal_str_sign_vs_zero(denominator_normalized) {
13        NumberCompareResult::Equal => None,
14        NumberCompareResult::Greater => Some(false),
15        NumberCompareResult::Less => Some(true),
16    }
17}
18
19// None if either denominator is zero; Some(true) if v*y > 0; Some(false) if v*y < 0.
20fn two_denominators_product_is_positive(left_den: &str, right_den: &str) -> Option<bool> {
21    let l = decimal_str_sign_vs_zero(left_den);
22    let r = decimal_str_sign_vs_zero(right_den);
23    match (l, r) {
24        (NumberCompareResult::Equal, _) | (_, NumberCompareResult::Equal) => None,
25        (NumberCompareResult::Less, NumberCompareResult::Less)
26        | (NumberCompareResult::Greater, NumberCompareResult::Greater) => Some(true),
27        _ => Some(false),
28    }
29}
30
31fn compare_result_matches_less_order(
32    compare_result: NumberCompareResult,
33    allow_equal: bool,
34    flip: bool,
35) -> bool {
36    if !flip {
37        if allow_equal {
38            matches!(
39                compare_result,
40                NumberCompareResult::Less | NumberCompareResult::Equal
41            )
42        } else {
43            matches!(compare_result, NumberCompareResult::Less)
44        }
45    } else if allow_equal {
46        matches!(
47            compare_result,
48            NumberCompareResult::Greater | NumberCompareResult::Equal
49        )
50    } else {
51        matches!(compare_result, NumberCompareResult::Greater)
52    }
53}
54
55impl Runtime {
56    pub fn try_verify_numeric_order_via_div_elimination(
57        &self,
58        left_obj: &Obj,
59        right_obj: &Obj,
60        allow_equal: bool,
61    ) -> Option<bool> {
62        if let (Obj::Div(left_div), Obj::Div(right_div)) = (left_obj, right_obj) {
63            let left_denominator_number = self.resolve_obj_to_number_resolved(&left_div.right)?;
64            let right_denominator_number = self.resolve_obj_to_number_resolved(&right_div.right)?;
65            let left_den_str = left_denominator_number.normalized_value.as_str();
66            let right_den_str = right_denominator_number.normalized_value.as_str();
67            let product_positive =
68                two_denominators_product_is_positive(left_den_str, right_den_str)?;
69            let flip = !product_positive;
70            let left_numerator_number = self.resolve_obj_to_number_resolved(&left_div.left)?;
71            let right_numerator_number = self.resolve_obj_to_number_resolved(&right_div.left)?;
72            let left_product = mul_signed_decimal_str(
73                &left_numerator_number.normalized_value,
74                &right_denominator_number.normalized_value,
75            );
76            let right_product = mul_signed_decimal_str(
77                &right_numerator_number.normalized_value,
78                &left_denominator_number.normalized_value,
79            );
80            let compare_result = compare_number_strings(&left_product, &right_product);
81            return Some(compare_result_matches_less_order(
82                compare_result,
83                allow_equal,
84                flip,
85            ));
86        }
87
88        if let Obj::Div(right_div) = right_obj {
89            let denominator_number = self.resolve_obj_to_number_resolved(&right_div.right)?;
90            let flip = nonzero_denominator_requires_flip(&denominator_number.normalized_value)?;
91            let numerator_number = self.resolve_obj_to_number_resolved(&right_div.left)?;
92            let left_number = self.resolve_obj_to_number_resolved(left_obj)?;
93            let left_scaled = mul_signed_decimal_str(
94                &left_number.normalized_value,
95                &denominator_number.normalized_value,
96            );
97            let compare_result =
98                compare_number_strings(&left_scaled, &numerator_number.normalized_value);
99            return Some(compare_result_matches_less_order(
100                compare_result,
101                allow_equal,
102                flip,
103            ));
104        }
105
106        if let Obj::Div(left_div) = left_obj {
107            let denominator_number = self.resolve_obj_to_number_resolved(&left_div.right)?;
108            let flip = nonzero_denominator_requires_flip(&denominator_number.normalized_value)?;
109            let numerator_number = self.resolve_obj_to_number_resolved(&left_div.left)?;
110            let right_number = self.resolve_obj_to_number_resolved(right_obj)?;
111            let right_scaled = mul_signed_decimal_str(
112                &right_number.normalized_value,
113                &denominator_number.normalized_value,
114            );
115            let compare_result =
116                compare_number_strings(&numerator_number.normalized_value, &right_scaled);
117            return Some(compare_result_matches_less_order(
118                compare_result,
119                allow_equal,
120                flip,
121            ));
122        }
123
124        None
125    }
126}
litex/verify/verify_builtin_rules/number_compare_div_elimination.rs

litex/verify/verify_builtin_rules/
number_compare_div_elimination.rs
