max maximal unfolding configurable

Z3Prover · Aug 4, 2022 · a8ff976 · a8ff976
1 parent a3161bd
commit a8ff976
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 2 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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");
     }