diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cvc4cpp.cpp | 35 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 22 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 14 |
3 files changed, 61 insertions, 10 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index fff4bef85..2e6e70d6b 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -2294,7 +2294,7 @@ Term Solver::mkValHelper(T t) const return res; } -Term Solver::mkRealFromStrHelper(std::string s) const +Term Solver::mkRealFromStrHelper(const std::string& s) const { /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP * throws an std::invalid_argument exception. For consistency, we treat it @@ -2318,7 +2318,7 @@ Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkBVFromStrHelper(std::string s, uint32_t base) const +Term Solver::mkBVFromStrHelper(const std::string& s, uint32_t base) const { CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string"; CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s) @@ -2328,7 +2328,7 @@ Term Solver::mkBVFromStrHelper(std::string s, uint32_t base) const } Term Solver::mkBVFromStrHelper(uint32_t size, - std::string s, + const std::string& s, uint32_t base) const { CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string"; @@ -2353,6 +2353,20 @@ Term Solver::mkBVFromStrHelper(uint32_t size, return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val)); } +Term Solver::mkCharFromStrHelper(const std::string& s) const +{ + CVC4_API_CHECK(s.find_first_not_of("0123456789abcdefABCDEF", 0) + == std::string::npos + && s.size() <= 5 && s.size() > 0) + << "Unexpected string for hexidecimal character " << s; + uint32_t val = static_cast<uint32_t>(std::stoul(s, 0, 16)); + CVC4_API_CHECK(val < String::num_codes()) + << "Not a valid code point for hexidecimal character " << s; + std::vector<unsigned> cpts; + cpts.push_back(val); + return mkValHelper<CVC4::String>(CVC4::String(cpts)); +} + Term Solver::mkTermFromKind(Kind kind) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -2951,6 +2965,21 @@ Term Solver::mkString(const std::vector<unsigned>& s) const CVC4_API_SOLVER_TRY_CATCH_END; } +Term Solver::mkChar(const std::string& s) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + return mkCharFromStrHelper(s); + CVC4_API_SOLVER_TRY_CATCH_END; +} + +Term Solver::mkChar(const char* s) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_NOT_NULLPTR(s); + return mkCharFromStrHelper(std::string(s)); + CVC4_API_SOLVER_TRY_CATCH_END; +} + Term Solver::mkUniverseSet(Sort sort) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 1a1cd3b61..edff95a2f 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2303,6 +2303,20 @@ class CVC4_PUBLIC Solver Term mkString(const std::vector<unsigned>& s) const; /** + * Create a character constant from a given string. + * @param s the string denoting the code point of the character (in base 16) + * @return the character constant + */ + Term mkChar(const std::string& s) const; + + /** + * Create a character constant from a given string. + * @param s the string denoting the code point of the character (in base 16) + * @return the character constant + */ + Term mkChar(const char* s) const; + + /** * Create a universe set of the given sort. * @param sort the sort of the set elements * @return the universe set constant @@ -2812,18 +2826,20 @@ class CVC4_PUBLIC Solver template <typename T> Term mkValHelper(T t) const; /* Helper for mkReal functions that take a string as argument. */ - Term mkRealFromStrHelper(std::string s) const; + Term mkRealFromStrHelper(const std::string& s) const; /* Helper for mkBitVector functions that take a string as argument. */ - Term mkBVFromStrHelper(std::string s, uint32_t base) const; + Term mkBVFromStrHelper(const std::string& s, uint32_t base) const; /* Helper for mkBitVector functions that take a string and a size as * arguments. */ - Term mkBVFromStrHelper(uint32_t size, std::string s, uint32_t base) const; + Term mkBVFromStrHelper(uint32_t size, const 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 for mkTerm functions that create Term from a Kind */ Term mkTermFromKind(Kind kind) const; + /* Helper for mkChar functions that take a string as argument. */ + Term mkCharFromStrHelper(const std::string& s) const; /** * Helper function that ensures that a given term is of sort real (as opposed diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index d0a73ce6a..1d0fb71cb 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2083,6 +2083,11 @@ termAtomic[CVC4::api::Term& atomTerm] api::Term v2 = SOLVER->mkConst(api::Sort(type2), "_emp2"); atomTerm = SOLVER->mkTerm(api::SEP_EMP, v1, v2); } + | CHAR_TOK HEX_LITERAL + { + std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); + atomTerm = SOLVER->mkChar(hexStr); + } | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals] { atomTerm = @@ -2094,10 +2099,10 @@ termAtomic[CVC4::api::Term& atomTerm] // Bit-vector constants | HEX_LITERAL - { - assert(AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0); - std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); - atomTerm = SOLVER->mkBitVector(hexStr, 16); + { + assert(AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0); + std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); + atomTerm = SOLVER->mkBitVector(hexStr, 16); } | BINARY_LITERAL { @@ -2686,6 +2691,7 @@ FORALL_TOK : 'forall'; CHOICE_TOK : { !PARSER_STATE->strictModeEnabled() }? 'choice'; EMP_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SEP) }? 'emp'; +CHAR_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) }? 'char'; TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'mkTuple'; TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tupSel'; |