= Linear arithmetic
<Linear arithmetic> is the fragment of <arithmetic> built from equalities and inequalities between linear expressions $a_1x_1+\cdots+a_nx_n+b$, combined by logical operations and, in some versions, quantifiers. Coefficients are fixed numbers; multiplying two unknowns, as in $xy$, leaves this fragment. One must specify whether the unknowns range over the <integers>, <rational numbers> or <real numbers>.<Arithmetic in the Online Z3 Guide>[Basics, Difference Arithmetic and Non-linear arithmetic]{ref}
For example, $2x+3y\le7$ and $x-y=1$ are linear constraints. Substitution gives $5y+2\le7$, hence $y\le1$. But $2x=1$ has a <real number> solution and no <integer> solution, so a procedure for one number system cannot simply be reused for the other. This distinction makes <linear arithmetic> useful in automated reasoning about counts, schedules and bounds.
Back to article page
