Relations may be simplified to respond to a query,
so you may see some changes in a relation if you print it before and
after a query.
For example, if you build a relation, print it
with ` Relation::print()`
, then ask if it is empty, and then print
it again, the formula in the second print will be different from but
equivalent to the first one. ` Relation::print_with_subs()`

would show no difference between those two calls, since it copies the relation and simplifies it in order to print it.

So, once you begin to query a relation, the Presburger formula may
change unexpectedly. Since the structure of the formula changes,
there are restrictions on the operations you can perform.
Specifically, most of the relation building operations are no
longer available (in other words, it is implicitly finalized).
You can no longer add constraints to ` F_And`

nodes, and you can no longer add new ` Formula`
nodes to any part
of the formula. The only way to modify the Presburger formula after
beginning to query it is to use ` Relation::and_with_EQ`
or
` Relation::and_with_GEQ`
.

If you wish to force a simplification of a relation for some reason,
use the function ` Relation::simplify()`
. This is a hint to the
library that it might be a good idea to simplify the relation
immediately. You might want to do this on a relation that has a
complicated formula, before you combine it with others using the
functions in Chapter
6. Sometimes, this can
speed up execution or reduce memory requirements.

omega@cs.umd.edu