mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
move initialization to support more sort usage scenarios
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
adeae18471
commit
23bc982ad2
|
@ -623,17 +623,17 @@ void cmd_context::init_manager() {
|
|||
// no-op
|
||||
}
|
||||
else if (m_manager) {
|
||||
m_manager_initialized = true;
|
||||
SASSERT(!m_own_manager);
|
||||
init_external_manager();
|
||||
m_manager_initialized = true;
|
||||
}
|
||||
else {
|
||||
m_manager_initialized = true;
|
||||
SASSERT(m_pmanager == 0);
|
||||
m_check_sat_result = 0;
|
||||
m_manager = m_params.mk_ast_manager();
|
||||
m_pmanager = alloc(pdecl_manager, *m_manager);
|
||||
init_manager_core(true);
|
||||
m_manager_initialized = true;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -294,7 +294,7 @@ public:
|
|||
std::string reason_unknown() const;
|
||||
|
||||
bool has_manager() const { return m_manager != 0; }
|
||||
ast_manager & m() const { if (!m_manager) const_cast<cmd_context*>(this)->init_manager(); return *m_manager; }
|
||||
ast_manager & m() const { const_cast<cmd_context*>(this)->init_manager(); return *m_manager; }
|
||||
virtual ast_manager & get_ast_manager() { return m(); }
|
||||
pdecl_manager & pm() const { if (!m_pmanager) const_cast<cmd_context*>(this)->init_manager(); return *m_pmanager; }
|
||||
sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast<cmd_context*>(this)->m_sexpr_manager = alloc(sexpr_manager); return *m_sexpr_manager; }
|
||||
|
|
Loading…
Reference in a new issue