mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

performance optimization in theory_str::classify_ast_by_type

Browse source
This commit is contained in:
Murphy Berzish 2016-09-12 16:41:35 -04:00
parent 2c5569aa1f
commit b3fddf4707
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_str.cpp
View file

@ -6597,10 +6597,10 @@ void theory_str::classify_ast_by_type(expr * node, std::map<expr*, int> & varMap
expr * arg1Val = get_eqc_value(arg1, arg1HasEq);
int canskip = 0;
if (arg0HasEq && arg0Val == m_strutil.mk_string("")) {
if (arg0HasEq && m_strutil.get_string_constant_value(arg0Val).empty()) {
canskip = 1;
}
if (canskip == 0 && arg1HasEq && arg1Val == m_strutil.mk_string("")) {
if (canskip == 0 && arg1HasEq && m_strutil.get_string_constant_value(arg1Val).empty()) {
canskip = 1;
}
if (canskip == 0 && concatMap.find(node) == concatMap.end()) {