Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions src/util/bitvector_expr.h
Original file line number Diff line number Diff line change
Expand Up @@ -121,6 +121,8 @@ inline bitnot_exprt &to_bitnot_expr(exprt &expr)
}

/// \brief Bit-wise OR
/// Any number of operands that is greater or equal one.
/// The type of all operands must be the same.
class bitor_exprt : public multi_ary_exprt
{
public:
Expand Down Expand Up @@ -162,6 +164,8 @@ inline bitor_exprt &to_bitor_expr(exprt &expr)

/// \brief Bit-wise NOR
///
/// Any number of operands that is greater or equal one.
/// The type of all operands must be the same.
/// When given one operand, this is equivalent to the bit-wise negation.
/// When given three or more operands, this is equivalent to the bit-wise
/// negation of the bitand expression with the same operands.
Expand Down Expand Up @@ -205,6 +209,8 @@ inline bitnor_exprt &to_bitnor_expr(exprt &expr)
}

/// \brief Bit-wise XOR
/// Any number of operands that is greater or equal one.
/// The type of all operands must be the same.
class bitxor_exprt : public multi_ary_exprt
{
public:
Expand Down Expand Up @@ -246,6 +252,8 @@ inline bitxor_exprt &to_bitxor_expr(exprt &expr)

/// \brief Bit-wise XNOR
///
/// Any number of operands that is greater or equal one.
/// The type of all operands must be the same.
/// When given one operand, this is equivalent to the bit-wise negation.
/// When given three or more operands, this is equivalent to the bit-wise
/// negation of the bitxor expression with the same operands.
Expand Down Expand Up @@ -291,6 +299,8 @@ inline bitxnor_exprt &to_bitxnor_expr(exprt &expr)
}

/// \brief Bit-wise AND
/// Any number of operands that is greater or equal one.
/// The type of all operands must be the same.
class bitand_exprt : public multi_ary_exprt
{
public:
Expand Down Expand Up @@ -332,6 +342,8 @@ inline bitand_exprt &to_bitand_expr(exprt &expr)

/// \brief Bit-wise NAND
///
/// Any number of operands that is greater or equal one.
/// The type of all operands must be the same.
/// When given one operand, this is equivalent to the bit-wise negation.
/// When given three or more operands, this is equivalent to the bit-wise
/// negation of the bitand expression with the same operands.
Expand Down
12 changes: 10 additions & 2 deletions src/util/std_expr.h
Original file line number Diff line number Diff line change
Expand Up @@ -2119,8 +2119,9 @@ inline typecast_exprt &to_typecast_expr(exprt &expr)
return static_cast<typecast_exprt &>(expr);
}


/// \brief Boolean AND
/// All operands must be boolean, and the result is always boolean.
/// Any number of operands that is greater or equal one.
class and_exprt:public multi_ary_exprt
{
public:
Expand Down Expand Up @@ -2189,6 +2190,8 @@ inline and_exprt &to_and_expr(exprt &expr)

/// \brief Boolean NAND
///
/// All operands must be boolean, and the result is always boolean.
/// Any number of operands that is greater or equal one.
/// When given one operand, this is equivalent to the negation.
/// When given three or more operands, this is equivalent to the negation
/// of the and expression with the same operands.
Expand Down Expand Up @@ -2269,8 +2272,9 @@ inline implies_exprt &to_implies_expr(exprt &expr)
return ret;
}


/// \brief Boolean OR
/// All operands must be boolean, and the result is always boolean.
/// Any number of operands that is greater or equal one.
class or_exprt:public multi_ary_exprt
{
public:
Expand Down Expand Up @@ -2334,6 +2338,8 @@ inline or_exprt &to_or_expr(exprt &expr)

/// \brief Boolean NOR
///
/// All operands must be boolean, and the result is always boolean.
/// Any number of operands that is greater or equal one.
/// When given one operand, this is equivalent to the negation.
/// When given three or more operands, this is equivalent to the negation
/// of the and expression with the same operands.
Expand Down Expand Up @@ -2371,6 +2377,8 @@ inline nor_exprt &to_nor_expr(exprt &expr)
}

/// \brief Boolean XOR
/// All operands must be boolean, and the result is always boolean.
/// Any number of operands that is greater or equal one.
class xor_exprt:public multi_ary_exprt
{
public:
Expand Down
Loading