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

Revert "ref_vector refactoring in theory_str::check_length_concat_concat"

Browse source 
This reverts commit 599cc1e75d.
This commit is contained in:
Murphy Berzish 2016-12-01 15:19:51 -05:00
parent 548f635f7e
commit b020c71f8a
1 changed files with 5 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/smt/theory_str.cpp
View file

@ -5569,13 +5569,7 @@ bool theory_str::check_length_concat_concat(expr * n1, expr * n2) {
bool concat1LenFixed = true; bool concat1LenFixed = true;
bool concat2LenFixed = true; bool concat2LenFixed = true;
/* expr_ref_vector items(mgr);
* Refactored from the Z3str2 version.
* We delay creation of new terms until a conflict
* is actually detected.
*/
expr_ref_vector eq_args(mgr);
vector<rational> eq_lens;
rational sum1(0), sum2(0); rational sum1(0), sum2(0);
@ -5586,9 +5580,7 @@ bool theory_str::check_length_concat_concat(expr * n1, expr * n2) {
if (argLen_exists) { if (argLen_exists) {
sum1 += argLen; sum1 += argLen;
if (!m_strutil.is_string(oneArg)) { if (!m_strutil.is_string(oneArg)) {
// items.push_back(ctx.mk_eq_atom(mk_strlen(oneArg), mk_int(argLen))); items.push_back(ctx.mk_eq_atom(mk_strlen(oneArg), mk_int(argLen)));
eq_args.push_back(oneArg);
eq_lens.push_back(rational(argLen));
} }
} else { } else {
concat1LenFixed = false; concat1LenFixed = false;
@ -5602,15 +5594,15 @@ bool theory_str::check_length_concat_concat(expr * n1, expr * n2) {
if (argLen_exists) { if (argLen_exists) {
sum2 += argLen; sum2 += argLen;
if (!m_strutil.is_string(oneArg)) { if (!m_strutil.is_string(oneArg)) {
// items.push_back(ctx.mk_eq_atom(mk_strlen(oneArg), mk_int(argLen))); items.push_back(ctx.mk_eq_atom(mk_strlen(oneArg), mk_int(argLen)));
eq_args.push_back(oneArg);
eq_lens.push_back(rational(argLen));
} }
} else { } else {
concat2LenFixed = false; concat2LenFixed = false;
} }
} }
items.push_back(ctx.mk_eq_atom(n1, n2));
bool conflict = false; bool conflict = false;
if (concat1LenFixed && concat2LenFixed) { if (concat1LenFixed && concat2LenFixed) {
@ -5629,13 +5621,6 @@ bool theory_str::check_length_concat_concat(expr * n1, expr * n2) {
if (conflict) { if (conflict) {
TRACE("t_str_detail", tout << "inconsistent length detected in concat <==> concat" << std::endl;); TRACE("t_str_detail", tout << "inconsistent length detected in concat <==> concat" << std::endl;);
expr_ref_vector items(mgr);
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)));
}
items.push_back(ctx.mk_eq_atom(n1, n2));
expr_ref toAssert(mgr.mk_not(mk_and(items)), mgr); expr_ref toAssert(mgr.mk_not(mk_and(items)), mgr);
assert_axiom(toAssert); assert_axiom(toAssert);
return false; return false;