mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

full upper bound refinement

Browse source
This commit is contained in:
Murphy Berzish 2018-01-03 12:02:11 -05:00
parent 0ac7082c80
commit 0917af7c56
1 changed files with 6 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/theory_str.cpp
View file

@ -9236,10 +9236,13 @@ namespace smt {
if (solution_at_upper_bound) {
if (refined_upper_bound.is_minus_one()) {
// If there are solutions at the upper bound but not below it, make the bound exact.
NOT_IMPLEMENTED_YET();
rhs.push_back(ctx.mk_eq_atom(str_len, m_autil.mk_numeral(upper_bound_value, true)));
} else {
// If there are solutions at and below the upper bound, add an additional bound.
NOT_IMPLEMENTED_YET();
rhs.push_back(m.mk_or(
ctx.mk_eq_atom(str_len, m_autil.mk_numeral(upper_bound_value, true)),
m_autil.mk_le(str_len, m_autil.mk_numeral(refined_upper_bound, true))
));
}
} else {
if (refined_upper_bound.is_minus_one()) {
@ -9247,7 +9250,7 @@ namespace smt {
rhs.push_back(m.mk_not(m_autil.mk_le(str_len, m_autil.mk_numeral(upper_bound_value, true))));
} else {
// If there are solutions below the upper bound but not at it, refine the bound.
NOT_IMPLEMENTED_YET();
rhs.push_back(m_autil.mk_le(str_len, m_autil.mk_numeral(refined_upper_bound, true)));
}
}