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 | |
parent | 51cb061609e10ff68fb9db053d23ea9dd72ddea2 (diff) |
New C++ API: Add unit tests for setInfo, setLogic, setOption. (#2782)
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cvc4cpp.cpp | 76 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 15 |
2 files changed, 73 insertions, 18 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 5321a90ec..123613797 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -29,6 +29,7 @@ #include "options/options.h" #include "smt/model.h" #include "smt/smt_engine.h" +#include "theory/logic_info.h" #include "util/random.h" #include "util/result.h" #include "util/utility.h" @@ -3374,26 +3375,70 @@ void Solver::reset(void) const { d_smtEngine->reset(); } */ void Solver::resetAssertions(void) const { d_smtEngine->resetAssertions(); } +// TODO: issue #2781 +void Solver::setLogicHelper(const std::string& logic) const +{ + CVC4_API_CHECK(!d_smtEngine->isFullyInited()) + << "Invalid call to 'setLogic', solver is already fully initialized"; + try + { + CVC4::LogicInfo logic_info(logic); + d_smtEngine->setLogic(logic_info); + } + catch (CVC4::IllegalArgumentException& e) + { + throw CVC4ApiException(e.getMessage()); + } +} + /** * ( set-info <attribute> ) */ void Solver::setInfo(const std::string& keyword, const std::string& value) const { - // CHECK: - // if keyword == "cvc4-logic": value must be string - // if keyword == "status": must be sat, unsat or unknown - // if keyword == "smt-lib-version": supported? + bool is_cvc4_keyword = false; + + /* Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_") */ + if (keyword.length() > 5) + { + std::string prefix = keyword.substr(0, 5); + if (prefix == "cvc4-" || prefix == "cvc4_") + { + is_cvc4_keyword = true; + std::string cvc4key = keyword.substr(5); + CVC4_API_ARG_CHECK_EXPECTED(cvc4key == "logic", keyword) + << "keyword 'cvc4-logic'"; + setLogicHelper(value); + } + } + if (!is_cvc4_keyword) + { + CVC4_API_ARG_CHECK_EXPECTED( + keyword == "source" || keyword == "category" || keyword == "difficulty" + || keyword == "filename" || keyword == "license" + || keyword == "name" || keyword == "notes" + || keyword == "smt-lib-version" || keyword == "status", + keyword) + << "'source', 'category', 'difficulty', 'filename', 'license', 'name', " + "'notes', 'smt-lib-version' or 'status'"; + CVC4_API_ARG_CHECK_EXPECTED(keyword != "smt-lib-version" || value == "2" + || value == "2.0" || value == "2.5" + || value == "2.6" || value == "2.6.1", + value) + << "'2.0', '2.5', '2.6' or '2.6.1'"; + CVC4_API_ARG_CHECK_EXPECTED(keyword != "status" || value == "sat" + || value == "unsat" || value == "unknown", + value) + << "'sat', 'unsat' or 'unknown'"; + } + d_smtEngine->setInfo(keyword, value); } /** * ( set-logic <symbol> ) */ -void Solver::setLogic(const std::string& logic) const -{ - // CHECK: !d_smtEngine->d_fullyInited - d_smtEngine->setLogic(logic); -} +void Solver::setLogic(const std::string& logic) const { setLogicHelper(logic); } /** * ( set-option <option> ) @@ -3401,9 +3446,16 @@ void Solver::setLogic(const std::string& logic) const void Solver::setOption(const std::string& option, const std::string& value) const { - // CHECK: option exists? - // CHECK: !d_smtEngine->d_fullInited, else option can't be set - d_smtEngine->setOption(option, value); + CVC4_API_CHECK(!d_smtEngine->isFullyInited()) + << "Invalid call to 'setOption', solver is already fully initialized"; + try + { + d_smtEngine->setOption(option, value); + } + catch (CVC4::OptionException& e) + { + throw CVC4ApiException(e.getMessage()); + } } Term Solver::ensureTermSort(const Term& t, const Sort& s) const 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 |