Parsing input expressions into linear form #
linarith computes the linear form of its input expressions,
assuming (without justification) that the type of these expressions
is a commutative semiring.
It identifies atoms up to ring-equivalence: that is,
(y*3)*x will be identified
where the monomial
x*y is the linear atom.
- Variables are represented by natural numbers.
- Monomials are represented by
monom := rb_map ℕ ℕ. The monomial
1is represented by the empty map.
- Linear combinations of monomials are represented by
sum := rb_map monom ℤ.
All input expressions are converted to
sums, preserving the map from expressions to variables.
We then discard the monomial information, mapping each distinct monomial to a natural number.
rb_map ℕ ℤ represents the ring-normalized linear form of the expression.
This is ultimately converted into a
linexp in the obvious way.
linear_forms_and_vars is the main entry point into this file. Everything else is contained.