mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

delay initializing internal manager so that parser does not choke on proper SMT-LIB logics. Reported by Venkateshan

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-11-06 13:09:25 +01:00
parent 591f6d096f
commit adeae18471
3 changed files with 29 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/api/z3_api.h
View file

@ -3988,6 +3988,12 @@ END_MLAPI_EXCLUDE
/**
\brief Return a unique identifier for \c t.
The identifier is unique up to structural equality. Thus, two ast nodes
created by the same context and having the same children and same function symbols
have the same identifiers. Ast nodes created in the same context, but having
different children or different functions have different identifiers.
Variables and quantifiers are also assigned different identifiers according to
their structure.
\mlonly \remark Implicitly used by [Pervasives.compare] for values of type [ast], [app], [sort], [func_decl], and [pattern]. \endmlonly
def_API('Z3_get_ast_id', UINT, (_in(CONTEXT), _in(AST)))
@ -3996,6 +4002,8 @@ END_MLAPI_EXCLUDE
/**
\brief Return a hash code for the given AST.
The hash code is structural. You can use Z3_get_ast_id interchangably with
this function.
\mlonly \remark Implicitly used by [Hashtbl.hash] for values of type [ast], [app], [sort], [func_decl], and [pattern]. \endmlonly
def_API('Z3_get_ast_hash', UINT, (_in(CONTEXT), _in(AST)))

33
src/cmd_context/cmd_context.cpp
View file

@ -314,8 +314,9 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
m_numeral_as_real(false),
m_ignore_check(false),
m_exit_on_error(false),
m_manager(m),
m_manager(m),
m_own_manager(m == 0),
m_manager_initialized(false),
m_pmanager(0),
m_sexpr_manager(0),
m_regular("stdout", std::cout),
@ -326,8 +327,6 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
install_core_tactic_cmds(*this);
install_interpolant_cmds(*this);
SASSERT(m != 0 || !has_manager());
if (m)
init_external_manager();
if (m_main_ctx) {
set_verbose_stream(diagnostic_stream());
}
@ -620,12 +619,22 @@ void cmd_context::init_manager_core(bool new_manager) {
}
void cmd_context::init_manager() {
SASSERT(m_manager == 0);
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);
if (m_manager_initialized) {
// no-op
}
else if (m_manager) {
SASSERT(!m_own_manager);
init_external_manager();
m_manager_initialized = true;
}
else {
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;
}
}
void cmd_context::init_external_manager() {
@ -1211,8 +1220,7 @@ void cmd_context::assert_expr(symbol const & name, expr * t) {
void cmd_context::push() {
m_check_sat_result = 0;
if (!has_manager())
init_manager();
init_manager();
m_scopes.push_back(scope());
scope & s = m_scopes.back();
s.m_func_decls_stack_lim = m_func_decls_stack.size();
@ -1332,8 +1340,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
return;
IF_VERBOSE(100, verbose_stream() << "(started \"check-sat\")" << std::endl;);
TRACE("before_check_sat", dump_assertions(tout););
if (!has_manager())
init_manager();
init_manager();
if (m_solver) {
m_check_sat_result = m_solver.get(); // solver itself stores the result.
m_solver->set_progress_callback(this);

1
src/cmd_context/cmd_context.h
View file

@ -149,6 +149,7 @@ protected:
ast_manager * m_manager;
bool m_own_manager;
bool m_manager_initialized;
pdecl_manager * m_pmanager;
sexpr_manager * m_sexpr_manager;
check_logic m_check_logic;