Fixes#6455
This commit adds support for array reduction methods (sum, product, and, or, xor)
with 'with' clauses in randomization constraints. Previously, expressions like
'array.sum() with (int'(item == value))' were not supported in constraints.
Implementation details:
- Added handler in ConstraintExprVisitor::visit(AstCMethodHard*) for
ARRAY_R_SUM, ARRAY_R_PRODUCT, ARRAY_R_AND, ARRAY_R_OR, ARRAY_R_XOR
- Substitutes lambda argument references (item/index) in the with expression
- Generates appropriate SMT operations (bvadd, bvmul, bvand, bvor, bvxor)
- Uses correct identity elements for each reduction operation
- Marks non-constant nodes with user1() flag to ensure proper SMT code generation
The implementation follows the same pattern as the existing ARRAY_INSIDE handler,
generating SMT expressions at Verilator compile time that are evaluated by the
constraint solver at runtime.
893589f444