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

pull out incorrectly-used data structures in theory_str for contains check, this will need to be revisited

Browse source
This commit is contained in:
Murphy Berzish 2016-08-15 18:58:36 -04:00
parent d28ef1d471
commit 685edbb268
2 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_str.cpp
View file

@ -4376,7 +4376,7 @@ void theory_str::check_contain_by_substr(expr * varNode, expr_ref_vector & willE
}
bool theory_str::in_contain_idx_map(expr * n) {
return contain_pair_idx_map.contains(n);
return contain_pair_idx_map.find(n) != contain_pair_idx_map.end();
}
void theory_str::check_contain_by_eq_nodes(expr * n1, expr * n2) {
@ -4384,8 +4384,8 @@ void theory_str::check_contain_by_eq_nodes(expr * n1, expr * n2) {
ast_manager & m = get_manager();
if (in_contain_idx_map(n1) && in_contain_idx_map(n2)) {
obj_pair_set<expr, expr>::iterator keysItor1 = contain_pair_idx_map[n1].begin();
obj_pair_set<expr, expr>::iterator keysItor2;
std::set<std::pair<expr*, expr*> >::iterator keysItor1 = contain_pair_idx_map[n1].begin();
std::set<std::pair<expr*, expr*> >::iterator keysItor2;
for (; keysItor1 != contain_pair_idx_map[n1].end(); keysItor1++) {
// keysItor1 is on set {<.., n1>, ..., <n1, ...>, ...}

4
src/smt/theory_str.h
View file

@ -214,7 +214,9 @@ namespace smt {
expr_ref_vector contains_map;
theory_str_contain_pair_bool_map_t contain_pair_bool_map;
obj_map<expr, obj_pair_set<expr, expr> > contain_pair_idx_map;
//obj_map<expr, obj_pair_set<expr, expr> > contain_pair_idx_map;
// TODO Find a better data structure, this is 100% a hack right now
std::map<expr*, std::set<std::pair<expr*, expr*> > > contain_pair_idx_map;
char * char_set;
std::map<char, int> charSetLookupTable;