From c917c1c53db30b875a645ba19879a61512d89b17 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 12 Sep 2014 15:54:42 -0700 Subject: [PATCH 1/5] reset ast trail on context deletion Signed-off-by: Nikolaj Bjorner --- src/api/api_context.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 05e1ca675..338c12f61 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -128,6 +128,7 @@ namespace api { for (unsigned i = 0; i < m_replay_stack.size(); ++i) { dealloc(m_replay_stack[i]); } + m_ast_trail.reset(); } reset_parser(); dealloc(m_solver); From 67b802c9d905329d2411615131b426789cb3856d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 12 Sep 2014 17:38:34 -0700 Subject: [PATCH 2/5] fix scope accounting bug and documentation per Konrad's request Signed-off-by: Nikolaj Bjorner --- src/api/api_context.cpp | 1 + src/api/api_solver_old.cpp | 2 +- src/api/z3_api.h | 7 ++++++- 3 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 338c12f61..3349bed7c 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -361,6 +361,7 @@ namespace api { } } } + SASSERT(num_scopes <= get_smt_kernel().get_scope_level()); get_smt_kernel().pop(num_scopes); } diff --git a/src/api/api_solver_old.cpp b/src/api/api_solver_old.cpp index e0533fbd9..b81fb2f2c 100644 --- a/src/api/api_solver_old.cpp +++ b/src/api/api_solver_old.cpp @@ -40,7 +40,7 @@ extern "C" { LOG_Z3_pop(c, num_scopes); RESET_ERROR_CODE(); CHECK_SEARCHING(c); - if (num_scopes > mk_c(c)->get_smt_kernel().get_scope_level()) { + if (num_scopes > mk_c(c)->get_num_scopes()) { SET_ERROR_CODE(Z3_IOB); return; } diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 4ffdfa9c2..e1c42667a 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -7069,7 +7069,7 @@ END_MLAPI_EXCLUDE \mlonly then a valid model is returned. Otherwise, it is unsafe to use the returned model.\endmlonly \conly The caller is responsible for deleting the model using the function #Z3_del_model. - \conly \remark In constrast with the rest of the Z3 API, the reference counter of the + \conly \remark In contrast with the rest of the Z3 API, the reference counter of the \conly model is incremented. This is to guarantee backward compatibility. In previous \conly versions, models did not support reference counting. @@ -7182,6 +7182,11 @@ END_MLAPI_EXCLUDE \brief Delete a model object. \sa Z3_check_and_get_model + + \conly \remark The Z3_check_and_get_model automatically increments a reference count on the model. + \conly The expected usage is that models created by that method are deleted using Z3_del_model. + \conly This is for backwards compatibility and in contrast to the rest of the API where + \conly callers are responsible for managing reference counts. \deprecated Subsumed by Z3_solver API From 919e0a5ea2f2bef4fe8ab9880e91dd52a7fc2bd1 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 16 Sep 2014 14:56:59 +0100 Subject: [PATCH 3/5] Z3Py: fix bug in substitute() with a list of on variable e.g. print substitute(Int('x'), [(Int('x'), Int('y'))]) Signed-off-by: Nuno Lopes --- src/api/python/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 50d29a790..d46d40ab2 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -6960,7 +6960,7 @@ def substitute(t, *m): if isinstance(m, tuple): m1 = _get_args(m) if isinstance(m1, list): - m = _get_args(m1) + m = m1 if __debug__: _z3_assert(is_expr(t), "Z3 expression expected") _z3_assert(all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(p[1].sort()) for p in m]), "Z3 invalid substitution, expression pairs expected.") From f7c3559c31b5d5c7335706a61a7f9c6e47a55545 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 16 Sep 2014 15:26:01 +0100 Subject: [PATCH 4/5] fix a few compiler warnings Signed-off-by: Nuno Lopes --- src/api/api_interp.cpp | 2 +- src/muz/pdr/pdr_farkas_learner.cpp | 1 - src/smt/smt_model_checker.cpp | 3 +-- 3 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 03d5ff843..e06ad5192 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -411,7 +411,7 @@ static void get_file_params(const char *filename, hash_map= 0 && eqpos < tok.size()){ + if(eqpos != std::string::npos){ std::string left = tok.substr(0,eqpos); std::string right = tok.substr(eqpos+1,tok.size()-eqpos-1); params[left] = right; diff --git a/src/muz/pdr/pdr_farkas_learner.cpp b/src/muz/pdr/pdr_farkas_learner.cpp index 7c38bf86f..b440ef519 100644 --- a/src/muz/pdr/pdr_farkas_learner.cpp +++ b/src/muz/pdr/pdr_farkas_learner.cpp @@ -905,7 +905,6 @@ namespace pdr { void farkas_learner::get_asserted(proof* p, expr_set const& bs, ast_mark& b_closed, obj_hashtable& lemma_set, expr_ref_vector& lemmas) { ast_manager& m = lemmas.get_manager(); ast_mark visited; - proof* p0 = p; ptr_vector todo; todo.push_back(p); diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 526447f9f..7053d63ec 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -136,9 +136,8 @@ namespace smt { if (cex == 0) return false; // no model available. unsigned num_decls = q->get_num_decls(); - unsigned num_sks = sks.size(); // Remark: sks were created for the flat version of q. - SASSERT(num_sks >= num_decls); + SASSERT(sks.size() >= num_decls); expr_ref_buffer bindings(m_manager); bindings.resize(num_decls); unsigned max_generation = 0; From 79326e24dfb9dff723d1ce64b3f50bcf394bd48c Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 16 Sep 2014 15:29:25 +0100 Subject: [PATCH 5/5] fix debug build.. Signed-off-by: Nuno Lopes --- src/muz/pdr/pdr_farkas_learner.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/muz/pdr/pdr_farkas_learner.cpp b/src/muz/pdr/pdr_farkas_learner.cpp index b440ef519..7c38bf86f 100644 --- a/src/muz/pdr/pdr_farkas_learner.cpp +++ b/src/muz/pdr/pdr_farkas_learner.cpp @@ -905,6 +905,7 @@ namespace pdr { void farkas_learner::get_asserted(proof* p, expr_set const& bs, ast_mark& b_closed, obj_hashtable& lemma_set, expr_ref_vector& lemmas) { ast_manager& m = lemmas.get_manager(); ast_mark visited; + proof* p0 = p; ptr_vector todo; todo.push_back(p);