mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
z3str3: address code reviews and remove some dead code (#5116)
This commit is contained in:
parent
bf692a5076
commit
064b1f0721
|
@ -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)) {
|
||||
|
|
|
@ -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<expr>(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);
|
||||
|
|
Loading…
Reference in a new issue