mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

micro tuning for #4192

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-05-02 11:03:37 -07:00
parent f313ab9e4c
commit 8be266c18c
3 changed files with 20 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_context.h
View file

@ -735,6 +735,10 @@ namespace smt {
bool ts_visit_children(expr * n, bool gate_ctx, svector<int> & tcolors, svector<int> & fcolors, svector<expr_bool_pair> & todo); bool ts_visit_children(expr * n, bool gate_ctx, svector<int> & tcolors, svector<int> & fcolors, svector<expr_bool_pair> & todo);
svector<expr_bool_pair> ts_todo;
svector<int> tcolors;
svector<int> fcolors;
void top_sort_expr(expr * n, svector<expr_bool_pair> & sorted_exprs); void top_sort_expr(expr * n, svector<expr_bool_pair> & sorted_exprs);
void assert_default(expr * n, proof * pr); void assert_default(expr * n, proof * pr);

25
src/smt/smt_internalizer.cpp
View file

@ -126,10 +126,7 @@ namespace smt {
if (!def_int) { if (!def_int) {
ptr_buffer<expr> descendants; ptr_buffer<expr> descendants;
get_foreign_descendants(to_app(n), fid, descendants); get_foreign_descendants(to_app(n), fid, descendants);
ptr_buffer<expr>::iterator it = descendants.begin(); for (expr * arg : descendants) {
ptr_buffer<expr>::iterator end = descendants.end();
for (; it != end; ++it) {
expr * arg = *it;
ts_visit_child(arg, false, tcolors, fcolors, todo, visited); ts_visit_child(arg, false, tcolors, fcolors, todo, visited);
} }
return visited; return visited;
@ -154,27 +151,27 @@ namespace smt {
} }
void context::top_sort_expr(expr * n, svector<expr_bool_pair> & sorted_exprs) { void context::top_sort_expr(expr * n, svector<expr_bool_pair> & sorted_exprs) {
svector<expr_bool_pair> todo; ts_todo.reset();
svector<int> tcolors; tcolors.reset();
svector<int> fcolors; fcolors.reset();
todo.push_back(expr_bool_pair(n, true)); ts_todo.push_back(expr_bool_pair(n, true));
while (!todo.empty()) { while (!ts_todo.empty()) {
expr_bool_pair & p = todo.back(); expr_bool_pair & p = ts_todo.back();
expr * curr = p.first; expr * curr = p.first;
bool gate_ctx = p.second; bool gate_ctx = p.second;
switch (get_color(tcolors, fcolors, curr, gate_ctx)) { switch (get_color(tcolors, fcolors, curr, gate_ctx)) {
case White: case White:
set_color(tcolors, fcolors, curr, gate_ctx, Grey); set_color(tcolors, fcolors, curr, gate_ctx, Grey);
ts_visit_children(curr, gate_ctx, tcolors, fcolors, todo); ts_visit_children(curr, gate_ctx, tcolors, fcolors, ts_todo);
break; break;
case Grey: case Grey:
SASSERT(ts_visit_children(curr, gate_ctx, tcolors, fcolors, todo)); SASSERT(ts_visit_children(curr, gate_ctx, tcolors, fcolors, ts_todo));
set_color(tcolors, fcolors, curr, gate_ctx, Black); set_color(tcolors, fcolors, curr, gate_ctx, Black);
if (n != curr && !m.is_not(curr)) if (n != curr && !m.is_not(curr))
sorted_exprs.push_back(expr_bool_pair(curr, gate_ctx)); sorted_exprs.push_back(expr_bool_pair(curr, gate_ctx));
break; break;
case Black: case Black:
todo.pop_back(); ts_todo.pop_back();
break; break;
default: default:
UNREACHABLE(); UNREACHABLE();
@ -185,7 +182,7 @@ namespace smt {
#define DEEP_EXPR_THRESHOLD 1024 #define DEEP_EXPR_THRESHOLD 1024
void context::internalize_deep(expr* n) { void context::internalize_deep(expr* n) {
if (::get_depth(n) > DEEP_EXPR_THRESHOLD) { if (!e_internalized(n) && ::get_depth(n) > DEEP_EXPR_THRESHOLD) {
// if the expression is deep, then execute topological sort to avoid // if the expression is deep, then execute topological sort to avoid
// stack overflow. // stack overflow.
// a caveat is that theory internalizers do rely on recursive descent so // a caveat is that theory internalizers do rely on recursive descent so

11
src/smt/theory_fpa.cpp
View file

@ -388,16 +388,15 @@ namespace smt {
context & ctx = get_context(); context & ctx = get_context();
expr_ref res(m), t(m); expr_ref res(m), t(m);
expr_ref_vector fmls(m);
proof_ref t_pr(m); proof_ref t_pr(m);
res = m.mk_true();
expr_ref_vector::iterator it = m_converter.m_extra_assertions.begin(); for (expr* arg : m_converter.m_extra_assertions) {
expr_ref_vector::iterator end = m_converter.m_extra_assertions.end(); ctx.get_rewriter()(arg, t, t_pr);
for (; it != end; it++) { fmls.push_back(t);
ctx.get_rewriter()(*it, t, t_pr);
res = m.mk_and(res, t);
} }
m_converter.m_extra_assertions.reset(); m_converter.m_extra_assertions.reset();
res = m.mk_and(fmls);
m_th_rw(res); m_th_rw(res);