diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 37be73333..3c6ad60ca 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -44,6 +44,7 @@ theory_str::theory_str(ast_manager & m): opt_CheckVariableScope(true), opt_UseFastLengthTesterCache(true), opt_UseFastValueTesterCache(true), + opt_AssertStrongerArrangements(true), /* Internal setup */ search_started(false), m_autil(m), @@ -2864,7 +2865,12 @@ 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); - assert_implication(ax_l, ax_r); + if (opt_AssertStrongerArrangements) { + expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr); + assert_axiom(ax_strong); + } else { + assert_implication(ax_l, ax_r); + } } else { loopDetected = true; TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;); @@ -2911,7 +2917,12 @@ 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); - assert_implication(ax_l, ax_r); + if (opt_AssertStrongerArrangements) { + expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr); + assert_axiom(ax_strong); + } else { + assert_implication(ax_l, ax_r); + } } else { loopDetected = true; TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;); @@ -3013,7 +3024,12 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { expr_ref premise(ctx.mk_eq_atom(concatAst1, concatAst2), mgr); expr_ref conclusion(mk_and(and_item), mgr); - assert_implication(premise, conclusion); + if (opt_AssertStrongerArrangements) { + expr_ref ax_strong(ctx.mk_eq_atom(premise, conclusion), mgr); + assert_axiom(ax_strong); + } else { + assert_implication(premise, conclusion); + } } else { TRACE("t_str", tout << "STOP: no split option found for two EQ concats." << std::endl;); } @@ -3206,7 +3222,12 @@ 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); - assert_implication(ax_l, ax_r); + if (opt_AssertStrongerArrangements) { + expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr); + assert_axiom(ax_strong); + } else { + assert_implication(ax_l, ax_r); + } } else { loopDetected = true; TRACE("t_str", tout << "AVOID LOOP: SKIP" << std::endl;); @@ -3269,7 +3290,12 @@ 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); - assert_implication(ax_l, ax_r); + if (opt_AssertStrongerArrangements) { + expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr); + assert_axiom(ax_strong); + } else { + assert_implication(ax_l, ax_r); + } } else { // negate! It's impossible to split str with these lengths TRACE("t_str", tout << "CONFLICT: Impossible to split str with these lengths." << std::endl;); @@ -3329,7 +3355,14 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { if (option > 0) { and_item.push_back(mk_or(or_item)); expr_ref implyR(mk_and(and_item), mgr); - assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR); + + if (opt_AssertStrongerArrangements) { + 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); + } else { + assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR); + } } else { TRACE("t_str", tout << "STOP: Should not split two EQ concats." << std::endl;); } @@ -3508,7 +3541,13 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { expr_ref_vector r_items(mgr); r_items.push_back(ctx.mk_eq_atom(x, prefixAst)); r_items.push_back(ctx.mk_eq_atom(y, suf_n_concat)); - assert_implication(ax_l, mk_and(r_items)); + + if (opt_AssertStrongerArrangements) { + expr_ref ax_strong(ctx.mk_eq_atom(ax_l, mk_and(r_items)), mgr); + assert_axiom(ax_strong); + } else { + assert_implication(ax_l, mk_and(r_items)); + } } else { // negate! It's impossible to split str with these lengths TRACE("t_str", tout << "CONFLICT: Impossible to split str with these lengths." << std::endl;); @@ -3522,7 +3561,13 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { ctx.mk_eq_atom(mk_strlen(y), mk_strlen(n))), mgr); 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); - assert_implication(ax_l, ax_r); + + if (opt_AssertStrongerArrangements) { + expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr); + assert_axiom(ax_strong); + } else { + assert_implication(ax_l, ax_r); + } } else if (splitType == 2) { // | x | y | @@ -3555,7 +3600,12 @@ 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); - assert_implication(ax_l, ax_r); + if (opt_AssertStrongerArrangements) { + expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr); + assert_axiom(ax_strong); + } else { + assert_implication(ax_l, ax_r); + } } else { loopDetected = true; TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;); @@ -3633,7 +3683,14 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { and_item.push_back(mk_or(or_item)); } expr_ref implyR(mk_and(and_item), mgr); - assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR); + + if (opt_AssertStrongerArrangements) { + 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); + } else { + assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR); + } } else { TRACE("t_str", tout << "STOP: should not split two eq. concats" << std::endl;); } @@ -3708,13 +3765,24 @@ 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); - assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR); + if (opt_AssertStrongerArrangements) { + expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr); + assert_axiom(ax_strong); + } else { + assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR); + } } } else if (str1Len == str2Len) { if (!in_same_eqc(n, y)) { //break down option 4-2 expr_ref implyR(ctx.mk_eq_atom(n, y), mgr); - assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR); + + if (opt_AssertStrongerArrangements) { + expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr); + assert_axiom(ax_strong); + } else { + assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR); + } } } else { std::string deltaStr = str2Value.substr(str1Len, str2Len - str1Len); @@ -3722,7 +3790,12 @@ 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); - assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR); + if (opt_AssertStrongerArrangements) { + expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr); + assert_axiom(ax_strong); + } else { + assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR); + } } } } @@ -3794,20 +3867,35 @@ void theory_str::process_concat_eq_type5(expr * concatAst1, expr * concatAst2) { expr_ref x_deltaStr(mk_concat(x, m_strutil.mk_string(deltaStr)), mgr); if (!in_same_eqc(m, x_deltaStr)) { expr_ref implyR(ctx.mk_eq_atom(m, x_deltaStr), mgr); - assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR); + if (opt_AssertStrongerArrangements) { + expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr); + assert_axiom(ax_strong); + } else { + assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR); + } } } else if (str1Len == str2Len) { // test if (!in_same_eqc(x, m)) { expr_ref implyR(ctx.mk_eq_atom(x, m), mgr); - assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR); + if (opt_AssertStrongerArrangements) { + expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr); + assert_axiom(ax_strong); + } else { + assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR); + } } } else { std::string deltaStr = str2Value.substr(0, str2Len - str1Len); expr_ref m_deltaStr(mk_concat(m, m_strutil.mk_string(deltaStr)), mgr); if (!in_same_eqc(x, m_deltaStr)) { expr_ref implyR(ctx.mk_eq_atom(x, m_deltaStr), mgr); - assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR); + if (opt_AssertStrongerArrangements) { + expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr); + assert_axiom(ax_strong); + } else { + assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR); + } } } } @@ -4020,7 +4108,13 @@ void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) { // case 6: concat("str1", y) = concat(m, "str2") and_item.push_back(mk_or(or_item)); expr_ref implyR(mk_and(and_item), mgr); - assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR); + + if (opt_AssertStrongerArrangements) { + expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr); + assert_axiom(ax_strong); + } else { + assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR); + } } void theory_str::process_unroll_eq_const_str(expr * unrollFunc, expr * constStr) { diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 5b8f644eb..8168d0632 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -189,6 +189,15 @@ namespace smt { */ bool opt_UseFastValueTesterCache; + /* + * If AssertStrongerArrangements is set to true, + * the implications that would normally be asserted during arrangement generation + * will instead be asserted as equivalences. + * This is a stronger version of the regular axiom. + * The default (Z3str2) behaviour is to set this to false. + */ + bool opt_AssertStrongerArrangements; + bool search_started; arith_util m_autil; str_util m_strutil;