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

z3str3: detect and give up when symbolic automaton construction fails (#4384)

Browse source 
typically this will happen due to non-constant terms in a RegLan expression
This commit is contained in:
Murphy Berzish 2020-05-28 11:57:33 -05:00 committed by GitHub
parent ccebd4db59
commit 71ea7287bb
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 28 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_str.cpp
View file

@ -8594,7 +8594,10 @@ namespace smt {
}
}
solve_regex_automata();
if (!solve_regex_automata()) {
TRACE("str", tout << "regex engine requested to give up!" << std::endl;);
return FC_GIVEUP;
}
bool needToAssignFreeVars = false;
expr_ref_vector free_variables(m);

2
src/smt/theory_str.h
View file

@ -623,7 +623,7 @@ protected:
void instantiate_axiom_RegexIn(enode * e);
// regex automata and length-aware regex
void solve_regex_automata();
bool solve_regex_automata();
unsigned estimate_regex_complexity(expr * re);
unsigned estimate_regex_complexity_under_complement(expr * re);
unsigned estimate_automata_intersection_difficulty(eautomaton * aut1, eautomaton * aut2);

28
src/smt/theory_str_regex.cpp
View file

@ -46,8 +46,8 @@ namespace smt {
return result;
}
void theory_str::solve_regex_automata() {
// Returns false if we need to give up solving, e.g. because we found symbolic expressions in an automaton.
bool theory_str::solve_regex_automata() {
ast_manager & m = get_manager();
// TODO since heuristics might fail, the "no progress" flag might need to be handled specially here
@ -216,6 +216,10 @@ namespace smt {
CTRACE("str", regex_get_counter(regex_fail_count, str_in_re) >= m_params.m_RegexAutomata_FailedAutomatonThreshold,
tout << "failed automaton threshold reached for " << mk_pp(str_in_re, m) << " -- automatically constructing full automaton" << std::endl;);
eautomaton * aut = m_mk_aut(re);
if (aut == nullptr) {
TRACE("str", tout << "ERROR: symbolic automaton construction failed, likely due to non-constant term in regex" << std::endl;);
return false;
}
aut->compress();
regex_automata.push_back(aut);
regex_automaton_under_assumptions new_aut(re, aut, true);
@ -354,6 +358,10 @@ namespace smt {
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);
if (aut == nullptr) {
TRACE("str", tout << "ERROR: symbolic automaton construction failed, likely due to non-constant term in regex" << std::endl;);
return false;
}
aut->compress();
regex_automata.push_back(aut);
regex_automaton_under_assumptions new_aut(re, aut, true);
@ -475,6 +483,10 @@ namespace smt {
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);
if (aut == nullptr) {
TRACE("str", tout << "ERROR: symbolic automaton construction failed, likely due to non-constant term in regex" << std::endl;);
return false;
}
aut->compress();
regex_automata.push_back(aut);
regex_automaton_under_assumptions new_aut(re, aut, true);
@ -508,6 +520,10 @@ namespace smt {
if (expected_complexity <= m_params.m_RegexAutomata_DifficultyThreshold
|| failureThresholdExceeded) {
eautomaton * aut = m_mk_aut(re);
if (aut == nullptr) {
TRACE("str", tout << "ERROR: symbolic automaton construction failed, likely due to non-constant term in regex" << std::endl;);
return false;
}
aut->compress();
regex_automata.push_back(aut);
regex_automaton_under_assumptions new_aut(re, aut, true);
@ -640,6 +656,10 @@ namespace smt {
// need to complement first
expr_ref rc(u.re.mk_complement(aut.get_regex_term()), m);
eautomaton * aut_c = m_mk_aut(rc);
if (aut_c == nullptr) {
TRACE("str", tout << "ERROR: symbolic automaton construction failed, likely due to non-constant term in regex" << std::endl;);
return false;
}
regex_automata.push_back(aut_c);
// TODO is there any way to build a complement automaton from an existing one?
// this discards length information
@ -713,9 +733,7 @@ namespace smt {
regex_axiom_add = true;
}
} // foreach (entry in regex_terms_by_string)
if (regex_axiom_add) {
//return FC_CONTINUE;
}
return true;
}
unsigned theory_str::estimate_regex_complexity(expr * re) {