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

reuse regex character constraints for the same string

Browse source
This commit is contained in:
Murphy Berzish 2018-01-15 14:30:12 -05:00
parent 6f889ab699
commit 058d24fd09
2 changed files with 35 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

43
src/smt/theory_str.cpp
View file

@ -6974,16 +6974,41 @@ namespace smt {
expr_ref_vector pathChars(m);
expr_ref_vector pathChars_len_constraints(m);
for (unsigned i = 0; i < lenVal.get_unsigned(); ++i) {
std::stringstream ss;
ss << "ch" << i;
expr_ref ch(mk_str_var(ss.str()), m);
pathChars.push_back(ch);
pathChars_len_constraints.push_back(ctx.mk_eq_atom(mk_strlen(ch), m_autil.mk_numeral(rational::one(), true)));
}
// TODO(mtrberzi) possibly modify this to reuse character terms over the same string,
// i.e. across different constraints over S the same variables S_0, S_1, ... are always used and refreshed
// reuse character terms over the same string
if (string_chars.contains(stringTerm)) {
// find out whether we have enough characters already
ptr_vector<expr> old_chars;
string_chars.find(stringTerm, old_chars);
if (old_chars.size() < lenVal.get_unsigned()) {
for (unsigned i = old_chars.size(); i < lenVal.get_unsigned(); ++i) {
std::stringstream ss;
ss << "ch" << i;
expr_ref ch(mk_str_var(ss.str()), m);
m_trail.push_back(ch);
old_chars.push_back(ch);
}
}
string_chars.insert(stringTerm, old_chars);
// now we're guaranteed to have at least the right number of characters in old_chars
for (unsigned i = 0; i < lenVal.get_unsigned(); ++i) {
expr_ref ch(old_chars.get(i), m);
refresh_theory_var(ch);
pathChars.push_back(ch);
pathChars_len_constraints.push_back(ctx.mk_eq_atom(mk_strlen(ch), m_autil.mk_numeral(rational::one(), true)));
}
} else {
ptr_vector<expr> new_chars;
for (unsigned i = 0; i < lenVal.get_unsigned(); ++i) {
std::stringstream ss;
ss << "ch" << i;
expr_ref ch(mk_str_var(ss.str()), m);
pathChars.push_back(ch);
pathChars_len_constraints.push_back(ctx.mk_eq_atom(mk_strlen(ch), m_autil.mk_numeral(rational::one(), true)));
new_chars.push_back(ch);
}
string_chars.insert(stringTerm, new_chars);
}
// modification of code in seq_rewriter::mk_str_in_regexp()
expr_ref_vector trail(m);

1
src/smt/theory_str.h
View file

@ -415,6 +415,7 @@ protected:
obj_map<expr, unsigned> regex_length_attempt_count;
obj_map<expr, unsigned> regex_fail_count;
obj_map<expr, unsigned> regex_intersection_fail_count;
obj_map<expr, ptr_vector<expr> > string_chars; // S --> [S_0, S_1, ...] for character terms S_i
svector<char> char_set;
std::map<char, int> charSetLookupTable;