Module assumptions 

Mathematical property inference engine.

This module implements a three-valued logic system for tracking mathematical properties of expressions. Each property can be Some(true) (known true), Some(false) (known false), or None (unknown).

The core data structures are:

• Props — a bitflag set naming mathematical properties.
• Assumptions — a pair of Props sets (known_true, known_false) representing three-valued knowledge about an expression.
• AssumptionCache — a cache mapping ExprId → Assumptions, with methods to query and compute properties.

Inference rules

When a property is asserted, Assumptions::forward_chain applies implication rules until a fixpoint is reached. For example, asserting integer = true immediately deduces rational = true, real = true, complex = true, finite = true, commutative = true, and algebraic = true.

The rules are derived from the same mathematical ontology as SymPy’s assumption system, but compiled into bitmask operations for speed.

Sign properties and infinities

positive, negative, nonnegative and nonpositive are extended real notions: oo is positive and -oo is negative (SymPy’s extended_positive / extended_negative). Consequently a sign property alone implies extended_real, nonzero (for the strict ones) and the negations of the opposite signs — but not real, finite or complex. Those follow from extended_real ∧ finite → real:

value	positive	extended_real	finite	real	complex	infinite
1	true	true	true	true	true	false
oo	true	true	false	false	false	true
-oo	false	true	false	false	false	true
zoo	false	false	false	false	false	true
I	false	false	true	false	true	false
nan	unknown	unknown	unknown	unknown	unknown	unknown

A symbol declared Positive (via Context::symbol_with, sym! or Ex::assume) is nevertheless a finite positive number, as in SymPy: Assumptions::normalize_declared adds finite to declared sets that carry a sign unless finiteness was declared explicitly. Declaring a contradictory set panics.

Structs

AssumptionCache

Cache of computed assumptions, indexed by ExprId.

Assumptions

Three-valued assumption state for a single expression.

Props

A set of mathematical properties.

Enums

Assumption

A user-facing assumption specifier for the sym! macro and Context::symbol_with.