diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index c8b365f22..5993e9fdd 100644 --- a/src/api/api_context.cpp +++ b/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()), diff --git a/src/api/api_context.h b/src/api/api_context.h index 185eb9e0f..72a0e4bbb 100644 --- a/src/api/api_context.h +++ b/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; } diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index f685c70d5..dfeaef9f8 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/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]); diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index f32e9990d..88b50af82 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -239,7 +239,6 @@ namespace datatype { map m_defs; svector 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 & todo) const; diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 0c9c5360c..4e8806d62 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/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)); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 11f800b25..9f93e1b93 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/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); diff --git a/src/cmd_context/context_params.h b/src/cmd_context/context_params.h index df62057fe..3d2947b7a 100644 --- a/src/cmd_context/context_params.h +++ b/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); diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index 32a92ea59..78187ebe1 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/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; diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 6af106ef3..e97fabbe4 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -283,13 +283,13 @@ namespace opt { struct is_propositional_fn; bool is_propositional(expr* e); - void init_solver(); - void update_solver(); - void setup_arith_solver(); - void add_maxsmt(symbol const& id, unsigned index); - void set_simplify(tactic *simplify); - void set_pareto(pareto_base* p); - void clear_state(); + void init_solver(); + void update_solver(); + void setup_arith_solver(); + void add_maxsmt(symbol const& id, unsigned index); + void set_simplify(tactic *simplify); + void set_pareto(pareto_base* p); + void clear_state(); bool is_numeral(expr* e, rational& n) const;