From afdfc5e8a60e2ee3cde83d78132773ff894f0258 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 27 Jul 2020 20:11:38 -0500 Subject: [PATCH] z3str3: fix incorrect automaton polarity in intersection check, and clean up code (#4595) --- src/smt/theory_str_regex.cpp | 75 +++++++++++++++--------------------- 1 file changed, 30 insertions(+), 45 deletions(-) diff --git a/src/smt/theory_str_regex.cpp b/src/smt/theory_str_regex.cpp index da96b13bb55..1b376dfbf3b 100644 --- a/src/smt/theory_str_regex.cpp +++ b/src/smt/theory_str_regex.cpp @@ -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::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::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 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::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::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::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 >::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 str_in_re_terms = it->m_value; + expr* str = entry.m_key; + ptr_vector str_in_re_terms = entry.m_value; svector 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::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::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::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::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