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

refactor: aligned external/internal names for str.strong_arrangements option

Browse source
This commit is contained in:
Murphy Berzish 2017-02-23 16:00:05 -05:00
parent 3816779ba1
commit a7b21dc5d5
3 changed files with 21 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/params/theory_str_params.cpp
View file

@ -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();

4
src/smt/params/theory_str_params.h
View file

@ -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),

36
src/smt/theory_str.cpp
View file

@ -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 {