summaryrefslogtreecommitdiff
path: root/src/api/cvc4cpp.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/api/cvc4cpp.h')
-rw-r--r--src/api/cvc4cpp.h5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index a701eb472..3481fd953 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -55,6 +55,7 @@ class CVC4_PUBLIC CVC4ApiException : public std::exception
CVC4ApiException(const std::string& str) : d_msg(str) {}
CVC4ApiException(const std::stringstream& stream) :d_msg(stream.str()) {}
std::string getMessage() const { return d_msg; }
+ const char* what() const noexcept override { return d_msg.c_str(); }
private:
std::string d_msg;
};
@@ -2427,6 +2428,10 @@ class CVC4_PUBLIC Solver
std::vector<Type> sortVectorToTypes(const std::vector<Sort>& vector) const;
/* Helper to convert a vector of sorts to internal types. */
std::vector<Expr> termVectorToExprs(const std::vector<Term>& vector) const;
+ /* Helper to check for API misuse in mkTerm functions. */
+ void checkMkOpTerm(OpTerm opTerm, uint32_t nchildren) const;
+ /* Helper to check for API misuse in mkOpTerm functions. */
+ void checkMkTerm(Kind kind, uint32_t nchildren) const;
/* The expression manager of this solver. */
std::unique_ptr<ExprManager> d_exprMgr;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback