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, whilex := x + (-2)
is not. The former matchesxi := ie - ie
, withx
and2
supported integer expressions. The latter is not supported, as it matchesxi := ie
, and theie
matchesi + j
, but thenj
is-2
, which is not a supported integer expression. -
x := x + 1 - 1
is supported, whilex := x - 1 + 1
is not. The former is parsed asx := (x + 1) - 1
, which matchesxi := ie - ie
, and the leftie
is thenx + 1
, which matchesi + j
, etc. The latter is parsed asx := (x - 1) + 1
, which matchesxi := ie
, withie
matchingi + j
withi
beingx - 1
, which is not a supported integer expression. -
x := x - (1 - 1)
is supported, whilex := x - 1 - 1
is not. The former matchesxi := ie - ie
, with the rightie
being1 - 1
, which can be statically evaluated to0
, and is therefore supported. The latter update is parsed asx := (x - 1) - 1
andx - 1
is not a supported integer expression. -
x := x + 1 - y
andx := x + y - 1
are supported, whilex := x - (y - 1)
andx := x - (1 - y)
are not. The former two are parsed asx := (x + 1) - y
andx := (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.
-