fix #1599. fix #1600

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/api_context.cpp

@@ -78,7 +78,6 @@ namespace api {
         m_bv_util(m()),
         m_datalog_util(m()),
         m_fpa_util(m()),
-        m_dtutil(m()),
         m_sutil(m()),
         m_last_result(m()),
         m_ast_trail(m()),

src/api/api_context.h

@@ -61,7 +61,6 @@ namespace api {
         bv_util                    m_bv_util;
         datalog::dl_decl_util      m_datalog_util;
         fpa_util                   m_fpa_util;
-        datatype_util              m_dtutil;
         seq_util                   m_sutil;
 
         // Support for old solver API
@@ -122,12 +121,12 @@ namespace api {
         bool produce_unsat_cores() const { return m_params.m_unsat_core; }
         bool use_auto_config() const { return m_params.m_auto_config; }
         unsigned get_timeout() const { return m_params.m_timeout; }
-        unsigned get_rlimit() const { return m_params.m_rlimit; }
+        unsigned get_rlimit() const { return m_params.rlimit(); }
         arith_util & autil() { return m_arith_util; }
         bv_util & bvutil() { return m_bv_util; }
         datalog::dl_decl_util & datalog_util() { return m_datalog_util; }
         fpa_util & fpautil() { return m_fpa_util; }
-        datatype_util& dtutil() { return m_dtutil; }
+        datatype_util& dtutil() { return m_dt_plugin->u(); }
         seq_util& sutil() { return m_sutil; }
         family_id get_basic_fid() const { return m_basic_fid; }
         family_id get_array_fid() const { return m_array_fid; }

src/ast/datatype_decl_plugin.cpp

@@ -390,6 +390,8 @@ namespace datatype {
                 TRACE("datatype", tout << "declaring " << datatypes[i]->name() << "\n";);
                 if (m_defs.find(datatypes[i]->name(), d)) {
                     TRACE("datatype", tout << "delete previous version for " << datatypes[i]->name() << "\n";);
+                    sort_ref_vector srts(*m_manager);
+                    u().reset();
                     dealloc(d);
                 }
                 m_defs.insert(datatypes[i]->name(), datatypes[i]);

src/ast/datatype_decl_plugin.h

@@ -239,7 +239,6 @@ namespace datatype {
             map<symbol, def*, symbol_hash_proc, symbol_eq_proc> m_defs; 
             svector<symbol>          m_def_block;
             unsigned                 m_class_id;
-            util & u() const;
 
             void inherit(decl_plugin* other_p, ast_translation& tr) override;
 
@@ -279,6 +278,8 @@ namespace datatype {
             def const& get_def(sort* s) const { return *(m_defs[datatype_name(s)]); }
             def& get_def(symbol const& s) { return *(m_defs[s]); }
             bool is_declared(sort* s) const { return m_defs.contains(datatype_name(s)); }
+            util & u() const;
+
         private:
             bool is_value_visit(expr * arg, ptr_buffer<app> & todo) const;
         

src/cmd_context/basic_cmds.cpp

@@ -503,7 +503,7 @@ public:
             ctx.set_random_seed(to_unsigned(val));
         }
         else if (m_option == m_reproducible_resource_limit) {
-            ctx.params().m_rlimit = to_unsigned(val);
+            ctx.params().set_rlimit(to_unsigned(val));
         }
         else if (m_option == m_verbosity) {
             set_verbosity_level(to_unsigned(val));

src/cmd_context/cmd_context.cpp

@@ -1328,7 +1328,8 @@ void cmd_context::push() {
     s.m_macros_stack_lim       = m_macros_stack.size();
     s.m_aux_pdecls_lim         = m_aux_pdecls.size();
     s.m_assertions_lim         = m_assertions.size();
-    if (m_solver)
+    m().limit().push(m_params.rlimit());
+    if (m_solver) 
         m_solver->push();
     if (m_opt)
         m_opt->push();
@@ -1443,6 +1444,9 @@ void cmd_context::pop(unsigned n) {
     restore_assertions(s.m_assertions_lim);
     restore_psort_inst(s.m_psort_inst_stack_lim);
     m_scopes.shrink(new_lvl);
+    while (n--) {
+        m().limit().pop();
+    }
 
 }
 
@@ -1453,7 +1457,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
     TRACE("before_check_sat", dump_assertions(tout););
     init_manager();
     unsigned timeout = m_params.m_timeout;
-    unsigned rlimit  = m_params.m_rlimit;
+    unsigned rlimit  = m_params.rlimit();
     scoped_watch sw(*this);
     lbool r;
     bool was_opt = false;
@@ -1530,7 +1534,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
 
 void cmd_context::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector & conseq) {
     unsigned timeout = m_params.m_timeout;
-    unsigned rlimit  = m_params.m_rlimit;
+    unsigned rlimit  = m_params.rlimit();
     lbool r;
     m_check_sat_result = m_solver.get(); // solver itself stores the result.
     m_solver->set_progress_callback(this);

src/cmd_context/context_params.h

@@ -27,6 +27,8 @@ class context_params {
     void set_bool(bool & opt, char const * param, char const * value);
     void set_uint(unsigned & opt, char const * param, char const * value);
 
+    unsigned    m_rlimit;
+
 public:
     bool        m_auto_config;
     bool        m_proof;
@@ -42,10 +44,11 @@ public:
     bool        m_unsat_core;
     bool        m_smtlib2_compliant; // it must be here because it enable/disable the use of coercions in the ast_manager.
     unsigned    m_timeout;
-    unsigned    m_rlimit;
 
+    unsigned rlimit() const { return m_rlimit; }
     context_params();
     void set(char const * param, char const * value);
+    void set_rlimit(unsigned lim) { m_rlimit = lim; }
     void updt_params();
     void updt_params(params_ref const & p);
     static void collect_param_descrs(param_descrs & d);

src/cmd_context/tactic_cmds.cpp

@@ -205,7 +205,7 @@ public:
         tref->set_logic(ctx.get_logic());
         ast_manager & m = ctx.m();
         unsigned timeout   = p.get_uint("timeout", ctx.params().m_timeout);
-        unsigned rlimit  =   p.get_uint("rlimit", ctx.params().m_rlimit);
+        unsigned rlimit  =   p.get_uint("rlimit", ctx.params().rlimit());
         labels_vec labels;
         goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores());
         assert_exprs_from(ctx, *g);
@@ -321,7 +321,7 @@ public:
             assert_exprs_from(ctx, *g);
 
             unsigned timeout   = p.get_uint("timeout", ctx.params().m_timeout);
-            unsigned rlimit  =   p.get_uint("rlimit", ctx.params().m_rlimit);
+            unsigned rlimit  =   p.get_uint("rlimit", ctx.params().rlimit());
 
             goal_ref_buffer     result_goals;
             model_converter_ref mc;

src/opt/opt_context.h

@@ -283,13 +283,13 @@ namespace opt {
         struct is_propositional_fn;
         bool is_propositional(expr* e);
 
-        void    init_solver();
+        void init_solver();
-        void    update_solver();
+        void update_solver();
-        void    setup_arith_solver();
+        void setup_arith_solver();
-        void    add_maxsmt(symbol const& id, unsigned index);
+        void add_maxsmt(symbol const& id, unsigned index);
-        void    set_simplify(tactic *simplify);
+        void set_simplify(tactic *simplify);
-        void    set_pareto(pareto_base* p);        
+        void set_pareto(pareto_base* p);        
-        void    clear_state();
+        void clear_state();
 
         bool is_numeral(expr* e, rational& n) const;