summaryrefslogtreecommitdiff
path: root/src/api
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2019-01-11 12:06:03 -0800
committerGitHub <noreply@github.com>2019-01-11 12:06:03 -0800
commit87f38648fe82b69b527a387bec9836455290cdba (patch)
treebea48537312148a144d159452cdea0ab2f019c13 /src/api
parent51cb061609e10ff68fb9db053d23ea9dd72ddea2 (diff)
New C++ API: Add unit tests for setInfo, setLogic, setOption. (#2782)
Diffstat (limited to 'src/api')
-rw-r--r--src/api/cvc4cpp.cpp76
-rw-r--r--src/api/cvc4cpp.h15
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback