mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

fix reset logic and load only logics admitted by context

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-11-07 15:44:21 +01:00
parent 23bc982ad2
commit ce7303b5e2
2 changed files with 27 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/cmd_context/cmd_context.cpp
View file

@ -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<family_id>& 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<family_id> 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<family_id>::iterator it = fids.begin();
svector<family_id>::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) {

1
src/cmd_context/cmd_context.h
View file

@ -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<family_id>& fids);
void init_manager_core(bool new_manager);
void init_manager();
void init_external_manager();