mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 13:53:39 +00:00
Code Activity

check duplicate bounds info for regex terms

Browse source
This commit is contained in:
Murphy Berzish 2018-01-17 13:02:32 -05:00
parent e5585ecf4c
commit 26ab91a448
2 changed files with 35 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/smt/theory_str.cpp
View file

@ -9755,7 +9755,32 @@ namespace smt {
CTRACE("str", lower_bound_exists, tout << "lower bound of " << mk_pp(str, m) << " is " << lower_bound_value << std::endl;); CTRACE("str", lower_bound_exists, tout << "lower bound of " << mk_pp(str, m) << " is " << lower_bound_value << std::endl;);
CTRACE("str", upper_bound_exists, tout << "upper bound of " << mk_pp(str, m) << " is " << upper_bound_value << std::endl;); CTRACE("str", upper_bound_exists, tout << "upper bound of " << mk_pp(str, m) << " is " << upper_bound_value << std::endl;);
if (upper_bound_exists) { bool new_lower_bound_info = true;
bool new_upper_bound_info = true;
// check last seen lower/upper bound to avoid performing duplicate work
if (regex_last_lower_bound.contains(str)) {
rational last_lb_value;
regex_last_lower_bound.find(str, last_lb_value);
if (last_lb_value == lower_bound_value) {
new_lower_bound_info = false;
}
}
if (regex_last_upper_bound.contains(str)) {
rational last_ub_value;
regex_last_upper_bound.find(str, last_ub_value);
if (last_ub_value == upper_bound_value) {
new_upper_bound_info = false;
}
}
if (new_lower_bound_info) {
regex_last_lower_bound.insert(str, lower_bound_value);
}
if (new_upper_bound_info) {
regex_last_upper_bound.insert(str, upper_bound_value);
}
if (upper_bound_exists && new_upper_bound_info) {
// check current assumptions // check current assumptions
if (regex_automaton_assumptions.contains(re) && if (regex_automaton_assumptions.contains(re) &&
!regex_automaton_assumptions[re].empty()){ !regex_automaton_assumptions[re].empty()){
@ -9869,7 +9894,7 @@ namespace smt {
} }
} else { // !upper_bound_exists } else { // !upper_bound_exists
// no upper bound information // no upper bound information
if (lower_bound_exists && !lower_bound_value.is_zero()) { if (lower_bound_exists && !lower_bound_value.is_zero() && new_lower_bound_info) {
// nonzero lower bound, no upper bound // nonzero lower bound, no upper bound
// check current assumptions // check current assumptions
@ -9930,10 +9955,13 @@ namespace smt {
rhs.push_back(ctx.mk_eq_atom(str_len, m_autil.mk_numeral(lower_bound_value, true))); rhs.push_back(ctx.mk_eq_atom(str_len, m_autil.mk_numeral(lower_bound_value, true)));
} else { } else {
// If there are solutions at and above the lower bound, add an additional bound. // If there are solutions at and above the lower bound, add an additional bound.
// DISABLED as this is causing non-termination in the integer solver. --mtrberzi
/*
rhs.push_back(m.mk_or( rhs.push_back(m.mk_or(
ctx.mk_eq_atom(str_len, m_autil.mk_numeral(lower_bound_value, true)), ctx.mk_eq_atom(str_len, m_autil.mk_numeral(lower_bound_value, true)),
m_autil.mk_ge(str_len, m_autil.mk_numeral(refined_lower_bound, true)) m_autil.mk_ge(str_len, m_autil.mk_numeral(refined_lower_bound, true))
)); ));
*/
} }
} else { } else {
if (refined_lower_bound.is_minus_one()) { if (refined_lower_bound.is_minus_one()) {

5
src/smt/theory_str.h
View file

@ -413,6 +413,11 @@ protected:
obj_map<expr, expr*> regex_term_to_length_constraint; // (str.in.re S R) -> (length constraint over S wrt. R) obj_map<expr, expr*> regex_term_to_length_constraint; // (str.in.re S R) -> (length constraint over S wrt. R)
obj_map<expr, ptr_vector<expr> > regex_term_to_extra_length_vars; // extra length vars used in regex_term_to_length_constraint entries obj_map<expr, ptr_vector<expr> > regex_term_to_extra_length_vars; // extra length vars used in regex_term_to_length_constraint entries
// keep track of the last lower/upper bound we saw for each string term
// so we don't perform duplicate work
obj_map<expr, rational> regex_last_lower_bound;
obj_map<expr, rational> regex_last_upper_bound;
// each counter maps a (str.in.re) expression to an integer. // each counter maps a (str.in.re) expression to an integer.
// use helper functions regex_inc_counter() and regex_get_counter() to access // use helper functions regex_inc_counter() and regex_get_counter() to access
obj_map<expr, unsigned> regex_length_attempt_count; obj_map<expr, unsigned> regex_length_attempt_count;