mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

theory_str iterator refactoring and dead code removal (#5222)

Browse source 
* z3str3: iterator refactoring

* z3str3: remove old nfa dead code

* z3str3: continued iterator refactoring

* z3str3: remove unroll dead code

* z3str3: ctx_dep_analysis iterator refactoring

* z3str3: continued iterator refactoring

* z3str3: final iterator refactoring
This commit is contained in:
Murphy Berzish 2021-05-05 10:06:03 -05:00 committed by GitHub
parent 0c6722f48b
commit 466269ee13
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 195 additions and 636 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

777
src/smt/theory_str.cpp
View file

File diff suppressed because it is too large Load diff

54
src/smt/theory_str.h
View file

@ -107,54 +107,6 @@ public:
}
};
struct c_hash { unsigned operator()(char u) const { return (unsigned)u; } };
struct c_eq { bool operator()(char u1, char u2) const { return u1 == u2; } };
class nfa {
protected:
bool m_valid;
unsigned m_next_id;
unsigned next_id() {
unsigned retval = m_next_id;
++m_next_id;
return retval;
}
unsigned m_start_state;
unsigned m_end_state;
std::map<unsigned, std::map<char, unsigned> > transition_map;
std::map<unsigned, std::set<unsigned> > epsilon_map;
void make_transition(unsigned start, char symbol, unsigned end) {
transition_map[start][symbol] = end;
}
void make_epsilon_move(unsigned start, unsigned end) {
epsilon_map[start].insert(end);
}
// Convert a regular expression to an e-NFA using Thompson's construction
void convert_re(expr * e, unsigned & start, unsigned & end, seq_util & u);
public:
nfa(seq_util & u, expr * e)
: m_valid(true), m_next_id(0), m_start_state(0), m_end_state(0) {
convert_re(e, m_start_state, m_end_state, u);
}
nfa() : m_valid(false), m_next_id(0), m_start_state(0), m_end_state(0) {}
bool is_valid() const {
return m_valid;
}
void epsilon_closure(unsigned start, std::set<unsigned> & closure);
bool matches(zstring input);
};
class regex_automaton_under_assumptions {
protected:
expr * re_term;
@ -489,7 +441,6 @@ 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 ]
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)
@ -718,15 +669,14 @@ protected:
void check_consistency_contains(expr * e, bool is_true);
int ctx_dep_analysis(std::map<expr*, int> & strVarMap, std::map<expr*, int> & freeVarMap,
std::map<expr*, std::set<expr*> > & unrollGroupMap, std::map<expr*, std::map<expr*, int> > & var_eq_concat_map);
std::map<expr*, std::map<expr*, int> > & var_eq_concat_map);
void trace_ctx_dep(std::ofstream & tout,
std::map<expr*, expr*> & aliasIndexMap,
std::map<expr*, expr*> & var_eq_constStr_map,
std::map<expr*, std::map<expr*, int> > & var_eq_concat_map,
std::map<expr*, std::map<expr*, int> > & var_eq_unroll_map,
std::map<expr*, expr*> & concat_eq_constStr_map,
std::map<expr*, std::map<expr*, int> > & concat_eq_concat_map,
std::map<expr*, std::set<expr*> > & unrollGroupMap);
std::map<expr*, std::map<expr*, int> > & concat_eq_concat_map);
bool term_appears_as_subterm(expr * needle, expr * haystack);
void classify_ast_by_type(expr * node, std::map<expr*, int> & varMap,