mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-05 19:00:25 +00:00
Code Activity

regex fail count and automaton fallback

Browse source
This commit is contained in:
Murphy Berzish 2018-01-16 18:15:29 -05:00
parent 153701eabe
commit e5585ecf4c
2 changed files with 22 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/smt/theory_str.cpp
View file

@ -9854,8 +9854,11 @@ namespace smt {
} else { } else {
// TODO check negation? // TODO check negation?
// TODO construct a partial automaton for R to the given upper bound? // TODO construct a partial automaton for R to the given upper bound?
// TODO increment failure count if we can't if (false) {
NOT_IMPLEMENTED_YET();
} else {
regex_inc_counter(regex_fail_count, str_in_re);
}
} }
continue; continue;
} }
@ -9866,8 +9869,8 @@ namespace smt {
} }
} else { // !upper_bound_exists } else { // !upper_bound_exists
// no upper bound information // no upper bound information
if (lower_bound_exists) { if (lower_bound_exists && !lower_bound_value.is_zero()) {
// lower bound, no upper bound // nonzero lower bound, no upper bound
// check current assumptions // check current assumptions
if (regex_automaton_assumptions.contains(re) && if (regex_automaton_assumptions.contains(re) &&
@ -9967,7 +9970,11 @@ namespace smt {
// TODO check negation? // TODO check negation?
// TODO construct a partial automaton for R to the given lower bound? // TODO construct a partial automaton for R to the given lower bound?
// TODO increment failure count // TODO increment failure count
NOT_IMPLEMENTED_YET(); if (false) {
} else {
regex_inc_counter(regex_fail_count, str_in_re);
}
} }
continue; continue;
} }
@ -9976,10 +9983,12 @@ namespace smt {
// check for existing automata; // check for existing automata;
// try to construct an automaton if we don't have one yet // try to construct an automaton if we don't have one yet
// and doing so without bounds is not difficult // and doing so without bounds is not difficult
NOT_IMPLEMENTED_YET(); bool existingAutomata = (regex_automaton_assumptions.contains(re) && !regex_automaton_assumptions[re].empty());
if (true) { bool failureThresholdExceeded = (regex_get_counter(regex_fail_count, str_in_re) >= m_params.m_RegexAutomata_FailedAutomatonThreshold);
if (!existingAutomata || failureThresholdExceeded) {
unsigned expected_complexity = estimate_regex_complexity(re); unsigned expected_complexity = estimate_regex_complexity(re);
if (expected_complexity <= m_params.m_RegexAutomata_DifficultyThreshold) { if (expected_complexity <= m_params.m_RegexAutomata_DifficultyThreshold
|| failureThresholdExceeded) {
eautomaton * aut = m_mk_aut(re); eautomaton * aut = m_mk_aut(re);
aut->compress(); aut->compress();
regex_automata.push_back(aut); regex_automata.push_back(aut);
@ -9991,7 +10000,11 @@ namespace smt {
TRACE("str", tout << "add new automaton for " << mk_pp(re, m) << ": no assumptions" << std::endl;); TRACE("str", tout << "add new automaton for " << mk_pp(re, m) << ": no assumptions" << std::endl;);
regex_axiom_add = true; regex_axiom_add = true;
// TODO immediately attempt to learn lower/upper bound info here // TODO immediately attempt to learn lower/upper bound info here
} else {
regex_inc_counter(regex_fail_count, str_in_re);
} }
} else {
regex_inc_counter(regex_fail_count, str_in_re);
} }
} }
} }

1
src/smt/theory_str.h
View file

@ -418,6 +418,7 @@ protected:
obj_map<expr, unsigned> regex_length_attempt_count; obj_map<expr, unsigned> regex_length_attempt_count;
obj_map<expr, unsigned> regex_fail_count; obj_map<expr, unsigned> regex_fail_count;
obj_map<expr, unsigned> regex_intersection_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 obj_map<expr, ptr_vector<expr> > string_chars; // S --> [S_0, S_1, ...] for character terms S_i
svector<char> char_set; svector<char> char_set;