From efbcdcbffd75b8cc32064273a43e872800f89915 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 20 Dec 2019 23:20:19 -0800 Subject: [PATCH] simplify diff rewriting --- src/ast/rewriter/bool_rewriter.cpp | 25 +++++++------------------ 1 file changed, 7 insertions(+), 18 deletions(-) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 8103a6425..39afbf1bb 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -741,7 +741,7 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args } expr_fast_mark1 visited; - bool all_value = true; + bool all_value = true, all_diff = true; for (unsigned i = 0; i < num_args; i++) { expr * arg = args[i]; if (visited.is_marked(arg)) { @@ -751,8 +751,13 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args visited.mark(arg); if (!m().is_unique_value(arg)) all_value = false; + if (!all_value && all_diff) { + for (unsigned j = 0; all_diff && j + 1 < i; ++j) { + all_diff = m().are_distinct(arg, args[j]); + } + } } - if (all_value) { + if (all_diff) { result = m().mk_true(); return BR_DONE; } @@ -763,22 +768,6 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args return BR_DONE; } - bool all_diff = true, some_eq = false; - for (unsigned i = 0; all_diff && !some_eq && i < num_args; i++) { - for (unsigned j = i + 1; all_diff && !some_eq && j < num_args; j++) { - all_diff = m().are_distinct(args[i], args[j]); - some_eq = m().are_equal(args[i], args[j]); - } - } - if (all_diff) { - result = m().mk_true(); - return BR_DONE; - } - if (some_eq) { - result = m().mk_false(); - return BR_DONE; - } - if (m_blast_distinct && num_args < m_blast_distinct_threshold) { ptr_buffer new_diseqs; for (unsigned i = 0; i < num_args; i++) {