From 5e7806c4a45dfb694c51ed4463944f990b28ddc0 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 13 May 2020 14:32:44 -0400 Subject: [PATCH] z3str3: use rational in place of unsigned during model construction --- src/smt/theory_str.cpp | 43 +++++++++++++++++++++++---------------- src/smt/theory_str.h | 4 ++-- src/smt/theory_str_mc.cpp | 16 +++++++-------- 3 files changed, 36 insertions(+), 27 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index c9904996e..e1325d06c 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -8833,7 +8833,7 @@ namespace smt { out << "TODO: theory_str display" << std::endl; } - unsigned theory_str::get_refine_length(expr* ex, expr_ref_vector& extra_deps){ + rational theory_str::get_refine_length(expr* ex, expr_ref_vector& extra_deps){ ast_manager & m = get_manager(); TRACE("str_fl", tout << "finding length for " << mk_ismt2_pp(ex, m) << std::endl;); @@ -8843,7 +8843,7 @@ namespace smt { SASSERT(str_exists); zstring str_const; u.str.is_string(str, str_const); - return str_const.length(); + return rational(str_const.length()); } else if (u.str.is_itos(ex)) { expr* fromInt = nullptr; u.str.is_itos(ex, fromInt); @@ -8855,7 +8855,7 @@ namespace smt { std::string s = std::to_string(val.get_int32()); extra_deps.push_back(ctx.mk_eq_atom(fromInt, mk_int(val))); - return static_cast(s.length()); + return rational((unsigned)s.length()); } else if (u.str.is_at(ex)) { expr* substrBase = nullptr; @@ -8867,7 +8867,7 @@ namespace smt { VERIFY(v.get_value(substrPos, pos)); extra_deps.push_back(ctx.mk_eq_atom(substrPos, mk_int(pos))); - return 1; + return rational::one(); } else if (u.str.is_extract(ex)) { expr* substrBase = nullptr; @@ -8881,7 +8881,7 @@ namespace smt { VERIFY(v.get_value(substrPos, pos)); extra_deps.push_back(ctx.mk_eq_atom(substrPos, mk_int(pos))); - return len.get_unsigned(); + return len; } else if (u.str.is_replace(ex)) { TRACE("str_fl", tout << "replace is like contains---not in conjunctive fragment!" << std::endl;); @@ -8917,8 +8917,8 @@ namespace smt { return nullptr; } - expr* theory_str::refine_eq(expr* lhs, expr* rhs, unsigned offset) { - TRACE("str_fl", tout << "refine eq " << offset << std::endl;); + expr* theory_str::refine_eq(expr* lhs, expr* rhs, unsigned _offset) { + TRACE("str_fl", tout << "refine eq " << _offset << std::endl;); ast_manager & m = get_manager(); expr_ref_vector Gamma(m); @@ -8929,9 +8929,11 @@ namespace smt { } expr_ref_vector extra_deps(m); + rational offset(_offset); // find len(Gamma[:i]) - unsigned left_count = 0, left_length = 0, last_length = 0; + unsigned left_count = 0; + rational left_length(0), last_length(0); while(left_count < Gamma.size() && left_length <= offset) { last_length = get_refine_length(Gamma.get(left_count), extra_deps); left_length += last_length; @@ -8947,7 +8949,8 @@ namespace smt { if (!u.str.is_string(to_app(Gamma.get(i)))) { len = u.str.mk_length(Gamma.get(i)); } else { - len = mk_int(offset - left_length); + rational lenDiff = offset - left_length; + len = mk_int(lenDiff); } if (left_sublen == nullptr) { left_sublen = len; @@ -8956,19 +8959,22 @@ namespace smt { } } if (offset - left_length != 0) { + rational lenDiff = offset - left_length; if (left_sublen == nullptr) { - left_sublen = mk_int(offset - left_length); + left_sublen = mk_int(lenDiff); } else { - left_sublen = m_autil.mk_add(left_sublen, mk_int(offset - left_length)); + left_sublen = m_autil.mk_add(left_sublen, mk_int(lenDiff)); } } expr* extra_left_cond = nullptr; if (!u.str.is_string(to_app(Gamma.get(left_count)))) { - extra_left_cond = m_autil.mk_ge(u.str.mk_length(Gamma.get(left_count)), mk_int(offset - left_length + 1)); + rational offsetLen = offset - left_length + 1; + extra_left_cond = m_autil.mk_ge(u.str.mk_length(Gamma.get(left_count)), mk_int(offsetLen)); } // find len(Delta[:j]) - unsigned right_count = 0, right_length = 0; + unsigned right_count = 0; + rational right_length(0); last_length = 0; while(right_count < Delta.size() && right_length <= offset) { last_length = get_refine_length(Delta.get(right_count), extra_deps); @@ -8985,7 +8991,8 @@ namespace smt { if (!u.str.is_string(to_app(Delta.get(i)))) { len = u.str.mk_length(Delta.get(i)); } else { - len = mk_int(offset - right_length); + rational offsetLen = offset - right_length; + len = mk_int(offsetLen); } if (right_sublen == nullptr) { right_sublen = len; @@ -8994,15 +9001,17 @@ namespace smt { } } if (offset - right_length != 0) { + rational offsetLen = offset - right_length; if (right_sublen == nullptr) { - right_sublen = mk_int(offset - right_length); + right_sublen = mk_int(offsetLen); } else { - right_sublen = m_autil.mk_add(right_sublen, mk_int(offset - right_length)); + right_sublen = m_autil.mk_add(right_sublen, mk_int(offsetLen)); } } expr* extra_right_cond = nullptr; if (!u.str.is_string(to_app(Delta.get(right_count)))) { - extra_right_cond = m_autil.mk_ge(u.str.mk_length(Delta.get(right_count)), mk_int(offset - right_length + 1)); + rational offsetLen = offset - right_length + 1; + extra_right_cond = m_autil.mk_ge(u.str.mk_length(Delta.get(right_count)), mk_int(offsetLen)); } // Offset tells us that Gamma[i+1:]) != Delta[j+1:] diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 34f371219..6c51a4f95 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -543,7 +543,7 @@ protected: // fixed length model construction expr_ref_vector fixed_length_subterm_trail; // trail for subterms generated *in the subsolver* expr_ref_vector fixed_length_assumptions; // cache of boolean terms to assert *into the subsolver*, unsat core is a subset of these - obj_map fixed_length_used_len_terms; // constraints used in generating fixed length model + obj_map fixed_length_used_len_terms; // constraints used in generating fixed length model obj_map > var_to_char_subterm_map; // maps a var to a list of character terms *in the subsolver* obj_map > uninterpreted_to_char_subterm_map; // maps an "uninterpreted" string term to a list of character terms *in the subsolver* obj_map> fixed_length_lesson; //keep track of information for the lesson @@ -603,7 +603,7 @@ protected: expr* refine_dis(expr* lhs, expr* rhs); expr* refine_function(expr* f); bool flatten(expr* ex, expr_ref_vector & flat); - unsigned get_refine_length(expr* ex, expr_ref_vector& extra_deps); + rational get_refine_length(expr* ex, expr_ref_vector& extra_deps); void instantiate_axiom_CharAt(enode * e); void instantiate_axiom_prefixof(enode * e); diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp index 9949ac740..6518a0186 100644 --- a/src/smt/theory_str_mc.cpp +++ b/src/smt/theory_str_mc.cpp @@ -624,17 +624,16 @@ namespace smt { cex = expr_ref(m_autil.mk_ge(mk_strlen(term), mk_int(0)), m); return false; } - SASSERT(varLen_value.is_unsigned() && "actually arithmetic solver can assign it a very large number"); TRACE("str_fl", tout << "creating character terms for variable " << mk_pp(term, m) << ", length = " << varLen_value << std::endl;); ptr_vector new_chars; - for (unsigned i = 0; i < varLen_value.get_unsigned(); ++i) { + for (rational i = rational::zero(); i < varLen_value; ++i) { // TODO we can probably name these better for the sake of debugging expr_ref ch(mk_fresh_const("char", bv8_sort), m); new_chars.push_back(ch); fixed_length_subterm_trail.push_back(ch); } var_to_char_subterm_map.insert(term, new_chars); - fixed_length_used_len_terms.insert(term, varLen_value.get_unsigned()); + fixed_length_used_len_terms.insert(term, varLen_value); } var_to_char_subterm_map.find(term, eqc_chars); } else if (u.str.is_concat(term, arg0, arg1)) { @@ -754,13 +753,13 @@ namespace smt { } TRACE("str_fl", tout << "creating character terms for uninterpreted function " << mk_pp(term, m) << ", length = " << ufLen_value << std::endl;); ptr_vector new_chars; - for (unsigned i = 0; i < ufLen_value.get_unsigned(); ++i) { + for (rational i = rational::zero(); i < ufLen_value; ++i) { expr_ref ch(mk_fresh_const("char", bv8_sort), m); new_chars.push_back(ch); fixed_length_subterm_trail.push_back(ch); } uninterpreted_to_char_subterm_map.insert(term, new_chars); - fixed_length_used_len_terms.insert(term, ufLen_value.get_unsigned()); + fixed_length_used_len_terms.insert(term, ufLen_value); } uninterpreted_to_char_subterm_map.find(term, eqc_chars); } @@ -794,7 +793,6 @@ namespace smt { fixed_length_assumptions.push_back(_e); fixed_length_lesson.insert(_e, std::make_tuple(rational(i), lhs, rhs)); } - // fixed_length_used_len_terms.push_back(get_context().mk_eq_atom(lhs, rhs)); return true; } @@ -1056,7 +1054,8 @@ namespace smt { for (auto e : fixed_length_used_len_terms) { expr * var = &e.get_key(); - precondition.push_back(m.mk_eq(u.str.mk_length(var), mk_int(e.get_value()))); + rational val = e.get_value(); + precondition.push_back(m.mk_eq(u.str.mk_length(var), mk_int(val))); } TRACE("str_fl", @@ -1172,7 +1171,8 @@ namespace smt { TRACE("str_fl", tout << "subsolver found UNSAT; constructing length counterexample" << std::endl;); for (auto e : fixed_length_used_len_terms) { expr * var = &e.get_key(); - cex.push_back(m.mk_eq(u.str.mk_length(var), mk_int(e.get_value()))); + rational val = e.get_value(); + cex.push_back(m.mk_eq(u.str.mk_length(var), mk_int(val))); } return l_false; } else {