#424 CIF to BDD: split precondition checking from conversion + support statically-evaluable predicates

This one was not so easy, as the conversion and precondition checking where quite intermixed, and the expression/predicate constraints are not super trivial.

Probably easiest to understand per commit. Several things change again later, so probably best to collect comments and report them on the final diff. The steps I followed are mostly like this:

• One by one move the precondition checks to a new precondition checker class.
• During that, and later afterwards, clean up and simplify the conversion code etc, since they may now assume a preconditions-satisfying specification.
• Fix regression bugs, make it all work again.
• Update test output and update some tests to still check the same (we now check in separate checks, not everything in sequence, etc).
• Extend/add some tests.
• Make changes for a weird corner case I only found out about later on (see below).

Changes to CIF to BDD:

• Split precondition checking from conversion.
• Conversion can now assume that precondition checking has succeeded, making various things easier, and reducing the code quite a bit (about 16% code reduction in converter class).
• Some comment improvements/fixes.
• Custom CifToBddVarOnlySpecificTypesCheck check, since it has very specific constraints on only discrete and input variables.
• Custom CifToBddExprOnlySupportedExprsCheck check, since it has very specific constraints on what expressions are supported and in what context:
  • This one is rather long. It started out as a copy of the conversion code, but I stripped the actual conversion, keeping only the parts needed for the check. I also clean up the code in various places.
  • For some reason, in the various iterations of making it, I made the check return boolean values that indicate whether expressions/predicates are OK. But, it was not used. I removed it again in a later commit.
• The non-determinism check is kept mostly as is, at least for now. It does have a slightly improvement in its output.
• The plants refer to requirement state check is kept as is, at least for now.
• Added support for predicates that are not one of the supported forms, but that can be statically evaluated to a single value, without giving evaluation errors. This one is tricky:
  • We now do the precondition checks with the checker framework. It pretty prints the specification to have position information for the entire specification, even if it was preprocessed.
  • The CIF pretty printer simplifies marked <trivially-true-expression> to marked, removing the predicate.
  • The reason the CIF pretty printer does this is because the CIF parser adds a true predicate there, even if not written in the syntax.
  • If we have marked [true][0] then this is fine for the precondition checker, as that is a trivially-true marker predicate, which is removed through pretty printing, and thus not actually checked at all.
  • But, we continue the conversion with the original specification before pretty printing and reparsing, so it still has the list and projection on list in there.
  • We don't support lists and projection in the conversion.
  • To make sure this is in sync, I added support for statically-evaluable predicates, just like we already support statically-evaluable non-boolean expressions.
  • This makes them in sync, and ensures that if the precondition checker thinks the specification is OK, the conversion will also succeed.

Other, related changes:

• Added new generic AutReqNoChannelCheck CIF check. Kept it as simple as needed for now. Can always be generalized later on.
• Added CifValueUtils.checkSingleValue, which is like CifValueUtils.hasSingleValue, but returns the first part of the expression that does not have a single value, such that it can be used to report check violations.

End user visible is:

• CIF data-based synthesis tool and CIF controller properties checker have improved output in case of precondition violations.
• CIF data-based synthesis tool and CIF controller properties checker now support CIF specifications with predicates that are not one of the supported forms, but that can be statically evaluated to a single value, without giving evaluation errors.
• CIF data-based synthesis tool and CIF controller properties checker have slightly improved documentation regarding preconditions.

Addresses #424 (closed)