Improve CIF data-based synthesis documentation on supported updates/expressions

The CIF data-based synthesis documentation about supported updates/expressions can be improved:

• From #458 (comment 1044579):

  I was also a little bit confused by the text in the documentation:

  Only discrete/input variables with a boolean type, ranged integer type (e.g. int[0..5]), or enumeration type are supported. For integer types, ranges that include negative integer values are not supported. For algebraic variables and algebraic parameters of components, all types are supported. For constants, all types are supported.

  The way it is formulated sound to me like that there should be no restrictions on what is allowed for constants, but apparently there are some.

  Clearly, for constants and algebraic variables/parameters, their values need to also be supported, for the context in which the constant or algebraic variable/parameter is used.

• Integer and enumeration expressions are listed as supported for the right hand side of assignments. Booleans are only covered as predicates, not as expressions. But, Booleans can also be used for right hand side of assignments, etc, like expressions. Essentially, for assignments to Boolean variables, the right hand side must be a supported expressions. This is not yet in the documentation.

• The documentation provides examples of expressions that can or can not be statically evaluated. By indenting this part, it would be more clear that this belongs to the last element of the list of supported integer/enumeration expressions.

• The documentation defines completely what updates/expressions are supported. But this may be subtle, and rewriting the expression may make it supported (see the discussion at #458 (comment 1044975)). For instance:

  • x := x - 2 is supported, while x := x + (-2) is not. The former matches xi := ie - ie, with x and 2 supported integer expressions. The latter is not supported, as it matches xi := ie, and the ie matches i + j, but then j is -2, which is not a supported integer expression.
  • x := x + 1 - 1 is supported, while x := x - 1 + 1 is not. The former is parsed as x := (x + 1) - 1, which matches xi := ie - ie, and the left ie is then x + 1, which matches i + j, etc. The latter is parsed as x := (x - 1) + 1, which matches xi := ie, with ie matching i + j with i being x - 1, which is not a supported integer expression.
  • x := x - (1 - 1) is supported, while x := x - 1 - 1 is not. The former matches xi := ie - ie, with the right ie being 1 - 1, which can be statically evaluated to 0, and is therefore supported. The latter update is parsed as x := (x - 1) - 1 and x - 1 is not a supported integer expression.
  • x := x + 1 - y and x := x + y - 1 are supported, while x := x - (y - 1) and x := x - (1 - y) are not. The former two are parsed as x := (x + 1) - y and x := (x + y) - 1, which leads to the - as top-level operator in the expression at the right hand side of the assignment. The latter two are unsupported, as the - operator is not a the top-level.

  Adding this to the documentation could help users to better interpret the rules for supported updates and expressions.