#458 CIF/BDD: allow negative integer literals, unary negation, and arbitrary use of binary subtraction

• Best to review per commit.
• End-user visible changes:
  • The CIF data-based synthesis tool and the CIF controller properties checker now support CIF models with negative integer literals and unary negation operations.
  • The CIF data-based synthesis tool and the CIF controller properties checker no longer restrict the use of binary subtraction in CIF models to only be allowed directly in assignments. Binary subtraction can now freely be used in expressions, as long as the arguments are supported expressions as well.
  • The CIF data-based synthesis tool and the CIF controller properties checker documentation about supported specifications have been reduced and simplified.
• Other changes:
  • Less manual casting in CifToBddConverter.convertExpr.
  • CifToBddConverter.convertExpr now has sanity checking for its expr parameter's type.
  • CifToBddConverter.convertExpr now returns only a bit vector, no more carry, and the bit vector can be either in unsigned or two's complement representation.
  • CifBddBitVector.ensureCompatible method has been added.
  • CifBddBitVector.ensureSameLength method has been added.
  • CifBddBitVector.*Any methods has been added for all binary operators (addAny, subtractAny, ifThenElseAny, lessThanAny, lessOrEqualAny, greaterThanAny, greaterOrEqualAny, equalToAny, unequalToAny).
  • Fixed TwosComplementCifBddBitVector createFromUnsignedBitVector to not have the two's complement bit vector share any of the bits of the unsigned bit vector.
• Note that variables with negative values in their integer ranges are still not supported. That is to follow later in #458 (closed).

Addresses #458 (closed)