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.