From a7f72bf4ef1a8c2aeb459accd2779c3f465f915f Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 13 Apr 2017 13:46:23 -0400 Subject: [PATCH] add overlap assumption to other cases in theory_str --- src/smt/theory_str.cpp | 49 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index b69ebda4c..9d3fef6d7 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -2898,6 +2898,9 @@ bool theory_str::is_concat_eq_type1(expr * concatAst1, expr * concatAst2) { void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { ast_manager & mgr = get_manager(); context & ctx = get_context(); + + bool overlapAssumptionUsed = false; + TRACE("t_str_detail", tout << "process_concat_eq TYPE 1" << std::endl << "concatAst1 = " << mk_ismt2_pp(concatAst1, mgr) << std::endl << "concatAst2 = " << mk_ismt2_pp(concatAst2, mgr) << std::endl; @@ -3074,6 +3077,11 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { } else { TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;); TRACE("t_str_detail", {print_cut_var(m, tout); print_cut_var(y, tout);}); + + if (!overlapAssumptionUsed) { + overlapAssumptionUsed = true; + assert_implication(ax_l, ctx.get_theory_str_overlap_assumption_term()); + } } } } else if (splitType == 1) { @@ -3132,6 +3140,11 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { } else { TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;); TRACE("t_str_detail", {print_cut_var(m, tout); print_cut_var(y, tout);}); + + if (!overlapAssumptionUsed) { + overlapAssumptionUsed = true; + assert_implication(ax_l, ctx.get_theory_str_overlap_assumption_term()); + } } } } else if (splitType == -1) { @@ -3183,6 +3196,11 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { } else { TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;); TRACE("t_str_detail", {print_cut_var(m, tout); print_cut_var(y, tout);}); + + if (!overlapAssumptionUsed) { + overlapAssumptionUsed = true; + arrangement_disjunction.push_back(ctx.get_theory_str_overlap_assumption_term()); + } } } @@ -3227,6 +3245,11 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { } else { TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;); TRACE("t_str_detail", {print_cut_var(x, tout); print_cut_var(n, tout);}); + + if (!overlapAssumptionUsed) { + overlapAssumptionUsed = true; + arrangement_disjunction.push_back(ctx.get_theory_str_overlap_assumption_term()); + } } } @@ -3286,6 +3309,9 @@ bool theory_str::is_concat_eq_type2(expr * concatAst1, expr * concatAst2) { void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { ast_manager & mgr = get_manager(); context & ctx = get_context(); + + bool overlapAssumptionUsed = false; + TRACE("t_str_detail", tout << "process_concat_eq TYPE 2" << std::endl << "concatAst1 = " << mk_ismt2_pp(concatAst1, mgr) << std::endl << "concatAst2 = " << mk_ismt2_pp(concatAst2, mgr) << std::endl; @@ -3466,6 +3492,11 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { } else { TRACE("t_str", tout << "AVOID LOOP: SKIP" << std::endl;); TRACE("t_str_detail", {print_cut_var(m, tout); print_cut_var(y, tout);}); + + if (!overlapAssumptionUsed) { + overlapAssumptionUsed = true; + assert_implication(ax_l, ctx.get_theory_str_overlap_assumption_term()); + } } } } @@ -3567,6 +3598,11 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { } else { TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;); TRACE("t_str_detail", {print_cut_var(m, tout); print_cut_var(y, tout);}); + + if (!overlapAssumptionUsed) { + overlapAssumptionUsed = true; + arrangement_disjunction.push_back(ctx.get_theory_str_overlap_assumption_term()); + } } } } @@ -3636,6 +3672,9 @@ bool theory_str::is_concat_eq_type3(expr * concatAst1, expr * concatAst2) { void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { ast_manager & mgr = get_manager(); context & ctx = get_context(); + + bool overlapAssumptionUsed = false; + TRACE("t_str_detail", tout << "process_concat_eq TYPE 3" << std::endl << "concatAst1 = " << mk_ismt2_pp(concatAst1, mgr) << std::endl << "concatAst2 = " << mk_ismt2_pp(concatAst2, mgr) << std::endl; @@ -3861,6 +3900,11 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { } else { TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;); TRACE("t_str_detail", {print_cut_var(x, tout); print_cut_var(n, tout);}); + + if (!overlapAssumptionUsed) { + overlapAssumptionUsed = true; + assert_implication(ax_l, ctx.get_theory_str_overlap_assumption_term()); + } } } } @@ -3940,6 +3984,11 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { } else { TRACE("t_str", tout << "AVOID LOOP: SKIPPED." << std::endl;); TRACE("t_str_detail", {print_cut_var(x, tout); print_cut_var(n, tout);}); + + if (!overlapAssumptionUsed) { + overlapAssumptionUsed = true; + arrangement_disjunction.push_back(ctx.get_theory_str_overlap_assumption_term()); + } } } }