diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-01-11 12:06:03 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-01-11 12:06:03 -0800 |
| commit | 87f38648fe82b69b527a387bec9836455290cdba (patch) | |
| tree | bea48537312148a144d159452cdea0ab2f019c13 /src/api/cvc4cpp.h | |
| parent | 51cb061609e10ff68fb9db053d23ea9dd72ddea2 (diff) | |
New C++ API: Add unit tests for setInfo, setLogic, setOption. (#2782)
Diffstat (limited to 'src/api/cvc4cpp.h')
| -rw-r--r-- | src/api/cvc4cpp.h | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 1d98f127d..a06f2e415 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -24,8 +24,8 @@ #include <map> #include <memory> #include <set> -#include <string> #include <sstream> +#include <string> #include <unordered_map> #include <unordered_set> #include <vector> @@ -53,9 +53,10 @@ class CVC4_PUBLIC CVC4ApiException : public std::exception { public: CVC4ApiException(const std::string& str) : d_msg(str) {} - CVC4ApiException(const std::stringstream& stream) :d_msg(stream.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; }; @@ -2237,9 +2238,8 @@ class CVC4_PUBLIC Solver * @param ctors the constructor declarations of the datatype sort * @return the datatype sort */ - Sort declareDatatype( - const std::string& symbol, - const std::vector<DatatypeConstructorDecl>& ctors) const; + Sort declareDatatype(const std::string& symbol, + const std::vector<DatatypeConstructorDecl>& ctors) const; /** * Declare 0-arity function symbol. @@ -2489,7 +2489,8 @@ class CVC4_PUBLIC Solver /* Helper to check for API misuse in mkOpTerm functions. */ void checkMkTerm(Kind kind, uint32_t nchildren) const; /* Helper for mk-functions that call d_exprMgr->mkConst(). */ - template <typename T> Term mkConstHelper(T t) const; + template <typename T> + Term mkConstHelper(T t) const; /* Helper for mkReal functions that take a string as argument. */ Term mkRealFromStrHelper(std::string s) const; /* Helper for mkBitVector functions that take a string as argument. */ @@ -2499,6 +2500,8 @@ class CVC4_PUBLIC Solver Term mkBVFromStrHelper(uint32_t size, std::string s, uint32_t base) const; /* Helper for mkBitVector functions that take an integer as argument. */ Term mkBVFromIntHelper(uint32_t size, uint64_t val) const; + /* Helper for setLogic. */ + void setLogicHelper(const std::string& logic) const; /** * Helper function that ensures that a given term is of sort real (as opposed |