CIF/BDD: Support more expressions, as well as 'if' updates

It would be good to support the following extra CIF language features for CIF/BDD (data-based synthesis, controller properties checker, etc):

• Binary expressions min and max on supported integers. (!1333 (merged))
• Binary expressions * (multiplication) on supported integers. (!1339 (merged))
• Standard library function abs on supported integers. (!1333 (merged))
  • This operation is already implemented by our BDD bit vectors.
• Standard library function sign on supported integers. (!1333 (merged), !1336 (merged), !1339 (merged))
• 'if' updates. (!1345 (merged))
  • This can be supported now by converting 'if' updates to 'if' expressions (like in the CIF to CIF transformation), given that we lifted the restriction on binary subtraction only occurring directly on the right hand side of an assignment. Previously, a supported subtraction could become part of an if expression, where it would be unsupported. Now that the restriction is lifted in #458 (closed), we can support this quite easily.