From a7b21dc5d51c3256ecadccc499b8b310af2ab31e Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 23 Feb 2017 16:00:05 -0500 Subject: [PATCH] refactor: aligned external/internal names for str.strong_arrangements option --- src/smt/params/theory_str_params.cpp | 2 +- src/smt/params/theory_str_params.h | 4 ++-- src/smt/theory_str.cpp | 36 ++++++++++++++-------------- 3 files changed, 21 insertions(+), 21 deletions(-) diff --git a/src/smt/params/theory_str_params.cpp b/src/smt/params/theory_str_params.cpp index f86cd9379..6090086b8 100644 --- a/src/smt/params/theory_str_params.cpp +++ b/src/smt/params/theory_str_params.cpp @@ -20,7 +20,7 @@ Revision History: void theory_str_params::updt_params(params_ref const & _p) { smt_params_helper p(_p); - m_AssertStrongerArrangements = p.str_strong_arrangements(); + m_StrongArrangements = p.str_strong_arrangements(); m_AggressiveLengthTesting = p.str_aggressive_length_testing(); m_AggressiveValueTesting = p.str_aggressive_value_testing(); m_AggressiveUnrollTesting = p.str_aggressive_unroll_testing(); diff --git a/src/smt/params/theory_str_params.h b/src/smt/params/theory_str_params.h index de0945395..207b635d7 100644 --- a/src/smt/params/theory_str_params.h +++ b/src/smt/params/theory_str_params.h @@ -28,7 +28,7 @@ struct theory_str_params { * This is a stronger version of the standard axiom. * The Z3str2 axioms can be simulated by setting this to false. */ - bool m_AssertStrongerArrangements; + bool m_StrongArrangements; /* * If AggressiveLengthTesting is true, we manipulate the phase of length tester equalities @@ -81,7 +81,7 @@ struct theory_str_params { double m_OverlapTheoryAwarePriority; theory_str_params(params_ref const & p = params_ref()): - m_AssertStrongerArrangements(true), + m_StrongArrangements(true), m_AggressiveLengthTesting(false), m_AggressiveValueTesting(false), m_AggressiveUnrollTesting(true), diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index b78cbbe59..80781d6aa 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -3079,7 +3079,7 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { add_cut_info_merge(t1, sLevel, m); add_cut_info_merge(t1, sLevel, y); - if (m_params.m_AssertStrongerArrangements) { + if (m_params.m_StrongArrangements) { expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr); assert_axiom(ax_strong); } else { @@ -3137,7 +3137,7 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { add_cut_info_merge(t2, sLevel, x); add_cut_info_merge(t2, sLevel, n); - if (m_params.m_AssertStrongerArrangements) { + if (m_params.m_StrongArrangements) { expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr); assert_axiom(ax_strong); } else { @@ -3272,7 +3272,7 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { if (!arrangement_disjunction.empty()) { expr_ref premise(ctx.mk_eq_atom(concatAst1, concatAst2), mgr); expr_ref conclusion(mk_or(arrangement_disjunction), mgr); - if (m_params.m_AssertStrongerArrangements) { + if (m_params.m_StrongArrangements) { expr_ref ax_strong(ctx.mk_eq_atom(premise, conclusion), mgr); assert_axiom(ax_strong); } else { @@ -3472,7 +3472,7 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { add_cut_info_merge(temp1, sLevel, y); add_cut_info_merge(temp1, sLevel, m); - if (m_params.m_AssertStrongerArrangements) { + if (m_params.m_StrongArrangements) { expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr); assert_axiom(ax_strong); } else { @@ -3547,7 +3547,7 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { expr_ref ax_l(mk_and(l_items), mgr); expr_ref ax_r(mk_and(r_items), mgr); - if (m_params.m_AssertStrongerArrangements) { + if (m_params.m_StrongArrangements) { expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr); assert_axiom(ax_strong); } else { @@ -3628,7 +3628,7 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { if (!arrangement_disjunction.empty()) { expr_ref implyR(mk_or(arrangement_disjunction), mgr); - if (m_params.m_AssertStrongerArrangements) { + if (m_params.m_StrongArrangements) { expr_ref implyLHS(ctx.mk_eq_atom(concatAst1, concatAst2), mgr); expr_ref ax_strong(ctx.mk_eq_atom(implyLHS, implyR), mgr); assert_axiom(ax_strong); @@ -3816,7 +3816,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { r_items.push_back(ctx.mk_eq_atom(x, prefixAst)); r_items.push_back(ctx.mk_eq_atom(y, suf_n_concat)); - if (m_params.m_AssertStrongerArrangements) { + if (m_params.m_StrongArrangements) { expr_ref ax_strong(ctx.mk_eq_atom(ax_l, mk_and(r_items)), mgr); assert_axiom(ax_strong); } else { @@ -3836,7 +3836,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { expr_ref ax_l(mgr.mk_and(ax_l1, ax_l2), mgr); expr_ref ax_r(mgr.mk_and(ctx.mk_eq_atom(x, strAst), ctx.mk_eq_atom(y, n)), mgr); - if (m_params.m_AssertStrongerArrangements) { + if (m_params.m_StrongArrangements) { expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr); assert_axiom(ax_strong); } else { @@ -3874,7 +3874,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { add_cut_info_merge(temp1, sLevel, x); add_cut_info_merge(temp1, sLevel, n); - if (m_params.m_AssertStrongerArrangements) { + if (m_params.m_StrongArrangements) { expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr); assert_axiom(ax_strong); } else { @@ -3977,7 +3977,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { if (!arrangement_disjunction.empty()) { expr_ref implyR(mk_or(arrangement_disjunction), mgr); - if (m_params.m_AssertStrongerArrangements) { + if (m_params.m_StrongArrangements) { expr_ref ax_lhs(ctx.mk_eq_atom(concatAst1, concatAst2), mgr); expr_ref ax_strong(ctx.mk_eq_atom(ax_lhs, implyR), mgr); assert_axiom(ax_strong); @@ -4059,7 +4059,7 @@ void theory_str::process_concat_eq_type4(expr * concatAst1, expr * concatAst2) { if (!in_same_eqc(tmpAst, n)) { // break down option 4-1 expr_ref implyR(ctx.mk_eq_atom(n, tmpAst), mgr); - if (m_params.m_AssertStrongerArrangements) { + if (m_params.m_StrongArrangements) { expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr); assert_axiom(ax_strong); } else { @@ -4071,7 +4071,7 @@ void theory_str::process_concat_eq_type4(expr * concatAst1, expr * concatAst2) { //break down option 4-2 expr_ref implyR(ctx.mk_eq_atom(n, y), mgr); - if (m_params.m_AssertStrongerArrangements) { + if (m_params.m_StrongArrangements) { expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr); assert_axiom(ax_strong); } else { @@ -4084,7 +4084,7 @@ void theory_str::process_concat_eq_type4(expr * concatAst1, expr * concatAst2) { if (!in_same_eqc(y, tmpAst)) { //break down option 4-3 expr_ref implyR(ctx.mk_eq_atom(y, tmpAst), mgr); - if (m_params.m_AssertStrongerArrangements) { + if (m_params.m_StrongArrangements) { expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr); assert_axiom(ax_strong); } else { @@ -4161,7 +4161,7 @@ void theory_str::process_concat_eq_type5(expr * concatAst1, expr * concatAst2) { expr_ref x_deltaStr(mk_concat(x, mk_string(deltaStr)), mgr); if (!in_same_eqc(m, x_deltaStr)) { expr_ref implyR(ctx.mk_eq_atom(m, x_deltaStr), mgr); - if (m_params.m_AssertStrongerArrangements) { + if (m_params.m_StrongArrangements) { expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr); assert_axiom(ax_strong); } else { @@ -4172,7 +4172,7 @@ void theory_str::process_concat_eq_type5(expr * concatAst1, expr * concatAst2) { // test if (!in_same_eqc(x, m)) { expr_ref implyR(ctx.mk_eq_atom(x, m), mgr); - if (m_params.m_AssertStrongerArrangements) { + if (m_params.m_StrongArrangements) { expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr); assert_axiom(ax_strong); } else { @@ -4184,7 +4184,7 @@ void theory_str::process_concat_eq_type5(expr * concatAst1, expr * concatAst2) { expr_ref m_deltaStr(mk_concat(m, mk_string(deltaStr)), mgr); if (!in_same_eqc(x, m_deltaStr)) { expr_ref implyR(ctx.mk_eq_atom(x, m_deltaStr), mgr); - if (m_params.m_AssertStrongerArrangements) { + if (m_params.m_StrongArrangements) { expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr); assert_axiom(ax_strong); } else { @@ -4420,7 +4420,7 @@ void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) { expr_ref implyR(mk_or(arrangement_disjunction), mgr); - if (m_params.m_AssertStrongerArrangements) { + if (m_params.m_StrongArrangements) { expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr); assert_axiom(ax_strong); } else { @@ -6515,7 +6515,7 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { assert_axiom(negate_ast); } else { implyR1 = mk_or(arrangement_disjunction); - if (m_params.m_AssertStrongerArrangements) { + if (m_params.m_StrongArrangements) { expr_ref ax_strong(ctx.mk_eq_atom(implyL, implyR1), m); assert_axiom(ax_strong); } else {