tract_data/dim/
assertion.rs

1use fmt::Display;
2
3use super::*;
4
5#[derive(Debug, PartialEq, Clone, Hash)]
6#[allow(clippy::upper_case_acronyms)]
7pub enum Assertion {
8    Eq(TDim, TDim),
9    LT(TDim, TDim),
10    GT(TDim, TDim),
11    LTE(TDim, TDim),
12    GTE(TDim, TDim),
13}
14
15impl Display for Assertion {
16    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
17        use Assertion::*;
18        match self {
19            Eq(l, r) => write!(f, "{l} == {r}"),
20            LT(l, r) => write!(f, "{l} < {r}"),
21            GT(l, r) => write!(f, "{l} > {r}"),
22            LTE(l, r) => write!(f, "{l} <= {r}"),
23            GTE(l, r) => write!(f, "{l} >= {r}"),
24        }
25    }
26}
27
28impl Assertion {
29    pub fn as_known_positive(&self) -> Option<TDim> {
30        use Assertion::*;
31        match self {
32            Eq(left, right) => Some(left.clone() - right),
33            GTE(left, right) => Some(left.clone() - right),
34            GT(left, right) => Some(left.clone() - 1 - right),
35            LTE(left, right) => Some(right.clone() - left),
36            LT(left, right) => Some(right.clone() - 1 - left),
37        }
38    }
39
40    pub fn check(&self, values: &SymbolValues) -> Option<bool> {
41        use Assertion::*;
42        match self {
43            Eq(left, right) => (left.eval(values) - right.eval(values)).as_i64().map(|d| d == 0),
44            GTE(left, right) => (left.eval(values) - right.eval(values)).as_i64().map(|d| d >= 0),
45            GT(left, right) => (left.eval(values) - right.eval(values)).as_i64().map(|d| d > 0),
46            LTE(left, right) => (left.eval(values) - right.eval(values)).as_i64().map(|d| d <= 0),
47            LT(left, right) => (left.eval(values) - right.eval(values)).as_i64().map(|d| d < 0),
48        }
49    }
50}
51
52#[cfg(test)]
53mod tests {
54    use super::*;
55    #[test]
56    fn use_equalities() {
57        let s = SymbolScope::default();
58        s.add_assertion("s==0").unwrap();
59        assert!(s.parse_tdim("s").unwrap().simplify().is_zero());
60    }
61
62    #[test]
63    fn prove_positive_with_axiom() {
64        let s = SymbolScope::default();
65        s.add_assertion("s>=0").unwrap();
66        assert!(s.parse_tdim("s").unwrap().prove_positive_or_zero());
67    }
68
69    #[test]
70    fn prove_positive_with_axiom_2() {
71        let s = SymbolScope::default();
72        s.add_assertion("s>=0").unwrap();
73        s.add_assertion("p>=0").unwrap();
74        s.add_assertion("p+s<4096").unwrap();
75        assert!(s.parse_tdim("4096-p").unwrap().prove_positive_or_zero());
76    }
77
78    #[test]
79    fn min_max_with_axiom() {
80        let symbols = SymbolScope::default();
81        symbols.add_assertion("a>=0").unwrap();
82        assert_eq!(symbols.parse_tdim("min(a,0)").unwrap().simplify(), 0.into());
83        assert_eq!(
84            symbols.parse_tdim("max(a,0)").unwrap().simplify(),
85            symbols.parse_tdim("a").unwrap()
86        );
87    }
88
89    #[test]
90    fn low_bound_0() -> TractResult<()> {
91        let symbols = SymbolScope::default().with_assertion("S>=0")?;
92        let s = symbols.parse_tdim("S").unwrap();
93        assert_eq!(s.low_inclusive_bound(), Some(0));
94        Ok(())
95    }
96
97    #[test]
98    fn low_bound_1() -> TractResult<()> {
99        let symbols = SymbolScope::default().with_assertion("S>0")?;
100        assert_eq!(symbols.parse_tdim("S").unwrap().low_inclusive_bound(), Some(1));
101        Ok(())
102    }
103
104    #[test]
105    fn low_bound_2() -> TractResult<()> {
106        let symbols = SymbolScope::default().with_assertion("S>0")?;
107        assert_eq!(symbols.parse_tdim("S + 1").unwrap().low_inclusive_bound(), Some(2));
108        Ok(())
109    }
110
111    #[test]
112    fn low_bound_3() -> TractResult<()> {
113        let symbols = SymbolScope::default().with_assertion("S>0")?;
114        assert_eq!(symbols.parse_tdim("4*S").unwrap().low_inclusive_bound(), Some(4));
115        Ok(())
116    }
117
118    #[test]
119    fn low_bound_4() -> TractResult<()> {
120        let symbols = SymbolScope::default().with_assertion("S>0")?.with_assertion("S>5")?;
121        assert_eq!(symbols.parse_tdim("S + 3").unwrap().low_inclusive_bound(), Some(9));
122        Ok(())
123    }
124
125    #[test]
126    fn max_bug_1() {
127        let symbols = SymbolScope::default();
128        symbols.add_assertion("S>8").unwrap();
129        assert_eq!(
130            symbols.parse_tdim("max(1,-1+(S+1)/4)").unwrap().simplify(),
131            symbols.parse_tdim("-1+(S+1)/4").unwrap(),
132        );
133    }
134
135    #[test]
136    fn min_bug_1() {
137        let symbols = SymbolScope::default();
138        symbols.add_assertion("S>8").unwrap();
139        assert_eq!(
140            symbols.parse_tdim("min(1,-1+(S+1)/4)").unwrap().simplify(),
141            symbols.parse_tdim("1").unwrap()
142        );
143    }
144
145    #[test]
146    fn min_bug_2() {
147        let symbols = SymbolScope::default();
148        symbols.add_assertion("S>50").unwrap();
149        assert_eq!(
150            symbols.parse_tdim("min(-3+2*(S+1)/4,-1+(S+1)/4)").unwrap().simplify(),
151            symbols.parse_tdim("-1+(S+1)/4").unwrap()
152        );
153    }
154
155    #[test]
156    fn min_bug_3() {
157        let symbols = SymbolScope::default();
158        symbols.add_assertion("S>=0").unwrap();
159        symbols.add_assertion("P>=0").unwrap();
160        assert_eq!(
161            symbols.parse_tdim("min(0,(S)#(P+S))").unwrap().simplify(),
162            symbols.parse_tdim("0").unwrap()
163        );
164    }
165
166    #[test]
167    fn guess_scenario() -> TractResult<()> {
168        let symbols = SymbolScope::default()
169            .with_assertion("S>=0")?
170            .with_assertion("P>=0")?
171            .with_scenario_assertion("tg", "S==1")?
172            .with_scenario_assertion("pp", "P==0")?;
173        let s = symbols.sym("S");
174        let p = symbols.sym("P");
175        assert_eq!(symbols.guess_scenario(&SymbolValues::default())?, None);
176        assert_eq!(symbols.guess_scenario(&SymbolValues::default().with(&s, 50))?, Some(1));
177        assert_eq!(symbols.guess_scenario(&SymbolValues::default().with(&p, 50))?, Some(0));
178        assert!(
179            symbols.guess_scenario(&SymbolValues::default().with(&p, 50).with(&s, 50)).is_err()
180        );
181        Ok(())
182    }
183
184    #[test]
185    fn min_llm_0() -> TractResult<()> {
186        let symbols = SymbolScope::default()
187            .with_assertion("S>=0")?
188            .with_assertion("P>=0")?
189            .with_scenario_assertion("tg", "S==1")?
190            .with_scenario_assertion("pp", "P==0")?;
191        assert_eq!(
192            symbols.parse_tdim("min(P,(S)#(P+S))").unwrap().simplify(),
193            symbols.parse_tdim("P").unwrap()
194        );
195        Ok(())
196    }
197}
tract_data/dim/assertion.rs

tract_data/dim/
assertion.rs
