oxiz_math/polynomial/
mod.rs

1//! Polynomial arithmetic for non-linear theories.
2//!
3//! This module provides multivariate polynomial representation and operations
4//! for SMT solving, particularly for non-linear real arithmetic (NRA).
5//!
6//! Reference: Z3's `math/polynomial/` directory.
7
8mod advanced_ops;
9mod arithmetic;
10mod constructors;
11mod extended_ops;
12mod helpers;
13pub mod simd;
14mod types;
15
16pub mod factorization;
17pub mod gcd;
18pub mod gcd_advanced;
19pub mod gcd_multivariate;
20pub mod gcd_multivariate_advanced;
21pub mod interpolation;
22pub mod resultant;
23pub mod root_counting;
24pub mod root_isolation;
25pub mod sparse_ops;
26pub mod symbolic_differentiation;
27
28// Re-export all public types
29pub use types::{Monomial, MonomialOrder, NULL_VAR, Term, Var, VarPower};
30
31// Re-export public utility functions
32pub use helpers::rational_sqrt;
33
34#[allow(unused_imports)]
35use crate::prelude::*;
36use core::ops::{Add, Mul, Neg, Sub};
37use num_traits::Signed;
38
39/// A multivariate polynomial over rationals.
40/// Represented as a sum of terms, sorted by monomial order.
41#[derive(Clone)]
42pub struct Polynomial {
43    /// Terms in decreasing order (according to monomial order).
44    pub(crate) terms: Vec<Term>,
45    /// The monomial ordering used.
46    pub(crate) order: MonomialOrder,
47}
48
49// Operator trait implementations
50impl Neg for Polynomial {
51    type Output = Polynomial;
52
53    fn neg(self) -> Polynomial {
54        Polynomial::neg(&self)
55    }
56}
57
58impl Neg for &Polynomial {
59    type Output = Polynomial;
60
61    fn neg(self) -> Polynomial {
62        Polynomial::neg(self)
63    }
64}
65
66impl Add for Polynomial {
67    type Output = Polynomial;
68
69    fn add(self, other: Polynomial) -> Polynomial {
70        Polynomial::add(&self, &other)
71    }
72}
73
74impl Add<&Polynomial> for &Polynomial {
75    type Output = Polynomial;
76
77    fn add(self, other: &Polynomial) -> Polynomial {
78        Polynomial::add(self, other)
79    }
80}
81
82impl Sub for Polynomial {
83    type Output = Polynomial;
84
85    fn sub(self, other: Polynomial) -> Polynomial {
86        Polynomial::sub(&self, &other)
87    }
88}
89
90impl Sub<&Polynomial> for &Polynomial {
91    type Output = Polynomial;
92
93    fn sub(self, other: &Polynomial) -> Polynomial {
94        Polynomial::sub(self, other)
95    }
96}
97
98impl Mul for Polynomial {
99    type Output = Polynomial;
100
101    fn mul(self, other: Polynomial) -> Polynomial {
102        Polynomial::mul(&self, &other)
103    }
104}
105
106impl Mul<&Polynomial> for &Polynomial {
107    type Output = Polynomial;
108
109    fn mul(self, other: &Polynomial) -> Polynomial {
110        Polynomial::mul(self, other)
111    }
112}
113
114impl PartialEq for Polynomial {
115    fn eq(&self, other: &Self) -> bool {
116        if self.terms.len() != other.terms.len() {
117            return false;
118        }
119
120        for i in 0..self.terms.len() {
121            if self.terms[i] != other.terms[i] {
122                return false;
123            }
124        }
125
126        true
127    }
128}
129
130impl Eq for Polynomial {}
131
132impl core::fmt::Debug for Polynomial {
133    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
134        if self.is_zero() {
135            write!(f, "0")
136        } else {
137            for (i, term) in self.terms.iter().enumerate() {
138                if i > 0 {
139                    if term.coeff.is_positive() {
140                        write!(f, " + ")?;
141                    } else {
142                        write!(f, " - ")?;
143                    }
144                    let mut t = term.clone();
145                    t.coeff = t.coeff.abs();
146                    write!(f, "{:?}", t)?;
147                } else {
148                    write!(f, "{:?}", term)?;
149                }
150            }
151            Ok(())
152        }
153    }
154}
155
156impl core::fmt::Display for Polynomial {
157    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
158        core::fmt::Debug::fmt(self, f)
159    }
160}
oxiz_math/polynomial/mod.rs

oxiz_math/polynomial/
mod.rs
