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

#5259 - the Ranjit 2s shave

Browse source 
shave a couple of seconds from the Ranjit regression
This commit is contained in:
Nikolaj Bjorner 2021-05-12 10:43:16 -07:00
parent cd82205b06
commit 7869cdbbc8
4 changed files with 31 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/ast/normal_forms/nnf.cpp
View file

@ -72,6 +72,7 @@ class skolemizer {
cache m_cache;
cache m_cache_pr;
bool m_proofs_enabled;
used_vars m_uv;
void process(quantifier * q, expr_ref & r, proof_ref & p) {
@ -81,14 +82,14 @@ class skolemizer {
p = nullptr;
return;
}
used_vars uv;
uv(q);
m_uv.reset();
m_uv(q);
SASSERT(is_well_sorted(m, q));
unsigned sz = uv.get_max_found_var_idx_plus_1();
unsigned sz = m_uv.get_max_found_var_idx_plus_1();
ptr_buffer<sort> sorts;
expr_ref_vector args(m);
for (unsigned i = 0; i < sz; i++) {
sort * s = uv.get(i);
sort * s = m_uv.get(i);
if (s != nullptr) {
sorts.push_back(s);
args.push_back(m.mk_var(i, s));
@ -111,7 +112,7 @@ class skolemizer {
// (VAR num_decls-1) is in the last position.
//
for (unsigned i = 0; i < sz; i++) {
sort * s = uv.get(i);
sort * s = m_uv.get(i);
if (s != nullptr)
substitution.push_back(m.mk_var(i, s));
else

4
src/ast/rewriter/var_subst.cpp
View file

@ -79,7 +79,9 @@ expr_ref unused_vars_eliminator::operator()(quantifier* q) {
result = q;
return result;
}
unsigned num_decls = q->get_num_decls();
m_used.reset();
m_used.set_num_decls(num_decls);
m_used.process(q->get_expr());
unsigned num_patterns = q->get_num_patterns();
for (unsigned i = 0; i < num_patterns; i++)
@ -88,7 +90,7 @@ expr_ref unused_vars_eliminator::operator()(quantifier* q) {
for (unsigned i = 0; i < num_no_patterns; i++)
m_used.process(q->get_no_pattern(i));
unsigned num_decls = q->get_num_decls();
if (m_used.uses_all_vars(num_decls)) {
q->set_no_unused_vars();
result = q;

15
src/ast/used_vars.cpp
View file

@ -22,6 +22,9 @@ Revision History:
void used_vars::process(expr * n, unsigned delta) {
unsigned j, idx;
if (m_num_found_vars == m_num_decls)
return;
m_cache.reset();
m_todo.reset();
m_todo.push_back(expr_delta_pair(n, delta));
@ -58,8 +61,16 @@ void used_vars::process(expr * n, unsigned delta) {
if (idx >= delta) {
idx = idx - delta;
if (idx >= m_found_vars.size())
m_found_vars.resize(idx + 1);
m_found_vars[idx] = to_var(n)->get_sort();
m_found_vars.resize(idx + 1, nullptr);
if (!m_found_vars[idx]) {
m_found_vars[idx] = to_var(n)->get_sort();
if (idx < m_num_decls)
m_num_found_vars++;
if (m_num_found_vars == m_num_decls) {
m_todo.reset();
return;
}
}
}
break;
case AST_QUANTIFIER:

10
src/ast/used_vars.h
View file

@ -26,18 +26,26 @@ class used_vars {
typedef hashtable<expr_delta_pair, obj_hash<expr_delta_pair>, default_eq<expr_delta_pair> > cache;
cache m_cache;
svector<expr_delta_pair> m_todo;
unsigned m_num_decls{ UINT_MAX };
unsigned m_num_found_vars{ 0 };
void process(expr * n, unsigned delta);
public:
void operator()(expr * n) {
m_found_vars.reset();
reset();
process(n, 0);
}
void reset() {
m_found_vars.reset();
m_num_decls = UINT_MAX;
m_num_found_vars = 0;
}
void set_num_decls(unsigned n) {
m_num_decls = n;
}
void process(expr * n) {