From a8ff976bcc20e8a78f07c836599ac0a580fa2d1a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 4 Aug 2022 16:58:01 +0300 Subject: [PATCH] max maximal unfolding configurable --- 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 | 4 ++-- 4 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 2cf29ffa8..3b32d7602 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -105,6 +105,7 @@ def_module_params(module_name='smt', ('core.validate', BOOL, False, '[internal] validate unsat core produced by SMT context. This option is intended for debugging'), ('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'), ('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 68cce6e66..196faf387 100644 --- a/src/smt/params/theory_seq_params.cpp +++ b/src/smt/params/theory_seq_params.cpp @@ -21,4 +21,5 @@ void theory_seq_params::updt_params(params_ref const & _p) { smt_params_helper p(_p); m_split_w_len = p.seq_split_w_len(); m_seq_validate = p.seq_validate(); + m_seq_max_unfolding = p.seq_max_unfolding(); } diff --git a/src/smt/params/theory_seq_params.h b/src/smt/params/theory_seq_params.h index 84437fa15..845411039 100644 --- a/src/smt/params/theory_seq_params.h +++ b/src/smt/params/theory_seq_params.h @@ -24,6 +24,7 @@ struct theory_seq_params { */ bool m_split_w_len = false; bool m_seq_validate = false; + unsigned m_seq_max_unfolding = UINT_MAX/4; 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 9a05ccfbf..bb509e549 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3276,7 +3276,7 @@ bool theory_seq::should_research(expr_ref_vector & unsat_core) { } } - if (k_min < UINT_MAX/4) { + if (k_min < get_fparams().m_seq_max_unfolding) { m_max_unfolding_depth++; k_min *= 2; if (m_util.is_seq(s_min)) @@ -3290,7 +3290,7 @@ bool theory_seq::should_research(expr_ref_vector & unsat_core) { IF_VERBOSE(1, verbose_stream() << "(smt.seq :increase-depth " << m_max_unfolding_depth << ")\n"); return true; } - else if (k_min != UINT_MAX && k_min >= UINT_MAX/4) { + else if (k_min != UINT_MAX && k_min >= get_fparams().m_seq_max_unfolding) { throw default_exception("reached max unfolding"); }