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

add cache for length terms to theory_str, but it seems to slow things down so I disabled it

Browse source
This commit is contained in:
Murphy Berzish 2016-11-08 15:20:47 -05:00
parent 521e0e175b
commit 61d1d5e8b0
2 changed files with 18 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/smt/theory_str.cpp
View file

@ -696,8 +696,21 @@ app * theory_str::mk_strlen(expr * e) {
int len = strlen(strval); int len = strlen(strval);
return m_autil.mk_numeral(rational(len), true); return m_autil.mk_numeral(rational(len), true);
} else { } else {
expr * args[1] = {e}; if (false) {
return get_manager().mk_app(get_id(), OP_STRLEN, 0, 0, 1, args); // use cache
app * lenTerm = NULL;
if (!length_ast_map.find(e, lenTerm)) {
expr * args[1] = {e};
lenTerm = get_manager().mk_app(get_id(), OP_STRLEN, 0, 0, 1, args);
length_ast_map.insert(e, lenTerm);
m_trail.push_back(lenTerm);
}
return lenTerm;
} else {
// always regen
expr * args[1] = {e};
return get_manager().mk_app(get_id(), OP_STRLEN, 0, 0, 1, args);
}
} }
} }

3
src/smt/theory_str.h
View file

@ -287,6 +287,9 @@ namespace smt {
// used when opt_FastValueTesterCache is true // used when opt_FastValueTesterCache is true
string_map valueTesterCache; string_map valueTesterCache;
// cache mapping each string S to Length(S)
obj_map<expr, app*> length_ast_map;
th_union_find m_find; th_union_find m_find;
th_trail_stack m_trail_stack; th_trail_stack m_trail_stack;
theory_var get_var(expr * n) const; theory_var get_var(expr * n) const;