From 758266b952c379015daf56518f6cbbb054f0d968 Mon Sep 17 00:00:00 2001 From: cttghc Date: Tue, 6 Sep 2016 18:32:41 -0500 Subject: [PATCH] Fix omission of Z3_model_has_interp in z3++.h --- src/api/c++/z3++.h | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index a9a4efd03..b4643aa2b 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1615,6 +1615,13 @@ namespace z3 { check_error(); return func_interp(ctx(), r); } + + // returns true iff the model contains an interpretation + // for function f. + bool has_interp(func_decl f) const { + check_context(*this, f); + return Z3_model_has_interp(ctx(), m_model, f); + } friend std::ostream & operator<<(std::ostream & out, model const & m); };