From cd937c07f325999fb03cf5e68448c9ce031ea0fe Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 15 May 2016 13:29:38 -0700
Subject: [PATCH] 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
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/api/api_model.cpp | 3 +--
src/api/c++/z3++.h | 3 +++
src/api/python/z3.py | 5 ++++-
3 files changed, 8 insertions(+), 3 deletions(-)
diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index 63092b2cf..10ede0922 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -50,14 +50,13 @@ extern "C" {
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;
LOG_Z3_model_get_const_interp(c, m, a);
RESET_ERROR_CODE();
CHECK_NON_NULL(m, 0);
expr * r = to_model_ref(m)->get_const_interp(to_func_decl(a));
if (!r) {
- SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0);
}
mk_c(c)->save_ast_trail(r);
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 6e8544770..9fb664819 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -1582,6 +1582,9 @@ namespace z3 {
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 {
check_context(*this, c);
Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 848883ba3..2126cf0fe 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -5516,7 +5516,10 @@ class ModelRef(Z3PPObject):
decl = decl.decl()
try:
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):
return self.get_interp(get_as_array_func(r))
else: