mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-03 01:40:22 +00:00
Code Activity

fix regex difficulty overflow bug; fix final check on regex terms that don't get path constraints

Browse source
This commit is contained in:
Murphy Berzish 2018-01-25 15:25:36 -05:00
parent 8d5065d35d
commit 852e0e0892
1 changed files with 29 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/smt/theory_str.cpp
View file

@ -6523,6 +6523,9 @@ namespace smt {
if (a == UINT_MAX || b == UINT_MAX) { if (a == UINT_MAX || b == UINT_MAX) {
return UINT_MAX; return UINT_MAX;
} }
if (a == 0 || b == 0) {
return 0;
}
unsigned result = a * b; unsigned result = a * b;
if (result < a || result < b) { if (result < a || result < b) {
return UINT_MAX; return UINT_MAX;
@ -9817,7 +9820,6 @@ namespace smt {
continue; continue;
} }
// find a consistent automaton for this term // find a consistent automaton for this term
bool found = false; bool found = false;
regex_automaton_under_assumptions assumption; regex_automaton_under_assumptions assumption;
@ -9835,7 +9837,7 @@ namespace smt {
found = true; found = true;
break; break;
} }
// check consistency of bounds assumptions // TODO check consistency of bounds assumptions
} // foreach(a in regex_automaton_assumptions) } // foreach(a in regex_automaton_assumptions)
} }
if (found) { if (found) {
@ -10101,7 +10103,8 @@ namespace smt {
// no existing automata/assumptions. // no existing automata/assumptions.
// if it's easy to construct a full automaton for R, do so // if it's easy to construct a full automaton for R, do so
unsigned expected_complexity = estimate_regex_complexity(re); unsigned expected_complexity = estimate_regex_complexity(re);
if (expected_complexity <= m_params.m_RegexAutomata_DifficultyThreshold) { bool failureThresholdExceeded = (regex_get_counter(regex_fail_count, str_in_re) >= m_params.m_RegexAutomata_FailedAutomatonThreshold);
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);
@ -10221,7 +10224,8 @@ namespace smt {
// no existing automata/assumptions. // no existing automata/assumptions.
// if it's easy to construct a full automaton for R, do so // if it's easy to construct a full automaton for R, do so
unsigned expected_complexity = estimate_regex_complexity(re); unsigned expected_complexity = estimate_regex_complexity(re);
if (expected_complexity <= m_params.m_RegexAutomata_DifficultyThreshold) { bool failureThresholdExceeded = (regex_get_counter(regex_fail_count, str_in_re) >= m_params.m_RegexAutomata_FailedAutomatonThreshold);
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);
@ -10518,6 +10522,27 @@ namespace smt {
return FC_CONTINUE; return FC_CONTINUE;
} }
// We must be be 100% certain that if there are any regex constraints,
// the string assignment for each variable is consistent with the automaton.
// The (probably) easiest way to do this is to ensure
// that we have path constraints set up for every assigned regex term.
if (m_params.m_RegexAutomata && !regex_terms.empty()) {
for (obj_hashtable<expr>::iterator it = regex_terms.begin(); it != regex_terms.end(); ++it) {
expr * str_in_re = *it;
expr * str;
expr * re;
u.str.is_in_re(str_in_re, str, re);
lbool current_assignment = ctx.get_assignment(str_in_re);
if (current_assignment == l_undef) {
continue;
}
if (!regex_terms_with_path_constraints.contains(str_in_re)) {
TRACE("str", tout << "assigned regex term " << mk_pp(str_in_re, m) << " has no path constraints -- continuing search" << std::endl;);
return FC_CONTINUE;
}
} // foreach (str.in.re in regex_terms)
}
if (unused_internal_variables.empty()) { if (unused_internal_variables.empty()) {
TRACE("str", tout << "All variables are assigned. Done!" << std::endl;); TRACE("str", tout << "All variables are assigned. Done!" << std::endl;);
return FC_DONE; return FC_DONE;