SMV word-level: support reduction and replication operators

[kroening]

Add lower() free functions for Verilog reduction operators (and/nand/or/nor/xor/xnor) and the replication operator in a new header src/verilog/verilog_expr_lowering.h. Use these in expr2smv.cpp to produce proper SMV output instead of norep dumps.

Also fix the Verilog type checker to unwrap the single-element concatenation that the parser wraps around the replication operand.

Changes

• src/verilog/verilog_expr_lowering.h (new): Free-standing lower() functions for reduction and replication expressions
• src/smvlang/expr2smv.cpp: Call lower() for reduction/replication operators in convert_rec()
• src/verilog/verilog_typecheck_expr.cpp: Unwrap single-element concatenation in replication operand
• regression/ebmc/smv-word-level/reduction1.desc: KNOWNBUG → CORE
• regression/ebmc/smv-word-level/replication1.desc: KNOWNBUG → CORE

Testing

All smv-word-level and verilog regression tests pass.

[kroening]

I'll do a PR against cbmc with the functions in src/verilog/verilog_expr_lowering.h becoming methods on the bitvector expressions.