mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

simplify diff rewriting

Browse source
This commit is contained in:
Nikolaj Bjorner 2019-12-20 23:20:19 -08:00
parent 4a94abe7d7
commit efbcdcbffd
1 changed files with 7 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

27
src/ast/rewriter/bool_rewriter.cpp
View file

@ -741,7 +741,7 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args
} }
expr_fast_mark1 visited; expr_fast_mark1 visited;
bool all_value = true; bool all_value = true, all_diff = true;
for (unsigned i = 0; i < num_args; i++) { for (unsigned i = 0; i < num_args; i++) {
expr * arg = args[i]; expr * arg = args[i];
if (visited.is_marked(arg)) { if (visited.is_marked(arg)) {
@ -751,30 +751,19 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args
visited.mark(arg); visited.mark(arg);
if (!m().is_unique_value(arg)) if (!m().is_unique_value(arg))
all_value = false; all_value = false;
} if (!all_value && all_diff) {
if (all_value) { for (unsigned j = 0; all_diff && j + 1 < i; ++j) {
result = m().mk_true(); all_diff = m().are_distinct(arg, args[j]);
return BR_DONE; }
}
SASSERT(num_args > 2);
if (m().is_bool(args[0])) {
result = m().mk_false();
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) { if (all_diff) {
result = m().mk_true(); result = m().mk_true();
return BR_DONE; return BR_DONE;
} }
if (some_eq) {
SASSERT(num_args > 2);
if (m().is_bool(args[0])) {
result = m().mk_false(); result = m().mk_false();
return BR_DONE; return BR_DONE;
} }