From 62ea86d5d211a18117ef24d59a6a19dbbb2de8f8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 29 Dec 2019 10:55:58 -0800 Subject: [PATCH] fix #2832 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bv_rewriter.cpp | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index cfc4d9c13..896f4b9aa 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -2024,13 +2024,24 @@ br_status bv_rewriter::mk_bv_nand(unsigned num, expr * const * args, expr_ref & return BR_REWRITE2; } -br_status bv_rewriter::mk_bv_nor(unsigned num, expr * const * args, expr_ref & result) { - result = m_util.mk_bv_not(m_util.mk_bv_or(num, args)); +br_status bv_rewriter::mk_bv_nor(unsigned num_args, expr * const * args, expr_ref & result) { + result = m_util.mk_bv_not(m_util.mk_bv_or(num_args, args)); return BR_REWRITE2; } br_status bv_rewriter::mk_bv_xnor(unsigned num_args, expr * const * args, expr_ref & result) { - result = m_util.mk_bv_not(m_util.mk_bv_xor(num_args, args)); + switch (num_args) { + case 0: result = m().mk_true(); break; + case 1: result = m_util.mk_bv_not(args[0]); break; + case 2: result = m_util.mk_bv_not(m_util.mk_bv_xor(num_args, args)); break; + default: + mk_bv_xnor(2, args, result); + for (unsigned i = 2; i < num_args; ++i) { + expr* _args[2] = { result, args[i] }; + mk_bv_xnor(2, _args, result); + } + return BR_REWRITE_FULL; + } return BR_REWRITE2; }