Commit Graph

2 Commits

Author SHA1 Message Date
github action 95dbd349d6 Apply 'make format' 2026-02-05 16:54:05 +05:30
Rahul Behl a868e70595 Support array reduction methods with 'with' clause in constraints
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.
2026-02-05 15:42:35 +05:30