Skip to content

Commit

Permalink
[NFC][SMT] Fix formatting & update description for smt.bv2int
Browse files Browse the repository at this point in the history
As per post-commit review on #8049
  • Loading branch information
TaoBi22 committed Jan 10, 2025
1 parent c226b54 commit a4356bc
Showing 1 changed file with 6 additions and 7 deletions.
13 changes: 6 additions & 7 deletions include/circt/Dialect/SMT/SMTBitVectorOps.td
Original file line number Diff line number Diff line change
Expand Up @@ -241,16 +241,15 @@ def RepeatOp : SMTBVOp<"repeat", [Pure]> {
def BV2IntOp : SMTOp<"bv2int", [Pure]> {
let summary = "Convert an SMT bit-vector to an SMT integer.";
let description = [{
Adapted from the Z3 documentation:
Create an integer from the bit-vector argument `input`.
If `is_signed` is false, then the bit-vector `input` is treated as
unsigned. So the result is non-negative and in the range [0..2^N-1], where
N are the number of bits in `input`. If `is_signed` is true, `input` is
treated as a signed bit-vector.
Create an integer from the bit-vector argument `input`. If `is_signed` is
present, the bit-vector is treated as two's complement signed. Otherwise,
it is treated as an unsigned integer in the range [0..2^N-1], where N is
the number of bits in `input`.
}];
let arguments = (ins BitVectorType:$input, UnitAttr:$is_signed);
let results = (outs IntType:$result);
let assemblyFormat = [{$input (`signed` $is_signed^)? attr-dict `:` qualified(type($input))}];
let assemblyFormat = [{$input (`signed` $is_signed^)? attr-dict `:`
qualified(type($input))}];
}

#endif // CIRCT_DIALECT_SMT_SMTBITVECTOROPS_TD

0 comments on commit a4356bc

Please sign in to comment.