mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-07-30 23:47:45 -07:00
parent ac64a370d7
commit e0d4669116
1 changed files with 14 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -136,7 +136,7 @@ br_status bool_rewriter::mk_nflat_and_core(unsigned num_args, expr * const * arg
unsigned sz = buffer.size();
switch(sz) {
switch (sz) {
case 0:
result = m().mk_true();
return BR_DONE;
@ -145,7 +145,7 @@ br_status bool_rewriter::mk_nflat_and_core(unsigned num_args, expr * const * arg
return BR_DONE;
default:
if (s) {
result = m().mk_and(sz, buffer.c_ptr());
result = m().mk_and(buffer);
return BR_DONE;
}
return BR_FAILED;
@ -166,16 +166,15 @@ br_status bool_rewriter::mk_flat_and_core(unsigned num_args, expr * const * args
expr * arg = args[i];
// Remark: all rewrites are depth 1.
if (m().is_and(arg)) {
unsigned num = to_app(arg)->get_num_args();
for (unsigned j = 0; j < num; j++)
flat_args.push_back(to_app(arg)->get_arg(j));
for (expr* e : *to_app(arg))
flat_args.push_back(e);
}
else {
flat_args.push_back(arg);
}
}
if (mk_nflat_and_core(flat_args.size(), flat_args.c_ptr(), result) == BR_FAILED)
result = m().mk_and(flat_args.size(), flat_args.c_ptr());
result = m().mk_and(flat_args);
return BR_DONE;
}
return mk_nflat_and_core(num_args, args, result);
@ -246,12 +245,12 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args
return BR_DONE;
default:
if (m_local_ctx && m_local_ctx_cost <= m_local_ctx_limit) {
if (local_ctx_simp(sz, buffer.c_ptr(), result))
if (local_ctx_simp(sz, buffer.c_ptr(), result))
return BR_DONE;
}
if (s) {
ast_lt lt;
std::sort(buffer.begin(), buffer.end(), lt);
std::sort(buffer.begin(), buffer.end(), lt);
result = m().mk_or(sz, buffer.c_ptr());
return BR_DONE;
}
@ -277,13 +276,12 @@ br_status bool_rewriter::mk_flat_or_core(unsigned num_args, expr * const * args,
// Remark: all rewrites are depth 1.
if (m().is_or(arg)) {
ordered = false;
unsigned num = to_app(arg)->get_num_args();
for (unsigned j = 0; j < num; j++)
flat_args.push_back(to_app(arg)->get_arg(j));
for (expr* e : *to_app(arg))
flat_args.push_back(e);
}
else {
flat_args.push_back(arg);
ordered &= !prev || !lt(arg, prev);
ordered &= (!prev || !lt(arg, prev));
prev = arg;
}
}
@ -292,7 +290,7 @@ br_status bool_rewriter::mk_flat_or_core(unsigned num_args, expr * const * args,
ast_lt lt;
std::sort(flat_args.begin(), flat_args.end(), lt);
}
result = m().mk_or(flat_args.size(), flat_args.c_ptr());
result = m().mk_or(flat_args);
}
return BR_DONE;
}
@ -342,7 +340,7 @@ bool bool_rewriter::simp_nested_not_or(unsigned num_args, expr * const * args,
new_args.push_back(arg);
}
if (simp) {
switch(new_args.size()) {
switch (new_args.size()) {
case 0:
result = m().mk_true();
return true;
@ -350,7 +348,7 @@ bool bool_rewriter::simp_nested_not_or(unsigned num_args, expr * const * args,
mk_not(new_args[0], result);
return true;
default:
result = m().mk_not(m().mk_or(new_args.size(), new_args.c_ptr()));
result = m().mk_not(m().mk_or(new_args));
return true;
}
}
@ -796,7 +794,7 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args
for (unsigned j = i + 1; j < num_args; j++)
new_diseqs.push_back(m().mk_not(mk_eq(args[i], args[j])));
}
result = m().mk_and(new_diseqs.size(), new_diseqs.c_ptr());
result = m().mk_and(new_diseqs);
return BR_REWRITE3;
}