From c47ca341b7d05aec8d5260ee181c78c4c958bf13 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Sep 2022 10:17:00 -0700 Subject: [PATCH] fix #6343 The bug was that axiom generation was not enabled on last_index, so no axioms got created to constrain last-index. With default settings the solver is now very slow on this example. It is related to that the smallest size of a satisfying assignment is above 24. Pending a good heuristic to find initial seeds and increments for iterative deepening, I am adding another parameter smt.seq.min_unfolding that when set to 30 helps for this example. --- src/ast/rewriter/seq_axioms.cpp | 2 ++ src/smt/params/smt_params_helper.pyg | 1 + src/smt/params/theory_seq_params.cpp | 1 + src/smt/params/theory_seq_params.h | 1 + src/smt/theory_seq.cpp | 2 ++ 5 files changed, 7 insertions(+) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index de0030fc9..c7dde763f 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -509,6 +509,8 @@ namespace seq { } /** + i = last_indexof(t, s): + !contains(t, s) => i = -1 |t| = 0 => |s| = 0 or i = -1 |t| = 0 & |s| = 0 => i = 0 diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index f856689eb..8dfcf5d3b 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -107,6 +107,7 @@ def_module_params(module_name='smt', ('seq.split_w_len', BOOL, True, 'enable splitting guided by length constraints'), ('seq.validate', BOOL, False, 'enable self-validation of theory axioms created by seq theory'), ('seq.max_unfolding', UINT, 1000000000, 'maximal unfolding depth for checking string equations and regular expressions'), + ('seq.min_unfolding', UINT, 1, 'initial bound for strings whose lengths are bounded by iterative deepening. Set this to a higher value if there are only models with larger string lengths'), ('str.strong_arrangements', BOOL, True, 'assert equivalences instead of implications when generating string arrangement axioms'), ('str.aggressive_length_testing', BOOL, False, 'prioritize testing concrete length values over generating more options'), ('str.aggressive_value_testing', BOOL, False, 'prioritize testing concrete string constant values over generating more options'), diff --git a/src/smt/params/theory_seq_params.cpp b/src/smt/params/theory_seq_params.cpp index 196faf387..290b2631d 100644 --- a/src/smt/params/theory_seq_params.cpp +++ b/src/smt/params/theory_seq_params.cpp @@ -22,4 +22,5 @@ void theory_seq_params::updt_params(params_ref const & _p) { m_split_w_len = p.seq_split_w_len(); m_seq_validate = p.seq_validate(); m_seq_max_unfolding = p.seq_max_unfolding(); + m_seq_min_unfolding = p.seq_min_unfolding(); } diff --git a/src/smt/params/theory_seq_params.h b/src/smt/params/theory_seq_params.h index 845411039..f964088eb 100644 --- a/src/smt/params/theory_seq_params.h +++ b/src/smt/params/theory_seq_params.h @@ -25,6 +25,7 @@ struct theory_seq_params { bool m_split_w_len = false; bool m_seq_validate = false; unsigned m_seq_max_unfolding = UINT_MAX/4; + unsigned m_seq_min_unfolding = 1; theory_seq_params(params_ref const & p = params_ref()) { updt_params(p); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 040171d82..5712d1d41 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -304,6 +304,7 @@ void theory_seq::init() { m_ax.add_axiom5 = add_ax; m_ax.mk_eq_empty2 = mk_eq_emp; m_arith_value.init(&ctx); + m_max_unfolding_depth = ctx.get_fparams().m_seq_min_unfolding; } #define TRACEFIN(s) { TRACE("seq", tout << ">>" << s << "\n";); IF_VERBOSE(20, verbose_stream() << s << "\n"); } @@ -3256,6 +3257,7 @@ void theory_seq::relevant_eh(app* n) { m_util.str.is_from_code(n) || m_util.str.is_to_code(n) || m_util.str.is_unit(n) || + m_util.str.is_last_index(n) || m_util.str.is_length(n) || /* m_util.str.is_replace_all(n) || uncomment to enable axiomatization */ m_util.str.is_le(n)) {