From 406b622f59c92caa59f7e2713f4d6f8d67d32ae4 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 1 Dec 2016 15:19:51 -0500 Subject: [PATCH] Revert "testing term generation refactor in theory_str::check_length_const_string" This reverts commit edf151c9a0a3b0b69803f9944c6fc88bf1443a76. --- src/smt/theory_str.cpp | 23 ++--------------------- 1 file changed, 2 insertions(+), 21 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 76b605ff9..37be73333 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -5453,7 +5453,6 @@ bool theory_str::can_two_nodes_eq(expr * n1, expr * n2) { // case 0: n1_curr is const string, n2_curr is const string if (is_string(n1_curr) && is_string(n2_curr)) { if (n1_curr != n2_curr) { - // TODO confirm whether it's okay to compare the pointers like this return false; } } @@ -5495,18 +5494,8 @@ bool theory_str::check_length_const_string(expr * n1, expr * constStr) { rational strLen((unsigned) (m_strutil.get_string_constant_value(constStr).length())); if (is_concat(to_app(n1))) { - /* - * This has been refactored from Z3str2. - * We avoid creating new subexpressions until we actually detect a conflict. - * This may avoid a bit of overhead incurred by creating these terms. - */ - ptr_vector args; - - expr_ref_vector eq_args(mgr); - vector eq_lens; - // foreach (arg, len) in zip(eq_args, eq_lens): - // generate eq(mk_strlen(arg), mk_int(len)) + expr_ref_vector items(mgr); get_nodes_in_concat(n1, args); @@ -5516,20 +5505,12 @@ bool theory_str::check_length_const_string(expr * n1, expr * constStr) { bool argLen_exists = get_len_value(args[i], argLen); if (argLen_exists) { if (!m_strutil.is_string(args[i])) { - // items.push_back(ctx.mk_eq_atom(mk_strlen(args[i]), mk_int(argLen))); - eq_args.push_back(args[i]); - eq_lens.push_back(rational(argLen)); + items.push_back(ctx.mk_eq_atom(mk_strlen(args[i]), mk_int(argLen))); } TRACE("t_str_detail", tout << "concat arg: " << mk_pp(args[i], mgr) << " has len = " << argLen.to_string() << std::endl;); sumLen += argLen; if (sumLen > strLen) { - expr_ref_vector items(mgr); items.push_back(ctx.mk_eq_atom(n1, constStr)); - for (unsigned int z = 0; z < eq_args.size(); ++z) { - expr * arg = eq_args.get(z); - rational len = eq_lens.get(z); - items.push_back(ctx.mk_eq_atom(mk_strlen(arg), mk_int(len))); - } expr_ref toAssert(mgr.mk_not(mk_and(items)), mgr); TRACE("t_str_detail", tout << "inconsistent length: concat (len = " << sumLen << ") <==> string constant (len = " << strLen << ")" << std::endl;); assert_axiom(toAssert);