mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

preliminary refactoring to use obj_map

Browse source
This commit is contained in:
Murphy Berzish 2018-03-12 17:09:55 -04:00
parent 5854492504
commit 73f7e301c3
2 changed files with 20 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/smt/theory_str.cpp
View file

@ -4582,8 +4582,9 @@ namespace smt {
std::pair<expr*, expr*> key = std::make_pair(concat, unroll);
expr_ref toAssert(mgr);
expr * _toAssert;
if (concat_eq_unroll_ast_map.find(key) == concat_eq_unroll_ast_map.end()) {
if (!concat_eq_unroll_ast_map.find(concat, unroll, _toAssert)) {
expr_ref arg1(to_app(concat)->get_arg(0), mgr);
expr_ref arg2(to_app(concat)->get_arg(1), mgr);
expr_ref r1(to_app(unroll)->get_arg(0), mgr);
@ -4634,9 +4635,9 @@ namespace smt {
toAssert = mgr.mk_and(opAnd1, opAnd2);
m_trail.push_back(toAssert);
concat_eq_unroll_ast_map[key] = toAssert;
concat_eq_unroll_ast_map.insert(concat, unroll, toAssert);
} else {
toAssert = concat_eq_unroll_ast_map[key];
toAssert = _toAssert;
}
assert_axiom(toAssert);
@ -4920,7 +4921,7 @@ namespace smt {
expr_ref_vector litems(m);
if (contain_pair_idx_map.find(varNode) != contain_pair_idx_map.end()) {
if (contain_pair_idx_map.contains(varNode)) {
std::set<std::pair<expr*, expr*> >::iterator itor1 = contain_pair_idx_map[varNode].begin();
for (; itor1 != contain_pair_idx_map[varNode].end(); ++itor1) {
expr * strAst = itor1->first;
@ -5057,7 +5058,7 @@ namespace smt {
ast_manager & m = get_manager();
expr_ref_vector litems(m);
if (contain_pair_idx_map.find(varNode) != contain_pair_idx_map.end()) {
if (contain_pair_idx_map.contains(varNode)) {
std::set<std::pair<expr*, expr*> >::iterator itor1 = contain_pair_idx_map[varNode].begin();
for (; itor1 != contain_pair_idx_map[varNode].end(); ++itor1) {
expr * strAst = itor1->first;
@ -5125,7 +5126,7 @@ namespace smt {
}
bool theory_str::in_contain_idx_map(expr * n) {
return contain_pair_idx_map.find(n) != contain_pair_idx_map.end();
return contain_pair_idx_map.contains(n);
}
void theory_str::check_contain_by_eq_nodes(expr * n1, expr * n2) {
@ -6456,7 +6457,7 @@ namespace smt {
} else {
expr_ref_vector::iterator itor = eqNodeSet.begin();
for (; itor != eqNodeSet.end(); itor++) {
if (regex_in_var_reg_str_map.find(*itor) != regex_in_var_reg_str_map.end()) {
if (regex_in_var_reg_str_map.contains(*itor)) {
std::set<zstring>::iterator strItor = regex_in_var_reg_str_map[*itor].begin();
for (; strItor != regex_in_var_reg_str_map[*itor].end(); strItor++) {
zstring regStr = *strItor;
@ -6469,7 +6470,7 @@ namespace smt {
expr * regexTerm = a_regexIn->get_arg(1);
// 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;);
regex_nfa_cache[regexTerm] = nfa(u, regexTerm);
} else {
@ -9596,7 +9597,7 @@ namespace smt {
if (low.is_neg()) {
toAssert = m_autil.mk_ge(cntInUnr, mk_int(0));
} 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 newVar2(mk_regex_rep_var(), mgr);

21
src/smt/theory_str.h
View file

@ -312,30 +312,29 @@ protected:
obj_hashtable<expr> input_var_in_len;
obj_map<expr, unsigned int> fvar_len_count_map;
std::map<expr*, ptr_vector<expr> > fvar_lenTester_map;
obj_map<expr, ptr_vector<expr> > fvar_lenTester_map;
obj_map<expr, expr*> lenTester_fvar_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, std::map<int, svector<std::pair<int, expr*> > > > fvar_valueTester_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,
// we would need to modify the allocator so we pass in ast_manager
std::map<expr*, std::map<std::set<expr*>, ptr_vector<expr> > > unroll_tries_map;
std::map<expr*, expr*> unroll_var_map;
std::map<std::pair<expr*, expr*>, expr*> concat_eq_unroll_ast_map;
obj_map<expr, std::map<std::set<expr*>, ptr_vector<expr> > > unroll_tries_map;
obj_map<expr, expr*> unroll_var_map;
obj_pair_map<expr, expr, expr*> concat_eq_unroll_ast_map;
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;
std::map<expr*, std::set<std::pair<expr*, expr*> > > contain_pair_idx_map;
obj_map<expr, std::set<std::pair<expr*, expr*> > > contain_pair_idx_map;
std::map<std::pair<expr*, zstring>, expr*> regex_in_bool_map;
std::map<expr*, std::set<zstring> > regex_in_var_reg_str_map;
obj_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;
std::map<char, int> charSetLookupTable;