mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

fix collection error

Browse source
This commit is contained in:
Murphy Berzish 2018-04-03 12:51:03 -04:00
parent 41703a4254
commit 6a3ce301b7
2 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_str.cpp
View file

@ -1854,6 +1854,9 @@ namespace smt {
std::pair<expr*, zstring> key1(ex->get_arg(0), regexStr);
// skip Z3str's map check, because we already check if we set up axioms on this term
regex_in_bool_map[key1] = ex;
if (!regex_in_var_reg_str_map.contains(ex->get_arg(0))) {
regex_in_var_reg_str_map.insert(ex->get_arg(0), std::set<zstring>());
}
regex_in_var_reg_str_map[ex->get_arg(0)].insert(regexStr);
}

2
src/smt/theory_str.h
View file

@ -399,7 +399,7 @@ protected:
obj_hashtable<expr> regex_terms;
obj_map<expr, ptr_vector<expr> > regex_terms_by_string; // S --> [ (str.in.re S *) ]
obj_map<expr, svector<regex_automaton_under_assumptions> > regex_automaton_assumptions; // RegEx --> [ aut+assumptions ]
std::map<expr*, nfa> regex_nfa_cache; // Regex term --> NFA
obj_map<expr, nfa> regex_nfa_cache; // Regex term --> NFA
obj_hashtable<expr> regex_terms_with_path_constraints; // set of string terms which have had path constraints asserted in the current scope
obj_hashtable<expr> regex_terms_with_length_constraints; // set of regex terms which had had length constraints asserted in the current scope
obj_map<expr, expr*> regex_term_to_length_constraint; // (str.in.re S R) -> (length constraint over S wrt. R)