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

fix regex automata leaked memory

Browse source
This commit is contained in:
Murphy Berzish 2018-04-12 14:35:29 -04:00
parent 47007d3f04
commit 3cfb32cd2d
2 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_str.cpp
View file

@ -77,6 +77,9 @@ namespace smt {
theory_str::~theory_str() { theory_str::~theory_str() {
m_trail_stack.reset(); m_trail_stack.reset();
for (eautomaton * aut : regex_automata) {
dealloc(aut);
}
regex_automata.clear(); regex_automata.clear();
} }
@ -10559,6 +10562,7 @@ namespace smt {
if ( (current_assignment == l_true && aut.get_polarity()) if ( (current_assignment == l_true && aut.get_polarity())
|| (current_assignment == l_false && !aut.get_polarity())) { || (current_assignment == l_false && !aut.get_polarity())) {
aut_inter = m_mk_aut.mk_product(aut_inter, aut.get_automaton()); aut_inter = m_mk_aut.mk_product(aut_inter, aut.get_automaton());
m_automata.push_back(aut_inter);
} else { } else {
// need to complement first // need to complement first
expr_ref rc(u.re.mk_complement(aut.get_regex_term()), m); expr_ref rc(u.re.mk_complement(aut.get_regex_term()), m);
@ -10567,6 +10571,7 @@ namespace smt {
// TODO is there any way to build a complement automaton from an existing one? // TODO is there any way to build a complement automaton from an existing one?
// this discards length information // this discards length information
aut_inter = m_mk_aut.mk_product(aut_inter, aut_c); aut_inter = m_mk_aut.mk_product(aut_inter, aut_c);
m_automata.push_back(aut_inter);
} }
used_intersect_constraints.push_back(aut); used_intersect_constraints.push_back(aut);
if (aut_inter->is_empty()) { if (aut_inter->is_empty()) {

1
src/smt/theory_str.h
View file

@ -395,6 +395,7 @@ protected:
obj_map<expr, std::set<zstring> > regex_in_var_reg_str_map; obj_map<expr, std::set<zstring> > regex_in_var_reg_str_map;
// regex automata // regex automata
scoped_ptr_vector<eautomaton> m_automata;
ptr_vector<eautomaton> regex_automata; ptr_vector<eautomaton> regex_automata;
obj_hashtable<expr> regex_terms; obj_hashtable<expr> regex_terms;
obj_map<expr, ptr_vector<expr> > regex_terms_by_string; // S --> [ (str.in.re S *) ] obj_map<expr, ptr_vector<expr> > regex_terms_by_string; // S --> [ (str.in.re S *) ]