mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
substr bugfix
This commit is contained in:
parent
a570149b57
commit
50e2273dbd
|
@ -431,18 +431,47 @@ br_status str_rewriter::mk_str_from_int(expr * arg0, expr_ref & result) {
|
|||
|
||||
br_status str_rewriter::mk_str_Substr(expr * base, expr * start, expr * len, expr_ref & result) {
|
||||
TRACE("t_str_rw", tout << "rewrite (Substr " << mk_pp(base, m()) << " " << mk_pp(start, m()) << " " << mk_pp(len, m()) << ")" << std::endl;);
|
||||
rational startVal, lenVal;
|
||||
if (m_strutil.is_string(base) && m_autil.is_numeral(start, startVal) && m_autil.is_numeral(len, lenVal)) {
|
||||
std::string baseStr = m_strutil.get_string_constant_value(base);
|
||||
// TODO handling for invalid start/len
|
||||
if (startVal.is_nonneg() && lenVal.is_nonneg() && startVal.get_unsigned() <= baseStr.length()) {
|
||||
TRACE("t_str_rw", tout << "rewriting constant Substr expression" << std::endl;);
|
||||
std::string substr = baseStr.substr(startVal.get_unsigned(), lenVal.get_unsigned());
|
||||
result = m_strutil.mk_string(substr);
|
||||
|
||||
bool constant_base = m_strutil.is_string(base);
|
||||
std::string baseStr;
|
||||
if (constant_base) {
|
||||
baseStr = m_strutil.get_string_constant_value(base);
|
||||
}
|
||||
rational startVal;
|
||||
bool constant_start = m_autil.is_numeral(start, startVal);
|
||||
rational lenVal;
|
||||
bool constant_len = m_autil.is_numeral(len, lenVal);
|
||||
|
||||
// case 1: start < 0 or len < 0
|
||||
if ( (constant_start && startVal.is_neg()) || (constant_len && lenVal.is_neg()) ) {
|
||||
TRACE("t_str_rw", tout << "start/len of substr is negative" << std::endl;);
|
||||
result = m_strutil.mk_string("");
|
||||
return BR_DONE;
|
||||
}
|
||||
// case 1.1: start >= length(base)
|
||||
if (constant_start && constant_base) {
|
||||
rational baseStrlen((unsigned int)baseStr.length());
|
||||
if (startVal >= baseStrlen) {
|
||||
TRACE("t_str_rw", tout << "start >= strlen for substr" << std::endl;);
|
||||
result = m_strutil.mk_string("");
|
||||
return BR_DONE;
|
||||
}
|
||||
}
|
||||
|
||||
if (constant_base && constant_start && constant_len) {
|
||||
rational baseStrlen((unsigned int)baseStr.length());
|
||||
std::string retval;
|
||||
if (startVal + lenVal >= baseStrlen) {
|
||||
// case 2: pos+len goes past the end of the string
|
||||
retval = baseStr.substr(startVal.get_unsigned(), std::string::npos);
|
||||
} else {
|
||||
// case 3: pos+len still within string
|
||||
retval = baseStr.substr(startVal.get_unsigned(), lenVal.get_unsigned());
|
||||
}
|
||||
result = m_strutil.mk_string(retval);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
|
|
|
@ -1579,6 +1579,86 @@ void theory_str::instantiate_axiom_Substr(enode * e) {
|
|||
|
||||
TRACE("t_str_detail", tout << "instantiate Substr axiom for " << mk_pp(expr, m) << std::endl;);
|
||||
|
||||
expr_ref substrBase(expr->get_arg(0), m);
|
||||
expr_ref substrPos(expr->get_arg(1), m);
|
||||
expr_ref substrLen(expr->get_arg(2), m);
|
||||
SASSERT(substrBase);
|
||||
SASSERT(substrPos);
|
||||
SASSERT(substrLen);
|
||||
|
||||
expr_ref zero(m_autil.mk_numeral(rational::zero(), true), m);
|
||||
expr_ref minusOne(m_autil.mk_numeral(rational::minus_one(), true), m);
|
||||
SASSERT(zero);
|
||||
SASSERT(minusOne);
|
||||
|
||||
expr_ref_vector argumentsValid_terms(m);
|
||||
// pos >= 0
|
||||
argumentsValid_terms.push_back(m_autil.mk_ge(substrPos, zero));
|
||||
// pos < strlen(base)
|
||||
// --> pos + -1*strlen(base) < 0
|
||||
argumentsValid_terms.push_back(m.mk_not(m_autil.mk_ge(
|
||||
m_autil.mk_add(substrPos, m_autil.mk_mul(minusOne, substrLen)),
|
||||
zero)));
|
||||
// len >= 0
|
||||
argumentsValid_terms.push_back(m_autil.mk_ge(substrLen, zero));
|
||||
|
||||
expr_ref argumentsValid(mk_and(argumentsValid_terms), m);
|
||||
SASSERT(argumentsValid);
|
||||
ctx.internalize(argumentsValid, false);
|
||||
|
||||
// (pos+len) >= strlen(base)
|
||||
// --> pos + len + -1*strlen(base) >= 0
|
||||
expr_ref lenOutOfBounds(m_autil.mk_ge(
|
||||
m_autil.mk_add(substrPos, substrLen, m_autil.mk_mul(minusOne, mk_strlen(substrBase))),
|
||||
zero), m);
|
||||
SASSERT(lenOutOfBounds);
|
||||
ctx.internalize(argumentsValid, false);
|
||||
|
||||
// Case 1: pos < 0 or pos >= strlen(base) or len < 0
|
||||
// ==> (Substr ...) = ""
|
||||
expr_ref case1_premise(m.mk_not(argumentsValid), m);
|
||||
SASSERT(case1_premise);
|
||||
ctx.internalize(case1_premise, false);
|
||||
expr_ref case1_conclusion(ctx.mk_eq_atom(expr, mk_string("")), m);
|
||||
SASSERT(case1_conclusion);
|
||||
ctx.internalize(case1_conclusion, false);
|
||||
expr_ref case1(rewrite_implication(case1_premise, case1_conclusion), m);
|
||||
SASSERT(case1);
|
||||
|
||||
// Case 2: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) >= strlen(base)
|
||||
// ==> base = t0.t1 AND len(t0) = pos AND (Substr ...) = t1
|
||||
expr_ref t0(mk_str_var("t0"), m);
|
||||
expr_ref t1(mk_str_var("t1"), m);
|
||||
expr_ref case2_conclusion(m.mk_and(
|
||||
ctx.mk_eq_atom(substrBase, mk_concat(t0,t1)),
|
||||
ctx.mk_eq_atom(mk_strlen(t0), substrPos),
|
||||
ctx.mk_eq_atom(expr, t1)), m);
|
||||
expr_ref case2(rewrite_implication(m.mk_and(argumentsValid, lenOutOfBounds), case2_conclusion), m);
|
||||
SASSERT(case2);
|
||||
|
||||
// Case 3: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) < strlen(base)
|
||||
// ==> base = t2.t3.t4 AND len(t2) = pos AND len(t3) = len AND (Substr ...) = t3
|
||||
expr_ref t2(mk_str_var("t2"), m);
|
||||
expr_ref t3(mk_str_var("t3"), m);
|
||||
expr_ref t4(mk_str_var("t4"), m);
|
||||
expr_ref_vector case3_conclusion_terms(m);
|
||||
case3_conclusion_terms.push_back(ctx.mk_eq_atom(substrBase, mk_concat(t2, mk_concat(t3, t4))));
|
||||
case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t2), substrPos));
|
||||
case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t3), substrLen));
|
||||
case3_conclusion_terms.push_back(ctx.mk_eq_atom(expr, t3));
|
||||
expr_ref case3_conclusion(mk_and(case3_conclusion_terms), m);
|
||||
expr_ref case3(rewrite_implication(m.mk_and(argumentsValid, m.mk_not(lenOutOfBounds)), case3_conclusion), m);
|
||||
SASSERT(case3);
|
||||
|
||||
ctx.internalize(case1, false);
|
||||
ctx.internalize(case2, false);
|
||||
ctx.internalize(case3, false);
|
||||
|
||||
expr_ref finalAxiom(m.mk_and(case1, case2, case3), m);
|
||||
SASSERT(finalAxiom);
|
||||
assert_axiom(finalAxiom);
|
||||
|
||||
/*
|
||||
expr_ref ts0(mk_str_var("ts0"), m);
|
||||
expr_ref ts1(mk_str_var("ts1"), m);
|
||||
expr_ref ts2(mk_str_var("ts2"), m);
|
||||
|
@ -1601,6 +1681,7 @@ void theory_str::instantiate_axiom_Substr(enode * e) {
|
|||
expr_ref finalAxiom(m.mk_and(breakdownAssert, reduceToVar), m);
|
||||
SASSERT(finalAxiom);
|
||||
assert_axiom(finalAxiom);
|
||||
*/
|
||||
}
|
||||
|
||||
void theory_str::instantiate_axiom_Replace(enode * e) {
|
||||
|
|
Loading…
Reference in a new issue