1use crate::interval::{Dyadic, Iv};
29use crate::numeric::Rational;
30use crate::poly::Poly;
31
32#[derive(Clone, Debug, PartialEq, Eq)]
34pub struct Monomial {
35 pub coefficient: Rational,
36 pub powers: Vec<u32>,
37}
38
39#[derive(Clone, Debug, PartialEq, Eq)]
41pub struct Field {
42 pub components: Vec<Vec<Monomial>>,
43}
44
45#[derive(Clone, Debug, PartialEq, Eq)]
47pub enum FlowError {
48 Escapes,
50 Shape,
52}
53
54impl Field {
55 pub fn dimension(&self) -> usize {
56 self.components.len()
57 }
58
59 fn well_formed(&self) -> bool {
60 let n = self.dimension();
61 n > 0
62 && self
63 .components
64 .iter()
65 .all(|c| c.iter().all(|m| m.powers.len() == n))
66 }
67
68 fn eval(&self, x: &[Iv], q: i64) -> Vec<Iv> {
70 self.components
71 .iter()
72 .map(|monomials| {
73 let mut total = Iv::point(Dyadic::zero());
74 for m in monomials {
75 let mut term = rational_iv(&m.coefficient, q);
76 for (i, &e) in m.powers.iter().enumerate() {
77 for _ in 0..e {
78 term = term.mul(&x[i]).round_out(q);
79 }
80 }
81 total = total.add(&term).round_out(q);
82 }
83 total
84 })
85 .collect()
86 }
87}
88
89fn rational_iv(r: &Rational, q: i64) -> Iv {
91 Iv {
92 lo: Dyadic::from_rational_floor(r, q),
93 hi: Dyadic::from_rational_ceil(r, q),
94 }
95}
96
97fn div_int(x: &Iv, k: i64, q: i64) -> Iv {
99 let k = Rational::from_i64(k);
100 let lo = x.lo.to_rational().div(&k).expect("k > 0");
101 let hi = x.hi.to_rational().div(&k).expect("k > 0");
102 Iv {
103 lo: Dyadic::from_rational_floor(&lo, q),
104 hi: Dyadic::from_rational_ceil(&hi, q),
105 }
106}
107
108fn subset(inner: &Iv, outer: &Iv) -> bool {
109 inner.lo.cmp(&outer.lo) != std::cmp::Ordering::Less && inner.hi.cmp(&outer.hi) != std::cmp::Ordering::Greater
110}
111
112struct Series<'f> {
114 field: &'f Field,
115 factors: Vec<Vec<Vec<usize>>>,
117 coefficients: Vec<Vec<Iv>>,
118 x: Vec<Vec<Iv>>,
120 partial: Vec<Vec<Vec<Vec<Iv>>>>,
122 q: i64,
123}
124
125impl<'f> Series<'f> {
126 fn new(field: &'f Field, start: &[Iv], q: i64) -> Series<'f> {
127 let factors: Vec<Vec<Vec<usize>>> = field
128 .components
129 .iter()
130 .map(|monomials| {
131 monomials
132 .iter()
133 .map(|m| {
134 m.powers
135 .iter()
136 .enumerate()
137 .flat_map(|(i, &e)| std::iter::repeat(i).take(e as usize))
138 .collect()
139 })
140 .collect()
141 })
142 .collect();
143 let coefficients = field
144 .components
145 .iter()
146 .map(|monomials| monomials.iter().map(|m| rational_iv(&m.coefficient, q)).collect())
147 .collect();
148 let partial = factors
149 .iter()
150 .map(|monomials| monomials.iter().map(|f| vec![Vec::new(); f.len()]).collect())
151 .collect();
152 Series {
153 field,
154 factors,
155 coefficients,
156 x: start.iter().map(|s| vec![s.clone()]).collect(),
157 partial,
158 q,
159 }
160 }
161
162 fn extend(&mut self) {
164 let j = self.x[0].len() - 1;
165 let q = self.q;
166 let mut next = Vec::with_capacity(self.field.dimension());
167 for c in 0..self.field.dimension() {
168 let mut total = Iv::point(Dyadic::zero());
169 for (k, factors) in self.factors[c].iter().enumerate() {
170 let value = if factors.is_empty() {
171 if j == 0 {
172 self.coefficients[c][k].clone()
173 } else {
174 Iv::point(Dyadic::zero())
175 }
176 } else {
177 for m in 0..factors.len() {
178 let coefficient = if m == 0 {
179 self.x[factors[0]][j].clone()
180 } else {
181 let mut sum = Iv::point(Dyadic::zero());
182 for i in 0..=j {
183 let product = self.partial[c][k][m - 1][i].mul(&self.x[factors[m]][j - i]);
184 sum = sum.add(&product).round_out(q);
185 }
186 sum
187 };
188 self.partial[c][k][m].push(coefficient);
189 }
190 let last = factors.len() - 1;
191 self.coefficients[c][k].mul(&self.partial[c][k][last][j]).round_out(q)
192 };
193 total = total.add(&value).round_out(q);
194 }
195 next.push(div_int(&total, (j + 1) as i64, q));
196 }
197 for (c, v) in next.into_iter().enumerate() {
198 self.x[c].push(v);
199 }
200 }
201
202 fn coefficient(&mut self, i: usize, order: usize) -> Iv {
203 while self.x[i].len() <= order {
204 self.extend();
205 }
206 self.x[i][order].clone()
207 }
208}
209
210fn a_priori(field: &Field, x0: &[Iv], h: &Iv, q: i64) -> Option<Vec<Iv>> {
212 let time = Iv {
213 lo: Dyadic::zero(),
214 hi: h.hi.clone(),
215 };
216 let mut b: Vec<Iv> = x0.to_vec();
217 for _ in 0..16 {
218 let fb = field.eval(&b, q);
219 let image: Vec<Iv> = x0
220 .iter()
221 .zip(&fb)
222 .map(|(x, f)| x.add(&time.mul(f)).round_out(q))
223 .collect();
224 if image.iter().zip(&b).all(|(i, o)| subset(i, o)) {
225 return Some(image);
226 }
227 b = image
228 .iter()
229 .map(|i| {
230 let slack = i.width().shift(-2).add(&Dyadic::new(crate::numeric::BigInt::from_i64(1), -q));
231 i.widen(&slack)
232 })
233 .collect();
234 if b.iter().any(|i| i.mag_bits() > 64) {
235 return None;
236 }
237 }
238 None
239}
240
241fn step(field: &Field, x0: &[Iv], h: &Iv, order: usize, q: i64) -> Option<Vec<Iv>> {
243 let b = a_priori(field, x0, h, q)?;
244 let mut inner = Series::new(field, x0, q);
245 let mut outer = Series::new(field, &b, q);
246 let mut out = Vec::with_capacity(x0.len());
247 let h_power_k = (0..order).fold(Iv::point(Dyadic::int(1)), |acc, _| acc.mul(h).round_out(q));
248 let remainder_time = Iv {
249 lo: Dyadic::zero().min(h_power_k.lo.clone()),
250 hi: h_power_k.hi.clone(),
251 };
252 for i in 0..x0.len() {
253 let mut sum = Iv::point(Dyadic::zero());
254 for j in (0..order).rev() {
255 sum = sum.mul(h).add(&inner.coefficient(i, j)).round_out(q);
256 }
257 let remainder = outer.coefficient(i, order).mul(&remainder_time).round_out(q);
258 out.push(sum.add(&remainder).round_out(q));
259 }
260 Some(out)
261}
262
263pub fn flow(field: &Field, start: &[Iv], t: &Rational, q: i64, cap: i64) -> Result<Vec<Iv>, FlowError> {
266 if !field.well_formed() || start.len() != field.dimension() {
267 return Err(FlowError::Shape);
268 }
269 let mut x = start.to_vec();
270 let mut remaining = t.clone();
271 let mut s: i64 = 3;
272 while remaining.is_positive() {
273 let full = Rational::from_ratio_i64(1, 1i64 << s.min(62)).expect("2^s > 0");
274 let last = remaining.cmp(&full) != std::cmp::Ordering::Greater;
275 let length = if last { remaining.clone() } else { full };
276 let h = rational_iv(&length, q);
277 let order = ((q / s) as usize + 4).clamp(8, 400);
278 match step(field, &x, &h, order, q) {
279 Some(next) => {
280 x = next;
281 remaining = remaining.sub(&length);
282 if x.iter().any(|i| i.mag_bits() > 64) {
283 return Err(FlowError::Escapes);
284 }
285 }
286 None => {
287 s += 1;
288 if s > cap {
289 return Err(FlowError::Escapes);
290 }
291 }
292 }
293 }
294 Ok(x)
295}
296
297fn lower_bound(p: &Poly, lo: &Rational, hi: &Rational) -> Rational {
299 let mut acc = (Rational::zero(), Rational::zero());
300 for c in p.coeffs().iter().rev() {
301 let products = [acc.0.mul(lo), acc.0.mul(hi), acc.1.mul(lo), acc.1.mul(hi)];
302 let least = products.iter().min().expect("four products").clone();
303 let most = products.iter().max().expect("four products").clone();
304 acc = (least.add(c), most.add(c));
305 }
306 acc.0
307}
308
309pub fn escape_time_bound(p: &Poly, x0: &Rational, cap: u32) -> Option<Rational> {
313 let d = p.degree()?;
314 if d < 2 {
315 return None;
316 }
317 let lc = p.coeff(d);
318 if !lc.is_positive() || !p.eval(x0).is_positive() || p.count_real_roots_in(x0, &p.root_bound()) != 0 {
319 return None;
320 }
321 let spread = (0..d).fold(Rational::zero(), |acc, i| acc.add(&p.coeff(i).abs()));
322 let b = [x0.clone(), Rational::one(), Rational::from_i64(2).mul(&spread).div(&lc).expect("lc > 0")]
323 .into_iter()
324 .max()
325 .expect("three candidates");
326 let slope = lc.sub(&spread.div(&b).expect("b ≥ 1"));
327 let tail = Rational::one()
328 .div(&slope.mul(&Rational::from_i64(d as i64 - 1)).mul(&b.pow((d - 1) as i32).expect("b ≥ 1")))
329 .expect("positive");
330 if b == *x0 {
331 return Some(tail);
332 }
333 let span = b.sub(x0);
334 for k in 0..=cap {
335 let pieces = 1i64 << k.min(40);
336 let width = span.div(&Rational::from_i64(pieces)).expect("pieces > 0");
337 let mut head = Rational::zero();
338 let mut positive = true;
339 for i in 0..pieces {
340 let lo = x0.add(&width.mul(&Rational::from_i64(i)));
341 let hi = lo.add(&width);
342 let least = lower_bound(p, &lo, &hi);
343 if !least.is_positive() {
344 positive = false;
345 break;
346 }
347 head = head.add(&width.div(&least).expect("least > 0"));
348 }
349 if positive {
350 return Some(head.add(&tail));
351 }
352 }
353 None
354}
355
356#[cfg(test)]
357#[path = "../../logicaffeine_tests/unit/logicaffeine_base/ode/tests.rs"]
358mod tests;