mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-01 18:38:47 +00:00
Code Activity

cache computing strings and regexes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-07-02 11:14:29 -07:00
parent 655166b867
commit 5987d9ae20
1 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/seq_decl_plugin.cpp
View file

@ -548,6 +548,10 @@ sort* seq_decl_plugin::apply_binding(ptr_vector<sort> const& binding, sort* s) {
SASSERT(is_sort(s->get_parameter(0).get_ast())); SASSERT(is_sort(s->get_parameter(0).get_ast()));
sort* p = apply_binding(binding, to_sort(s->get_parameter(0).get_ast())); sort* p = apply_binding(binding, to_sort(s->get_parameter(0).get_ast()));
parameter param(p); parameter param(p);
if (p == m_char && s->get_decl_kind() == SEQ_SORT)
return m_string;
if (p == m_string && s->get_decl_kind() == RE_SORT)
return m_reglan;
return mk_sort(s->get_decl_kind(), 1, &param); return mk_sort(s->get_decl_kind(), 1, &param);
} }
return s; return s;