remove automata references

Signed-off-by: Nikolaj Bjorner <[email protected]>

src/smt/params/smt_params_helper.pyg

@@ -97,7 +97,6 @@ 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.use_derivatives', BOOL, False, 'dev flag (not for users) enable derivative based unfolding of regex'),
 	                  ('seq.use_unicode', BOOL, False, 'dev flag (not for users) enable unicode semantics'),
                           ('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'),

src/smt/params/theory_seq_params.cpp

@@ -21,6 +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_use_derivatives = p.seq_use_derivatives();
     m_seq_use_unicode = p.seq_use_unicode();
 }

src/smt/params/theory_seq_params.h

@@ -24,14 +24,12 @@ struct theory_seq_params {
      */
     bool m_split_w_len;
     bool m_seq_validate;
-    bool m_seq_use_derivatives;
     bool m_seq_use_unicode;
 
 
     theory_seq_params(params_ref const & p = params_ref()):
         m_split_w_len(false),
         m_seq_validate(false),
-        m_seq_use_derivatives(false),
         m_seq_use_unicode(false)
     {
         updt_params(p);