mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

return proper ast-option from get_const_interp function insetad of raising exceptions from inside the C API. Fixes discrepancy with documentation and behavior across extensions of the API. Issue #587

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-05-15 13:29:38 -07:00
parent e5ca676251
commit cd937c07f3
3 changed files with 8 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/api/api_model.cpp
View file

@ -50,14 +50,13 @@ extern "C" {
Z3_CATCH; Z3_CATCH;
} }
Z3_ast Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a) { Z3_ast_opt Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a) {
Z3_TRY; Z3_TRY;
LOG_Z3_model_get_const_interp(c, m, a); LOG_Z3_model_get_const_interp(c, m, a);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
CHECK_NON_NULL(m, 0); CHECK_NON_NULL(m, 0);
expr * r = to_model_ref(m)->get_const_interp(to_func_decl(a)); expr * r = to_model_ref(m)->get_const_interp(to_func_decl(a));
if (!r) { if (!r) {
SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); RETURN_Z3(0);
} }
mk_c(c)->save_ast_trail(r); mk_c(c)->save_ast_trail(r);

3
src/api/c++/z3++.h
View file

@ -1582,6 +1582,9 @@ namespace z3 {
return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts()); return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
} }
// returns interpretation of constant declaration c.
// If c is not assigned any value in the model it returns
// an expression with a null ast reference.
expr get_const_interp(func_decl c) const { expr get_const_interp(func_decl c) const {
check_context(*this, c); check_context(*this, c);
Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c); Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);

5
src/api/python/z3.py
View file

@ -5516,7 +5516,10 @@ class ModelRef(Z3PPObject):
decl = decl.decl() decl = decl.decl()
try: try:
if decl.arity() == 0: if decl.arity() == 0:
r = _to_expr_ref(Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast), self.ctx) _r = Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast)
if _r.value is None:
return None
r = _to_expr_ref(_r, self.ctx)
if is_as_array(r): if is_as_array(r):
return self.get_interp(get_as_array_func(r)) return self.get_interp(get_as_array_func(r))
else: else: