From 64f1a759a7fc550587aec313eabb11e0f4391f62 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 29 Jun 2020 19:14:17 +0100 Subject: [PATCH] inline api_context::reset_error_code() --- src/api/api_context.cpp | 4 ---- src/api/api_context.h | 8 ++------ 2 files changed, 2 insertions(+), 10 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index bd0967ab2..e7d9b4ec2 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -147,10 +147,6 @@ namespace api { } } - void context::reset_error_code() { - m_error_code = Z3_OK; - } - void context::check_searching() { if (m_searching) { set_error_code(Z3_INVALID_USAGE, "cannot use function while searching"); // TBD: error code could be fixed. diff --git a/src/api/api_context.h b/src/api/api_context.h index 28fee34b3..da444165f 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -17,9 +17,7 @@ Author: Revision History: --*/ -#ifndef API_CONTEXT_H_ -#define API_CONTEXT_H_ - +#pragma once #include "util/hashtable.h" #include "util/mutex.h" @@ -170,7 +168,7 @@ namespace api { family_id get_special_relations_fid() const { return m_special_relations_fid; } Z3_error_code get_error_code() const { return m_error_code; } - void reset_error_code(); + void reset_error_code() { m_error_code = Z3_OK; } void set_error_code(Z3_error_code err, char const* opt_msg); void set_error_handler(Z3_error_handler h) { m_error_handler = h; } // Sign an error if solver is searching @@ -268,5 +266,3 @@ inline bool is_expr(Z3_ast a) { return is_expr(to_ast(a)); } inline bool is_bool_expr(Z3_context c, Z3_ast a) { return is_expr(a) && mk_c(c)->m().is_bool(to_expr(a)); } #define CHECK_FORMULA(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_) || !is_bool_expr(c, _a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return _ret_; } } inline void check_sorts(Z3_context c, ast * n) { mk_c(c)->check_sorts(n); } - -#endif