From 064b1f0721186be80490bafb1373aa1b370146c0 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Fri, 19 Mar 2021 12:37:16 -0500 Subject: [PATCH] z3str3: address code reviews and remove some dead code (#5116) --- src/smt/theory_str_mc.cpp | 8 ++------ src/smt/theory_str_regex.cpp | 34 +--------------------------------- 2 files changed, 3 insertions(+), 39 deletions(-) diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp index d84494ac3..e642d6c7b 100644 --- a/src/smt/theory_str_mc.cpp +++ b/src/smt/theory_str_mc.cpp @@ -447,11 +447,6 @@ namespace smt { ast_manager & sub_m = subsolver.m(); - // NSB code review: to remove dependencies on subsolver.get_context(). - // It uses a method that should be removed from smt_kernel. - // currently sub_ctx is used to retrieve a rewriter. Theory_str already has a rewriter attahed. - context & sub_ctx = subsolver.get_context(); - expr * str = nullptr, *re = nullptr; VERIFY(u.str.is_in_re(f, str, re)); @@ -554,7 +549,8 @@ namespace smt { } } expr_ref result(mk_or(ors), sub_m); - sub_ctx.get_rewriter()(result); + th_rewriter rw(sub_m); + rw(result); TRACE("str_fl", tout << "regex path constraint: " << mk_pp(result, sub_m) << std::endl;); if (sub_m.is_false(result)) { diff --git a/src/smt/theory_str_regex.cpp b/src/smt/theory_str_regex.cpp index 36e1f2117..032592171 100644 --- a/src/smt/theory_str_regex.cpp +++ b/src/smt/theory_str_regex.cpp @@ -45,9 +45,6 @@ namespace smt { // 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() { - - // TODO since heuristics might fail, the "no progress" flag might need to be handled specially here - bool regex_axiom_add = false; for (auto str_in_re : regex_terms) { expr * str = nullptr; expr * re = nullptr; @@ -108,7 +105,6 @@ namespace smt { regex_terms_with_length_constraints.insert(str_in_re); m_trail_stack.push(insert_obj_trail(regex_terms_with_length_constraints, str_in_re)); - regex_axiom_add = true; } } // re not in regex_terms_with_length_constraints @@ -193,7 +189,6 @@ namespace smt { expr_ref conflict(m.mk_not(lhs), m); assert_axiom(conflict); } - regex_axiom_add = true; regex_inc_counter(regex_length_attempt_count, re); continue; } else { @@ -219,7 +214,6 @@ namespace smt { } regex_automaton_assumptions[re].push_back(new_aut); TRACE("str", tout << "add new automaton for " << mk_pp(re, m) << ": no assumptions" << std::endl;); - regex_axiom_add = true; find_automaton_initial_bounds(str_in_re, aut); } else { regex_inc_counter(regex_fail_count, str_in_re); @@ -337,7 +331,6 @@ namespace smt { expr_ref lhs_terms(mk_and(lhs), m); expr_ref rhs_terms(mk_and(rhs), m); assert_implication(lhs_terms, rhs_terms); - regex_axiom_add = true; } } } else { @@ -359,24 +352,12 @@ namespace smt { } regex_automaton_assumptions[re].push_back(new_aut); TRACE("str", tout << "add new automaton for " << mk_pp(re, m) << ": no assumptions" << std::endl;); - regex_axiom_add = true; find_automaton_initial_bounds(str_in_re, aut); } else { - // TODO check negation? - // TODO construct a partial automaton for R to the given upper bound? - if (false) { - - } else { - regex_inc_counter(regex_fail_count, str_in_re); - } + regex_inc_counter(regex_fail_count, str_in_re); } continue; } - // if we have *any* automaton for R, and the upper bound is not too large, - // finitize the automaton (if we have not already done so) and assert all solutions - if (upper_bound_value < 50) { // TODO better metric for threshold - // NOT_IMPLEMENTED_YET(); // TODO(mtrberzi) - } } else { // !upper_bound_exists // no upper bound information if (lower_bound_exists && !lower_bound_value.is_zero() && new_lower_bound_info) { @@ -460,7 +441,6 @@ namespace smt { expr_ref lhs_terms(mk_and(lhs), m); expr_ref rhs_terms(mk_and(rhs), m); assert_implication(lhs_terms, rhs_terms); - regex_axiom_add = true; } } } else { @@ -482,7 +462,6 @@ namespace smt { } regex_automaton_assumptions[re].push_back(new_aut); TRACE("str", tout << "add new automaton for " << mk_pp(re, m) << ": no assumptions" << std::endl;); - regex_axiom_add = true; find_automaton_initial_bounds(str_in_re, aut); } else { // TODO check negation? @@ -519,7 +498,6 @@ namespace smt { } regex_automaton_assumptions[re].push_back(new_aut); TRACE("str", tout << "add new automaton for " << mk_pp(re, m) << ": no assumptions" << std::endl;); - regex_axiom_add = true; find_automaton_initial_bounds(str_in_re, aut); } else { regex_inc_counter(regex_fail_count, str_in_re); @@ -704,7 +682,6 @@ namespace smt { expr_ref rhs2(ctx.mk_eq_atom(mk_strlen(str), m_autil.mk_numeral(rational::zero(), true)), m); expr_ref rhs(m.mk_and(rhs1, rhs2), m); assert_implication(conflict_lhs, rhs); - regex_axiom_add = true; } } } @@ -714,11 +691,8 @@ namespace smt { expr_ref conflict_clause(m.mk_not(mk_and(conflict_terms)), m); assert_axiom(conflict_clause); add_persisted_axiom(conflict_clause); - regex_axiom_add = true; } } // foreach (entry in regex_terms_by_string) - // NSB: compiler warns that regex_axiom_add is set but not used. - (void)regex_axiom_add; return true; } @@ -1464,12 +1438,6 @@ namespace smt { if (u.is_const_char(range_lo, lo_val) && u.is_const_char(range_hi, hi_val)) { TRACE("str", tout << "make range predicate from " << lo_val << " to " << hi_val << std::endl;); expr_ref cond_rhs(m); - - if (hi_val < lo_val) { - // NSB: why? The range would be empty. - std::swap(lo_val, hi_val); - } - expr_ref_vector cond_rhs_terms(m); for (unsigned i = lo_val; i <= hi_val; ++i) { zstring str_const(i);