Struct NatPolyForm 

pub struct NatPolyForm { /* private fields */ }

A normalized polynomial form for Nat expressions.

This is the canonical representation for Nat arithmetic (Level 1 addition + Level 2 multiplication). Each term is a monomial mapped to its coefficient. Two NatPolyForms are equal iff their normalized terms match.

Implementations

impl NatPolyForm

pub fn from_constant(c: u64) -> Self

Create a polynomial from a constant.

pub fn from_var(name: GenericParamName) -> Self

Create a polynomial from a single variable with coefficient 1.

pub fn add(&self, other: &Self) -> Result<Self, NatOverflowError>

Add two polynomials.

Returns an error if a coefficient overflows.

pub fn mul(&self, other: &Self) -> Result<Self, NatOverflowError>

Multiply two polynomials (distributive law).

Returns an error if a coefficient or exponent overflows.

pub fn constant(&self) -> u64

Returns the constant term (coefficient of the empty monomial).

pub fn is_constant(&self) -> bool

Returns true if this form has no variables (is a constant).

pub fn evaluate(&self, bindings: &HashMap<GenericParamName, u64>) -> Option<u64>

Evaluate to a concrete value given variable bindings.

Returns None if any variable is unbound or arithmetic overflows.

pub fn format(&self) -> String

Format as a human-readable string.

Examples: "3", "N", "N + 1", "M * N", "2 * N^2 + N + 1".

pub fn is_leq(&self, other: &Self) -> bool

Check if self <= other for all non-negative variable assignments.

Returns true iff for every monomial, the coefficient in self is <= the coefficient in other. This is sound because all Nat variables are non-negative, so each monomial evaluates to a non-negative value.

pub fn variables(&self) -> BTreeSet<GenericParamName>

Collect all variable names that appear in any monomial of this polynomial.

impl NatPolyForm

pub fn to_nat_range_identity( &self, ) -> Result<NatRangeIndexIdentity, NatRangeIndexError>

Wrap this normalized Nat form as a typed Nat-range index identity.

Errors

Returns an error when the form is a concrete invalid Nat range size.

Trait Implementations

impl Clone for NatPolyForm

fn clone(&self) -> NatPolyForm

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for NatPolyForm

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for NatPolyForm

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Eq for NatPolyForm

impl Hash for NatPolyForm

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for NatPolyForm

fn eq(&self, other: &NatPolyForm) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for NatPolyForm