From ce7303b5e2713be2909a39d862c0fe2bba8659c5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 7 Nov 2014 15:44:21 +0100 Subject: [PATCH] fix reset logic and load only logics admitted by context Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 30 ++++++++++++++++++++++++++---- src/cmd_context/cmd_context.h | 1 + 2 files changed, 27 insertions(+), 4 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 5d24977b5..ee5437bd6 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -470,6 +470,16 @@ void cmd_context::register_plugin(symbol const & name, decl_plugin * p, bool ins } } +void cmd_context::load_plugin(symbol const & name, bool install, svector& fids) { + family_id id = m_manager->get_family_id(name); + decl_plugin* p = m_manager->get_plugin(id); + if (install && p && fids.contains(id)) { + register_builtin_sorts(p); + register_builtin_ops(p); + } + fids.erase(id); +} + bool cmd_context::logic_has_arith_core(symbol const & s) const { return s == "QF_LRA" || @@ -586,17 +596,26 @@ void cmd_context::init_manager_core(bool new_manager) { register_builtin_sorts(basic); register_builtin_ops(basic); // the manager was created by the command context. - register_plugin(symbol("arith"), alloc(arith_decl_plugin), logic_has_arith()); - register_plugin(symbol("bv"), alloc(bv_decl_plugin), logic_has_bv()); - register_plugin(symbol("array"), alloc(array_decl_plugin), logic_has_array()); + register_plugin(symbol("arith"), alloc(arith_decl_plugin), logic_has_arith()); + register_plugin(symbol("bv"), alloc(bv_decl_plugin), logic_has_bv()); + register_plugin(symbol("array"), alloc(array_decl_plugin), logic_has_array()); register_plugin(symbol("datatype"), alloc(datatype_decl_plugin), logic_has_datatype()); register_plugin(symbol("seq"), alloc(seq_decl_plugin), logic_has_seq()); register_plugin(symbol("float"), alloc(float_decl_plugin), logic_has_floats()); } else { - // the manager was created by an external module, we must register all plugins available in the manager. + // the manager was created by an external module + // we register all plugins available in the manager. + // unless the logic specifies otherwise. svector fids; m_manager->get_range(fids); + load_plugin(symbol("arith"), logic_has_arith(), fids); + load_plugin(symbol("bv"), logic_has_bv(), fids); + load_plugin(symbol("array"), logic_has_array(), fids); + load_plugin(symbol("datatype"), logic_has_datatype(), fids); + load_plugin(symbol("seq"), logic_has_seq(), fids); + load_plugin(symbol("float"), logic_has_floats(), fids); + svector::iterator it = fids.begin(); svector::iterator end = fids.end(); for (; it != end; ++it) { @@ -1174,12 +1193,15 @@ void cmd_context::reset(bool finalize) { if (m_own_manager) { dealloc(m_manager); m_manager = 0; + m_manager_initialized = false; } else { // doesn't own manager... so it cannot be deleted // reinit cmd_context if this is not a finalization step if (!finalize) init_external_manager(); + else + m_manager_initialized = false; } } if (m_sexpr_manager) { diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index c4aa34c61..1c8dba21a 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -214,6 +214,7 @@ protected: void register_builtin_sorts(decl_plugin * p); void register_builtin_ops(decl_plugin * p); void register_plugin(symbol const & name, decl_plugin * p, bool install_names); + void load_plugin(symbol const & name, bool install_names, svector& fids); void init_manager_core(bool new_manager); void init_manager(); void init_external_manager();