1use std::collections::BTreeMap;
9
10use num_bigint::BigInt;
11
12use crate::differences::{DiffGraph, DiffNode};
13use crate::error::Error;
14use crate::graph::{Graph, Node};
15use crate::parse::{Position, Predicate};
16
17type Variable = (usize, u8);
19
20type Monomial = Vec<(Variable, u32)>;
23
24#[derive(Clone, Debug, PartialEq, Eq)]
27pub struct Polynomial {
28 terms: BTreeMap<Monomial, BigInt>,
29}
30
31impl Polynomial {
32 fn zero() -> Self {
33 Polynomial {
34 terms: BTreeMap::new(),
35 }
36 }
37
38 fn constant(value: i64) -> Self {
39 let mut p = Polynomial::zero();
40 if value != 0 {
41 p.terms.insert(Vec::new(), BigInt::from(value));
42 }
43 p
44 }
45
46 fn variable(point: usize, axis: u8) -> Self {
47 let mut p = Polynomial::zero();
48 p.terms.insert(vec![((point, axis), 1)], BigInt::from(1));
49 p
50 }
51
52 fn add_scaled(&mut self, other: &Polynomial, negate: bool) -> u64 {
55 let mut bits = 0;
56 for (monomial, coefficient) in &other.terms {
57 let entry = self.terms.entry(monomial.clone()).or_default();
58 if negate {
59 *entry -= coefficient;
60 } else {
61 *entry += coefficient;
62 }
63 bits = bits.max(entry.bits());
64 if *entry == BigInt::ZERO {
65 self.terms.remove(monomial);
66 }
67 }
68 bits
69 }
70
71 fn multiply(&self, other: &Polynomial) -> Result<Polynomial, String> {
74 let mut result = Polynomial::zero();
75 for (m1, c1) in &self.terms {
76 for (m2, c2) in &other.terms {
77 let entry = result.terms.entry(multiply_monomials(m1, m2)?).or_default();
78 *entry += c1 * c2;
79 }
80 }
81 result.terms.retain(|_, c| *c != BigInt::ZERO);
82 Ok(result)
83 }
84
85 pub fn degree(&self) -> Option<u32> {
88 self.terms.keys().map(monomial_degree).max()
89 }
90
91 pub fn is_homogeneous(&self) -> bool {
94 let mut degrees = self.terms.keys().map(monomial_degree);
95 match degrees.next() {
96 None => true,
97 Some(first) => degrees.all(|d| d == first),
98 }
99 }
100
101 pub fn terms(&self) -> usize {
103 self.terms.len()
104 }
105
106 pub fn is_zero(&self) -> bool {
108 self.terms.is_empty()
109 }
110}
111
112fn monomial_degree(monomial: &Monomial) -> u32 {
115 monomial.iter().map(|&(_, e)| e).sum()
116}
117
118fn multiply_monomials(a: &Monomial, b: &Monomial) -> Result<Monomial, String> {
122 let degree = u64::from(monomial_degree(a)) + u64::from(monomial_degree(b));
123 if degree > u64::from(u32::MAX) {
124 return Err(format!(
125 "the expression is too large to expand: a term would have a degree above {}",
126 u32::MAX
127 ));
128 }
129 let mut out = Vec::with_capacity(a.len() + b.len());
130 let (mut i, mut j) = (0, 0);
131 while i < a.len() && j < b.len() {
132 match a[i].0.cmp(&b[j].0) {
133 std::cmp::Ordering::Less => {
134 out.push(a[i]);
135 i += 1;
136 }
137 std::cmp::Ordering::Greater => {
138 out.push(b[j]);
139 j += 1;
140 }
141 std::cmp::Ordering::Equal => {
142 out.push((a[i].0, a[i].1 + b[j].1));
144 i += 1;
145 j += 1;
146 }
147 }
148 }
149 out.extend_from_slice(&a[i..]);
150 out.extend_from_slice(&b[j..]);
151 Ok(out)
152}
153
154pub(crate) const MAX_TERMS: usize = 1 << 16;
156
157pub(crate) const MAX_WORK: u64 = 1 << 20;
160
161pub(crate) const MAX_COEFFICIENT_BITS: u64 = 1 << 16;
163
164#[derive(Clone)]
167struct Value {
168 polynomial: Polynomial,
169 bits: u64,
170}
171
172struct Budget {
174 work: u64,
175}
176
177impl Budget {
178 fn spend(&mut self, pairs: u64, bits: u64) -> Result<(), String> {
181 if bits > MAX_COEFFICIENT_BITS {
182 return Err(format!(
183 "the expression is too large to expand: a coefficient would have \
184 more than {MAX_COEFFICIENT_BITS} bits"
185 ));
186 }
187 let cost = pairs.saturating_mul(1 + bits / 64);
188 self.work = self.work.saturating_add(cost);
189 if self.work > MAX_WORK {
190 return Err(format!(
191 "the expression is too large to expand: expanding it would take \
192 more than {MAX_WORK} operations on its terms"
193 ));
194 }
195 Ok(())
196 }
197}
198
199fn coefficient_bits(p: &Polynomial) -> u64 {
201 p.terms.values().map(BigInt::bits).max().unwrap_or(0)
202}
203
204pub fn canonical(graph: &Graph, file: &str, position: Position) -> Result<Polynomial, Error> {
219 expand(graph).map_err(|message| Error::at(file, position, message))
220}
221
222fn expand(graph: &Graph) -> Result<Polynomial, String> {
223 let mut uses = vec![0usize; graph.nodes.len()];
224 uses[graph.root] += 1;
225 for node in &graph.nodes {
226 if let Node::Add(x, y) | Node::Sub(x, y) | Node::Mul(x, y) = *node {
227 uses[x] += 1;
228 uses[y] += 1;
229 }
230 }
231 let mut budget = Budget { work: 0 };
232 let mut values: Vec<Option<Value>> = vec![None; graph.nodes.len()];
233 let mut take = |values: &mut Vec<Option<Value>>, budget: &mut Budget, id: usize| {
234 uses[id] -= 1;
235 if uses[id] == 0 {
236 Ok(values[id].take().expect("children come before parents"))
237 } else {
238 let value = values[id].as_ref().expect("children come before parents");
239 budget.spend(value.polynomial.terms() as u64, value.bits)?;
240 Ok::<Value, String>(value.clone())
241 }
242 };
243 for (id, node) in graph.nodes.iter().enumerate() {
244 let value = match *node {
245 Node::Coord { point, axis } => Value {
246 polynomial: Polynomial::variable(point, axis),
247 bits: 1,
248 },
249 Node::Int(n) => {
250 let polynomial = Polynomial::constant(n);
251 let bits = coefficient_bits(&polynomial);
252 Value { polynomial, bits }
253 }
254 Node::Add(x, y) | Node::Sub(x, y) => {
255 let mut left = take(&mut values, &mut budget, x)?;
256 let right = take(&mut values, &mut budget, y)?;
257 budget.spend(
258 right.polynomial.terms() as u64,
259 left.bits.max(right.bits) + 1,
260 )?;
261 let changed = left
262 .polynomial
263 .add_scaled(&right.polynomial, matches!(node, Node::Sub(..)));
264 left.bits = left.bits.max(changed);
266 left
267 }
268 Node::Mul(x, y) => {
269 let left = take(&mut values, &mut budget, x)?;
270 let right = take(&mut values, &mut budget, y)?;
271 let (l, r) = (
272 left.polynomial.terms() as u64,
273 right.polynomial.terms() as u64,
274 );
275 let bits = left.bits + right.bits + u64::from(64 - l.min(r).leading_zeros());
278 budget.spend(l.saturating_mul(r), bits)?;
279 let polynomial = left.polynomial.multiply(&right.polynomial)?;
280 let bits = coefficient_bits(&polynomial);
281 Value { polynomial, bits }
282 }
283 };
284 if value.polynomial.terms() > MAX_TERMS {
285 return Err(format!(
286 "the expression is too large to expand: a subexpression has more \
287 than {MAX_TERMS} terms"
288 ));
289 }
290 values[id] = Some(value);
291 }
292 Ok(take(&mut values, &mut budget, graph.root)?.polynomial)
293}
294
295pub fn check_same_polynomial(predicate: &Predicate, file: &str) -> Result<(), Error> {
305 let main = canonical(&predicate.main, file, predicate.position)?;
306 if main.is_zero() {
307 return Err(Error::at(
308 file,
309 predicate.position,
310 format!(
311 "the polynomial of `{}` is identically zero, so its sign is always zero",
312 predicate.name
313 ),
314 ));
315 }
316 if let Some(exact_graph) = &predicate.exact {
317 let position = predicate.exact_position.unwrap_or(predicate.position);
318 let exact = canonical(exact_graph, file, position)?;
319 if exact != main {
320 return Err(Error::at(
321 file,
322 position,
323 format!(
324 "the exact form of `{}` differs from its main form: \
325 they are not the same polynomial (main form has {} terms, exact form has {})",
326 predicate.name,
327 main.terms(),
328 exact.terms()
329 ),
330 ));
331 }
332 }
333 Ok(())
334}
335
336pub fn canonical_of_differences(
348 graph: &DiffGraph,
349 file: &str,
350 position: Position,
351) -> Result<Polynomial, Error> {
352 let mut nodes = vec![Node::Int(0)];
353 let mut ids = Vec::with_capacity(graph.nodes.len());
354 for node in &graph.nodes {
355 let id = match *node {
356 DiffNode::Leaf {
357 axis,
358 minuend,
359 subtrahend,
360 } => {
361 nodes.push(Node::Coord {
362 point: minuend,
363 axis,
364 });
365 nodes.push(Node::Coord {
366 point: subtrahend,
367 axis,
368 });
369 nodes.push(Node::Sub(nodes.len() - 2, nodes.len() - 1));
370 nodes.len() - 1
371 }
372 DiffNode::Neg(x) => {
373 nodes.push(Node::Sub(0, ids[x]));
374 nodes.len() - 1
375 }
376 DiffNode::Add(x, y) => {
377 nodes.push(Node::Add(ids[x], ids[y]));
378 nodes.len() - 1
379 }
380 DiffNode::Sub(x, y) => {
381 nodes.push(Node::Sub(ids[x], ids[y]));
382 nodes.len() - 1
383 }
384 DiffNode::Mul(x, y) => {
385 nodes.push(Node::Mul(ids[x], ids[y]));
386 nodes.len() - 1
387 }
388 };
389 ids.push(id);
390 }
391 let graph = Graph {
392 root: ids[graph.root],
393 nodes,
394 };
395 canonical(&graph, file, position)
396}