mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

z3str3: fix incorrect automaton polarity in intersection check, and clean up code (#4595)

Browse source
This commit is contained in:
Murphy Berzish 2020-07-27 20:11:38 -05:00 committed by GitHub
parent 6910c0d5eb
commit afdfc5e8a6
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 30 additions and 45 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

75
src/smt/theory_str_regex.cpp
View file

@ -48,8 +48,7 @@ namespace smt {
// TODO since heuristics might fail, the "no progress" flag might need to be handled specially here
bool regex_axiom_add = false;
for (obj_hashtable<expr>::iterator it = regex_terms.begin(); it != regex_terms.end(); ++it) {
expr * str_in_re = *it;
for (auto str_in_re : regex_terms) {
expr * str = nullptr;
expr * re = nullptr;
u.str.is_in_re(str_in_re, str, re);
@ -78,8 +77,7 @@ namespace smt {
regex_term_to_extra_length_vars.find(str_in_re, extra_length_vars);
assert_axiom(top_level_length_constraint);
for(ptr_vector<expr>::iterator it = extra_length_vars.begin(); it != extra_length_vars.end(); ++it) {
expr * v = *it;
for(auto v : extra_length_vars) {
refresh_theory_var(v);
expr_ref len_constraint(m_autil.mk_ge(v, m_autil.mk_numeral(rational::zero(), true)), m);
assert_axiom(len_constraint);
@ -95,16 +93,15 @@ namespace smt {
TRACE("str", tout << "top-level length constraint: " << mk_pp(top_level_length_constraint, m) << std::endl;);
// assert and track length constraint
assert_axiom(top_level_length_constraint);
for(expr_ref_vector::iterator it = extra_length_vars.begin(); it != extra_length_vars.end(); ++it) {
expr * v = *it;
for(auto v : extra_length_vars) {
expr_ref len_constraint(m_autil.mk_ge(v, m_autil.mk_numeral(rational::zero(), true)), m);
assert_axiom(len_constraint);
}
regex_term_to_length_constraint.insert(str_in_re, top_level_length_constraint);
ptr_vector<expr> vtmp;
for(expr_ref_vector::iterator it = extra_length_vars.begin(); it != extra_length_vars.end(); ++it) {
vtmp.push_back(*it);
for(auto v : extra_length_vars) {
vtmp.push_back(v);
}
regex_term_to_extra_length_vars.insert(str_in_re, vtmp);
}
@ -129,9 +126,7 @@ namespace smt {
regex_automaton_under_assumptions assumption;
if (regex_automaton_assumptions.contains(re) &&
!regex_automaton_assumptions[re].empty()){
for (svector<regex_automaton_under_assumptions>::iterator it = regex_automaton_assumptions[re].begin();
it != regex_automaton_assumptions[re].end(); ++it) {
regex_automaton_under_assumptions autA = *it;
for (auto autA : regex_automaton_assumptions[re]) {
rational assumed_upper_bound, assumed_lower_bound;
bool assumes_upper_bound = autA.get_upper_bound(assumed_upper_bound);
bool assumes_lower_bound = autA.get_lower_bound(assumed_lower_bound);
@ -276,9 +271,7 @@ namespace smt {
bool need_assumption = true;
regex_automaton_under_assumptions last_assumption;
rational last_ub = rational::minus_one();
for (svector<regex_automaton_under_assumptions>::iterator it = regex_automaton_assumptions[re].begin();
it != regex_automaton_assumptions[re].end(); ++it) {
regex_automaton_under_assumptions autA = *it;
for (auto autA : regex_automaton_assumptions[re]) {
if ((current_assignment == l_true && autA.get_polarity() == false)
|| (current_assignment == l_false && autA.get_polarity() == true)) {
// automaton uses incorrect polarity
@ -399,9 +392,7 @@ namespace smt {
bool need_assumption = true;
regex_automaton_under_assumptions last_assumption;
rational last_lb = rational::zero(); // the default
for (svector<regex_automaton_under_assumptions>::iterator it = regex_automaton_assumptions[re].begin();
it != regex_automaton_assumptions[re].end(); ++it) {
regex_automaton_under_assumptions autA = *it;
for (auto autA : regex_automaton_assumptions[re]) {
if ((current_assignment == l_true && autA.get_polarity() == false)
|| (current_assignment == l_false && autA.get_polarity() == true)) {
// automaton uses incorrect polarity
@ -540,12 +531,11 @@ namespace smt {
}
} // foreach (entry in regex_terms)
for (obj_map<expr, ptr_vector<expr> >::iterator it = regex_terms_by_string.begin();
it != regex_terms_by_string.end(); ++it) {
for (auto entry : regex_terms_by_string) {
// TODO do we need to check equivalence classes of strings here?
expr * str = it->m_key;
ptr_vector<expr> str_in_re_terms = it->m_value;
expr* str = entry.m_key;
ptr_vector<expr> str_in_re_terms = entry.m_value;
svector<regex_automaton_under_assumptions> intersect_constraints;
// we may find empty intersection before checking every constraint;
@ -554,12 +544,11 @@ namespace smt {
// choose an automaton/assumption for each assigned (str.in.re)
// that's consistent with the current length information
for (ptr_vector<expr>::iterator term_it = str_in_re_terms.begin();
term_it != str_in_re_terms.end(); ++term_it) {
for (auto str_in_re_term : str_in_re_terms) {
expr * _unused = nullptr;
expr * re = nullptr;
SASSERT(u.str.is_in_re(*term_it));
u.str.is_in_re(*term_it, _unused, re);
SASSERT(u.str.is_in_re(str_in_re_term));
u.str.is_in_re(str_in_re_term, _unused, re);
rational exact_len;
bool has_exact_len = get_len_value(str, exact_len);
@ -570,9 +559,7 @@ namespace smt {
if (regex_automaton_assumptions.contains(re) &&
!regex_automaton_assumptions[re].empty()){
for (svector<regex_automaton_under_assumptions>::iterator aut_it = regex_automaton_assumptions[re].begin();
aut_it != regex_automaton_assumptions[re].end(); ++aut_it) {
regex_automaton_under_assumptions aut = *aut_it;
for (auto aut : regex_automaton_assumptions[re]) {
rational aut_ub;
bool assume_ub = aut.get_upper_bound(aut_ub);
rational aut_lb;
@ -615,16 +602,7 @@ namespace smt {
eautomaton * aut_inter = nullptr;
CTRACE("str", !intersect_constraints.empty(), tout << "check intersection of automata constraints for " << mk_pp(str, m) << std::endl;);
for (svector<regex_automaton_under_assumptions>::iterator aut_it = intersect_constraints.begin();
aut_it != intersect_constraints.end(); ++aut_it) {
regex_automaton_under_assumptions aut = *aut_it;
if (aut_inter == nullptr) {
// start somewhere
aut_inter = aut.get_automaton();
used_intersect_constraints.push_back(aut);
continue;
}
for (auto aut : intersect_constraints) {
TRACE("str",
{
unsigned v = regex_get_counter(regex_length_attempt_count, aut.get_regex_term());
@ -646,8 +624,12 @@ namespace smt {
// TODO do we need to push the intermediates into a vector for deletion anyway?
if ( (current_assignment == l_true && aut.get_polarity())
|| (current_assignment == l_false && !aut.get_polarity())) {
aut_inter = m_mk_aut.mk_product(aut_inter, aut.get_automaton());
m_automata.push_back(aut_inter);
if (aut_inter == nullptr) {
aut_inter = aut.get_automaton();
} else {
aut_inter = m_mk_aut.mk_product(aut_inter, aut.get_automaton());
m_automata.push_back(aut_inter);
}
} else {
// need to complement first
expr_ref rc(u.re.mk_complement(aut.get_regex_term()), m);
@ -659,8 +641,12 @@ namespace smt {
regex_automata.push_back(aut_c);
// TODO is there any way to build a complement automaton from an existing one?
// this discards length information
aut_inter = m_mk_aut.mk_product(aut_inter, aut_c);
m_automata.push_back(aut_inter);
if (aut_inter == nullptr) {
aut_inter = aut_c;
} else {
aut_inter = m_mk_aut.mk_product(aut_inter, aut_c);
m_automata.push_back(aut_inter);
}
}
used_intersect_constraints.push_back(aut);
if (aut_inter->is_empty()) {
@ -679,9 +665,7 @@ namespace smt {
expr_ref_vector conflict_terms(m);
expr_ref conflict_lhs(m);
for (svector<regex_automaton_under_assumptions>::iterator aut_it = used_intersect_constraints.begin();
aut_it != used_intersect_constraints.end(); ++aut_it) {
regex_automaton_under_assumptions aut = *aut_it;
for (auto aut : used_intersect_constraints) {
expr * str_in_re_term(u.re.mk_in_re(str, aut.get_regex_term()));
lbool current_assignment = ctx.get_assignment(str_in_re_term);
if (current_assignment == l_true) {
@ -702,6 +686,7 @@ namespace smt {
}
}
conflict_lhs = mk_and(conflict_terms);
TRACE("str", tout << "conflict lhs: " << mk_pp(conflict_lhs, m) << std::endl;);
if (used_intersect_constraints.size() > 1 && aut_inter != nullptr) {
// check whether the intersection is only the empty string