mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

add overlap assumption to other cases in theory_str

Browse source
This commit is contained in:
Murphy Berzish 2017-04-13 13:46:23 -04:00
parent 7207cabc97
commit a7f72bf4ef
1 changed files with 49 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

49
src/smt/theory_str.cpp
View file

@ -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) { void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
ast_manager & mgr = get_manager(); ast_manager & mgr = get_manager();
context & ctx = get_context(); context & ctx = get_context();
bool overlapAssumptionUsed = false;
TRACE("t_str_detail", tout << "process_concat_eq TYPE 1" << std::endl TRACE("t_str_detail", tout << "process_concat_eq TYPE 1" << std::endl
<< "concatAst1 = " << mk_ismt2_pp(concatAst1, mgr) << std::endl << "concatAst1 = " << mk_ismt2_pp(concatAst1, mgr) << std::endl
<< "concatAst2 = " << mk_ismt2_pp(concatAst2, 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 { } else {
TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;); TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;);
TRACE("t_str_detail", {print_cut_var(m, tout); print_cut_var(y, tout);}); 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) { } else if (splitType == 1) {
@ -3132,6 +3140,11 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
} else { } else {
TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;); TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;);
TRACE("t_str_detail", {print_cut_var(m, tout); print_cut_var(y, tout);}); 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) { } else if (splitType == -1) {
@ -3183,6 +3196,11 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
} else { } else {
TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;); TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;);
TRACE("t_str_detail", {print_cut_var(m, tout); print_cut_var(y, tout);}); 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 { } else {
TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;); TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;);
TRACE("t_str_detail", {print_cut_var(x, tout); print_cut_var(n, tout);}); 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) { void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) {
ast_manager & mgr = get_manager(); ast_manager & mgr = get_manager();
context & ctx = get_context(); context & ctx = get_context();
bool overlapAssumptionUsed = false;
TRACE("t_str_detail", tout << "process_concat_eq TYPE 2" << std::endl TRACE("t_str_detail", tout << "process_concat_eq TYPE 2" << std::endl
<< "concatAst1 = " << mk_ismt2_pp(concatAst1, mgr) << std::endl << "concatAst1 = " << mk_ismt2_pp(concatAst1, mgr) << std::endl
<< "concatAst2 = " << mk_ismt2_pp(concatAst2, 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 { } else {
TRACE("t_str", tout << "AVOID LOOP: SKIP" << std::endl;); TRACE("t_str", tout << "AVOID LOOP: SKIP" << std::endl;);
TRACE("t_str_detail", {print_cut_var(m, tout); print_cut_var(y, tout);}); 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 { } else {
TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;); TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;);
TRACE("t_str_detail", {print_cut_var(m, tout); print_cut_var(y, tout);}); 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) { void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) {
ast_manager & mgr = get_manager(); ast_manager & mgr = get_manager();
context & ctx = get_context(); context & ctx = get_context();
bool overlapAssumptionUsed = false;
TRACE("t_str_detail", tout << "process_concat_eq TYPE 3" << std::endl TRACE("t_str_detail", tout << "process_concat_eq TYPE 3" << std::endl
<< "concatAst1 = " << mk_ismt2_pp(concatAst1, mgr) << std::endl << "concatAst1 = " << mk_ismt2_pp(concatAst1, mgr) << std::endl
<< "concatAst2 = " << mk_ismt2_pp(concatAst2, 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 { } else {
TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;); TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;);
TRACE("t_str_detail", {print_cut_var(x, tout); print_cut_var(n, tout);}); 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 { } else {
TRACE("t_str", tout << "AVOID LOOP: SKIPPED." << std::endl;); TRACE("t_str", tout << "AVOID LOOP: SKIPPED." << std::endl;);
TRACE("t_str_detail", {print_cut_var(x, tout); print_cut_var(n, tout);}); 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());
}
} }
} }
} }