From 740f3991723ed05a8a54e9ceacd70bb435e6c634 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 17 Dec 2024 06:55:15 -0800 Subject: [PATCH] add nand_exprt, nor_exprt, xnor_exprt, bitnand_exprt, bitnor_exprt This adds classes for the nand, nor, bitnand, and bitnor expressions, documenting already existing expressions. This furthermore adds a class for the new xnor expression, to mirror the existing bitxnor expression. The comments clarify the meaning when those expressions are not binary. --- src/util/bitvector_expr.h | 97 +++++++++++++++++++++++++++++++ src/util/irep_ids.def | 1 + src/util/std_expr.h | 117 ++++++++++++++++++++++++++++++++++++++ 3 files changed, 215 insertions(+) diff --git a/src/util/bitvector_expr.h b/src/util/bitvector_expr.h index e9e3a32fde8..ec93a8006b4 100644 --- a/src/util/bitvector_expr.h +++ b/src/util/bitvector_expr.h @@ -160,6 +160,50 @@ inline bitor_exprt &to_bitor_expr(exprt &expr) return static_cast(expr); } +/// \brief Bit-wise NOR +/// +/// 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. +class bitnor_exprt : public multi_ary_exprt +{ +public: + bitnor_exprt(exprt _op0, exprt _op1) + : multi_ary_exprt(std::move(_op0), ID_bitnor, std::move(_op1)) + { + } + + bitnor_exprt(exprt::operandst _operands, typet _type) + : multi_ary_exprt(ID_bitnor, std::move(_operands), std::move(_type)) + { + } +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_bitnor; +} + +/// \brief Cast an exprt to a \ref bitnor_exprt +/// +/// \a expr must be known to be \ref bitnor_exprt. +/// +/// \param expr: Source expression +/// \return Object of type \ref bitnor_exprt +inline const bitnor_exprt &to_bitnor_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_bitnor); + return static_cast(expr); +} + +/// \copydoc to_bitnor_expr(const exprt &) +inline bitnor_exprt &to_bitnor_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_bitnor); + return static_cast(expr); +} + /// \brief Bit-wise XOR class bitxor_exprt : public multi_ary_exprt { @@ -201,6 +245,10 @@ inline bitxor_exprt &to_bitxor_expr(exprt &expr) } /// \brief Bit-wise XNOR +/// +/// 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. class bitxnor_exprt : public multi_ary_exprt { public: @@ -208,6 +256,11 @@ class bitxnor_exprt : public multi_ary_exprt : multi_ary_exprt(std::move(_op0), ID_bitxnor, std::move(_op1)) { } + + bitxnor_exprt(exprt::operandst _operands, typet _type) + : multi_ary_exprt(ID_bitxnor, std::move(_operands), std::move(_type)) + { + } }; template <> @@ -275,6 +328,50 @@ inline bitand_exprt &to_bitand_expr(exprt &expr) return static_cast(expr); } +/// \brief Bit-wise NAND +/// +/// 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. +class bitnand_exprt : public multi_ary_exprt +{ +public: + bitnand_exprt(exprt _op0, exprt _op1) + : multi_ary_exprt(std::move(_op0), ID_bitnand, std::move(_op1)) + { + } + + bitnand_exprt(exprt::operandst _operands, typet _type) + : multi_ary_exprt(ID_bitnand, std::move(_operands), std::move(_type)) + { + } +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_bitnand; +} + +/// \brief Cast an exprt to a \ref bitnand_exprt +/// +/// \a expr must be known to be \ref bitnand_exprt. +/// +/// \param expr: Source expression +/// \return Object of type \ref bitnand_exprt +inline const bitnand_exprt &to_bitnand_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_bitnand); + return static_cast(expr); +} + +/// \copydoc to_bitnand_expr(const exprt &) +inline bitnand_exprt &to_bitnand_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_bitnand); + return static_cast(expr); +} + /// \brief A base class for shift and rotate operators class shift_exprt : public binary_exprt { diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 2582e750cd5..507043b0d7d 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -48,6 +48,7 @@ IREP_ID_ONE(nand) IREP_ID_ONE(or) IREP_ID_ONE(nor) IREP_ID_ONE(xor) +IREP_ID_ONE(xnor) IREP_ID_ONE(not) IREP_ID_ONE(bitand) IREP_ID_ONE(bitor) diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 8a4b0276f10..9c10b8e8389 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -2182,6 +2182,43 @@ inline and_exprt &to_and_expr(exprt &expr) return static_cast(expr); } +/// \brief Boolean NAND +/// +/// 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. +class nand_exprt : public multi_ary_exprt +{ +public: + nand_exprt(exprt op0, exprt op1) + : multi_ary_exprt(std::move(op0), ID_nand, std::move(op1), bool_typet()) + { + } + + explicit nand_exprt(exprt::operandst _operands) + : multi_ary_exprt(ID_nand, std::move(_operands), bool_typet()) + { + } +}; + +/// \brief Cast an exprt to a \ref nand_exprt +/// +/// \a expr must be known to be \ref nand_exprt. +/// +/// \param expr: Source expression +/// \return Object of type \ref nand_exprt +inline const nand_exprt &to_nand_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_nand); + return static_cast(expr); +} + +/// \copydoc to_nand_expr(const exprt &) +inline nand_exprt &to_nand_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_nand); + return static_cast(expr); +} /// \brief Boolean implication class implies_exprt:public binary_exprt @@ -2290,6 +2327,43 @@ inline or_exprt &to_or_expr(exprt &expr) return static_cast(expr); } +/// \brief Boolean NOR +/// +/// 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. +class nor_exprt : public multi_ary_exprt +{ +public: + nor_exprt(exprt op0, exprt op1) + : multi_ary_exprt(std::move(op0), ID_nor, std::move(op1), bool_typet()) + { + } + + explicit nor_exprt(exprt::operandst _operands) + : multi_ary_exprt(ID_nor, std::move(_operands), bool_typet()) + { + } +}; + +/// \brief Cast an exprt to a \ref nor_exprt +/// +/// \a expr must be known to be \ref nor_exprt. +/// +/// \param expr: Source expression +/// \return Object of type \ref nor_exprt +inline const nor_exprt &to_nor_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_nor); + return static_cast(expr); +} + +/// \copydoc to_nor_expr(const exprt &) +inline nor_exprt &to_nor_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_nor); + return static_cast(expr); +} /// \brief Boolean XOR class xor_exprt:public multi_ary_exprt @@ -2331,6 +2405,49 @@ inline xor_exprt &to_xor_expr(exprt &expr) return static_cast(expr); } +/// \brief Boolean XNOR +/// +/// When given one operand, this is equivalent to the negation. +/// When given three or more operands, this is equivalent to the negation +/// of the xor expression with the same operands. +class xnor_exprt : public multi_ary_exprt +{ +public: + xnor_exprt(exprt _op0, exprt _op1) + : multi_ary_exprt(std::move(_op0), ID_xnor, std::move(_op1), bool_typet()) + { + } + + explicit xnor_exprt(exprt::operandst _operands) + : multi_ary_exprt(ID_xnor, std::move(_operands), bool_typet()) + { + } +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_xnor; +} + +/// \brief Cast an exprt to a \ref xnor_exprt +/// +/// \a expr must be known to be \ref xnor_exprt. +/// +/// \param expr: Source expression +/// \return Object of type \ref xnor_exprt +inline const xnor_exprt &to_xnor_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_xnor); + return static_cast(expr); +} + +/// \copydoc to_xnor_expr(const exprt &) +inline xnor_exprt &to_xnor_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_xnor); + return static_cast(expr); +} /// \brief Boolean negation class not_exprt:public unary_exprt