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

moving more std::map std::set to obj_*, #1529

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-17 04:21:28 -07:00
parent f59d4c6ac0
commit aa913c564c
2 changed files with 15 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/smt/theory_str.cpp
View file

@ -441,7 +441,7 @@ namespace smt {
void theory_str::track_variable_scope(expr * var) { void theory_str::track_variable_scope(expr * var) {
if (internal_variable_scope_levels.find(sLevel) == internal_variable_scope_levels.end()) { if (internal_variable_scope_levels.find(sLevel) == internal_variable_scope_levels.end()) {
internal_variable_scope_levels[sLevel] = std::set<expr*>(); internal_variable_scope_levels[sLevel] = obj_hashtable<expr>();
} }
internal_variable_scope_levels[sLevel].insert(var); internal_variable_scope_levels[sLevel].insert(var);
} }
@ -6468,9 +6468,9 @@ namespace smt {
expr * regexTerm = a_regexIn->get_arg(1); expr * regexTerm = a_regexIn->get_arg(1);
// TODO figure out regex NFA stuff // TODO figure out regex NFA stuff
if (regex_nfa_cache.find(regexTerm) == regex_nfa_cache.end()) { if (!regex_nfa_cache.contains(regexTerm)) {
TRACE("str", tout << "regex_nfa_cache: cache miss" << std::endl;); TRACE("str", tout << "regex_nfa_cache: cache miss" << std::endl;);
regex_nfa_cache[regexTerm] = nfa(u, regexTerm); regex_nfa_cache.insert(regexTerm, nfa(u, regexTerm));
} else { } else {
TRACE("str", tout << "regex_nfa_cache: cache hit" << std::endl;); TRACE("str", tout << "regex_nfa_cache: cache hit" << std::endl;);
} }
@ -9286,7 +9286,7 @@ namespace smt {
h++; h++;
coverAll = get_next_val_encode(options[options.size() - 1], base); coverAll = get_next_val_encode(options[options.size() - 1], base);
} }
val_range_map[val_indicator] = options[options.size() - 1]; val_range_map.insert(val_indicator, options[options.size() - 1]);
TRACE("str", TRACE("str",
tout << "value tester encoding " << "{" << std::endl; tout << "value tester encoding " << "{" << std::endl;
@ -9380,7 +9380,7 @@ namespace smt {
TRACE("str", tout << "no previous value testers, or none of them were in scope" << std::endl;); TRACE("str", tout << "no previous value testers, or none of them were in scope" << std::endl;);
int tries = 0; int tries = 0;
expr * val_indicator = mk_internal_valTest_var(freeVar, len, tries); expr * val_indicator = mk_internal_valTest_var(freeVar, len, tries);
valueTester_fvar_map[val_indicator] = freeVar; valueTester_fvar_map.insert(val_indicator, freeVar);
fvar_valueTester_map[freeVar][len].push_back(std::make_pair(sLevel, val_indicator)); fvar_valueTester_map[freeVar][len].push_back(std::make_pair(sLevel, val_indicator));
print_value_tester_list(fvar_valueTester_map[freeVar][len]); print_value_tester_list(fvar_valueTester_map[freeVar][len]);
return gen_val_options(freeVar, len_indicator, val_indicator, len_valueStr, tries); return gen_val_options(freeVar, len_indicator, val_indicator, len_valueStr, tries);
@ -9430,7 +9430,7 @@ namespace smt {
refresh_theory_var(valTester); refresh_theory_var(valTester);
} else { } else {
valTester = mk_internal_valTest_var(freeVar, len, i + 1); valTester = mk_internal_valTest_var(freeVar, len, i + 1);
valueTester_fvar_map[valTester] = freeVar; valueTester_fvar_map.insert(valTester, freeVar);
fvar_valueTester_map[freeVar][len].push_back(std::make_pair(sLevel, valTester)); fvar_valueTester_map[freeVar][len].push_back(std::make_pair(sLevel, valTester));
print_value_tester_list(fvar_valueTester_map[freeVar][len]); print_value_tester_list(fvar_valueTester_map[freeVar][len]);
} }
@ -9595,7 +9595,7 @@ namespace smt {
if (low.is_neg()) { if (low.is_neg()) {
toAssert = m_autil.mk_ge(cntInUnr, mk_int(0)); toAssert = m_autil.mk_ge(cntInUnr, mk_int(0));
} else { } else {
if (unroll_var_map.find(unrFunc) == unroll_var_map.end()) { if (!unroll_var_map.contains(unrFunc)) {
expr_ref newVar1(mk_regex_rep_var(), mgr); expr_ref newVar1(mk_regex_rep_var(), mgr);
expr_ref newVar2(mk_regex_rep_var(), mgr); expr_ref newVar2(mk_regex_rep_var(), mgr);
@ -9627,8 +9627,9 @@ namespace smt {
// put together // put together
toAssert = mgr.mk_and(ctx.mk_eq_atom(op0, and1), toAssert); toAssert = mgr.mk_and(ctx.mk_eq_atom(op0, and1), toAssert);
unroll_var_map[unrFunc] = toAssert; unroll_var_map.insert(unrFunc, toAssert);
} else { }
else {
toAssert = unroll_var_map[unrFunc]; toAssert = unroll_var_map[unrFunc];
} }
} }

11
src/smt/theory_str.h
View file

@ -286,7 +286,7 @@ protected:
obj_hashtable<expr> variable_set; obj_hashtable<expr> variable_set;
obj_hashtable<expr> internal_variable_set; obj_hashtable<expr> internal_variable_set;
obj_hashtable<expr> regex_variable_set; obj_hashtable<expr> regex_variable_set;
std::map<int, std::set<expr*> > internal_variable_scope_levels; std::map<int, obj_hashtable<expr> > internal_variable_scope_levels;
obj_hashtable<expr> internal_lenTest_vars; obj_hashtable<expr> internal_lenTest_vars;
obj_hashtable<expr> internal_valTest_vars; obj_hashtable<expr> internal_valTest_vars;
@ -295,21 +295,20 @@ protected:
obj_hashtable<expr> input_var_in_len; obj_hashtable<expr> input_var_in_len;
obj_map<expr, unsigned int> fvar_len_count_map; obj_map<expr, unsigned int> fvar_len_count_map;
// TBD: need to replace by obj_map for determinism
std::map<expr*, ptr_vector<expr> > fvar_lenTester_map; std::map<expr*, ptr_vector<expr> > fvar_lenTester_map;
obj_map<expr, expr*> lenTester_fvar_map; obj_map<expr, expr*> lenTester_fvar_map;
// TBD: need to replace by obj_map for determinism // TBD: need to replace by obj_map for determinism
std::map<expr*, std::map<int, svector<std::pair<int, expr*> > > > fvar_valueTester_map; std::map<expr*, std::map<int, svector<std::pair<int, expr*> > > > fvar_valueTester_map;
std::map<expr*, expr*> valueTester_fvar_map; obj_map<expr, expr*> valueTester_fvar_map;
std::map<expr*, int_vector> val_range_map; obj_map<expr, int_vector> val_range_map;
// This can't be an expr_ref_vector because the constructor is wrong, // This can't be an expr_ref_vector because the constructor is wrong,
// we would need to modify the allocator so we pass in ast_manager // we would need to modify the allocator so we pass in ast_manager
// TBD: need to replace by obj_map for determinism // TBD: need to replace by obj_map for determinism
std::map<expr*, std::map<std::set<expr*>, ptr_vector<expr> > > unroll_tries_map; std::map<expr*, std::map<std::set<expr*>, ptr_vector<expr> > > unroll_tries_map;
std::map<expr*, expr*> unroll_var_map; obj_map<expr, expr*> unroll_var_map;
// TBD: need to replace by obj_pair_map for determinism // TBD: need to replace by obj_pair_map for determinism
std::map<std::pair<expr*, expr*>, expr*> concat_eq_unroll_ast_map; std::map<std::pair<expr*, expr*>, expr*> concat_eq_unroll_ast_map;
@ -323,7 +322,7 @@ protected:
std::map<std::pair<expr*, zstring>, expr*> regex_in_bool_map; std::map<std::pair<expr*, zstring>, expr*> regex_in_bool_map;
// TBD: need to replace by obj_map for determinism // TBD: need to replace by obj_map for determinism
std::map<expr*, std::set<zstring> > regex_in_var_reg_str_map; std::map<expr*, std::set<zstring> > regex_in_var_reg_str_map;
std::map<expr*, nfa> regex_nfa_cache; // Regex term --> NFA obj_map<expr, nfa> regex_nfa_cache; // Regex term --> NFA
svector<char> char_set; svector<char> char_set;
std::map<char, int> charSetLookupTable; std::map<char, int> charSetLookupTable;