From 225b527d5832848bc80bc3406b3fafde36d581a8 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 6 Dec 2016 16:09:38 -0500 Subject: [PATCH] boolean case split theory_str process_concat_eq_type2 --- src/smt/theory_str.cpp | 35 +++++++++++++++++------------------ 1 file changed, 17 insertions(+), 18 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 4b38d02d3..ef86be313 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -3328,8 +3328,8 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { } else { // Split type -1: no idea about the length... int optionTotal = 2 + strValue.length(); - expr_ref_vector or_item(mgr); - expr_ref_vector and_item(mgr); + expr_ref_vector arrangement_disjunction(mgr); + int option = 0; int pos = 1; @@ -3339,16 +3339,16 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { if (can_two_nodes_eq(y, temp1_strAst)) { if (!avoidLoopCut || !has_self_cut(m, y)) { // break down option 2-1 - expr_ref current_or_item_option(ctx.mk_eq_atom(xorFlag, mk_int(option)), mgr); - or_item.push_back(current_or_item_option); + expr_ref_vector and_item(mgr); + expr_ref x_temp1(mk_concat(x, temp1), mgr); - and_item.push_back(ctx.mk_eq_atom(current_or_item_option, ctx.mk_eq_atom(m, x_temp1))); - and_item.push_back(ctx.mk_eq_atom(current_or_item_option, ctx.mk_eq_atom(y, temp1_strAst))); + and_item.push_back(ctx.mk_eq_atom(m, x_temp1)); + and_item.push_back(ctx.mk_eq_atom(y, temp1_strAst)); - and_item.push_back(ctx.mk_eq_atom(current_or_item_option, ctx.mk_eq_atom(mk_strlen(m), - m_autil.mk_add(mk_strlen(x), mk_strlen(temp1))))); + and_item.push_back(ctx.mk_eq_atom(mk_strlen(m), + m_autil.mk_add(mk_strlen(x), mk_strlen(temp1)))); - ++option; + arrangement_disjunction.push_back(mk_and(and_item)); add_cut_info_merge(temp1, ctx.get_scope_level(), y); add_cut_info_merge(temp1, ctx.get_scope_level(), m); } else { @@ -3366,18 +3366,16 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { expr_ref cropStr(m_strutil.mk_string(part2Str), mgr); if (can_two_nodes_eq(x, x_concat) && can_two_nodes_eq(y, cropStr)) { // break down option 2-2 - expr_ref current_or_item_option(ctx.mk_eq_atom(xorFlag, mk_int(option)), mgr); - or_item.push_back(current_or_item_option); - and_item.push_back(ctx.mk_eq_atom(current_or_item_option, ctx.mk_eq_atom(x, x_concat))); - and_item.push_back(ctx.mk_eq_atom(current_or_item_option, ctx.mk_eq_atom(y, cropStr))); - and_item.push_back(ctx.mk_eq_atom(current_or_item_option, ctx.mk_eq_atom(mk_strlen(y), mk_int(part2Str.length())))); - ++option; + expr_ref_vector and_item(mgr); + and_item.push_back(ctx.mk_eq_atom(x, x_concat)); + and_item.push_back(ctx.mk_eq_atom(y, cropStr)); + and_item.push_back(ctx.mk_eq_atom(mk_strlen(y), mk_int(part2Str.length()))); + arrangement_disjunction.push_back(mk_and(and_item)); } } - if (option > 0) { - and_item.push_back(mk_or(or_item)); - expr_ref implyR(mk_and(and_item), mgr); + if (!arrangement_disjunction.empty()) { + expr_ref implyR(mk_or(arrangement_disjunction), mgr); if (opt_AssertStrongerArrangements) { expr_ref implyLHS(ctx.mk_eq_atom(concatAst1, concatAst2), mgr); @@ -3386,6 +3384,7 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { } else { assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR); } + assert_axiom(generate_mutual_exclusion(arrangement_disjunction)); } else { TRACE("t_str", tout << "STOP: Should not split two EQ concats." << std::endl;); }