diff options
-rw-r--r-- | src/parser/CMakeLists.txt | 6 | ||||
-rw-r--r-- | src/parser/antlr_input.h | 32 | ||||
-rw-r--r-- | src/parser/cvc/Cvc.g | 32 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 4 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 1 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 1 | ||||
-rw-r--r-- | src/parser/tptp/Tptp.g | 2 | ||||
-rw-r--r-- | test/api/CMakeLists.txt | 4 |
8 files changed, 3 insertions, 79 deletions
diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt index 26472740e..da6b1bd58 100644 --- a/src/parser/CMakeLists.txt +++ b/src/parser/CMakeLists.txt @@ -108,12 +108,6 @@ target_compile_definitions(cvc4parser PRIVATE -D__BUILDING_CVC4PARSERLIB) target_link_libraries(cvc4parser PUBLIC cvc4) target_link_libraries(cvc4parser PRIVATE ANTLR3) -if(USE_CLN) - target_link_libraries(cvc4parser PRIVATE ${CLN_LIBRARIES}) - target_include_directories(cvc4parser PRIVATE $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>) -endif() -target_link_libraries(cvc4parser PRIVATE GMP) - install(TARGETS cvc4parser EXPORT cvc4-targets DESTINATION ${CMAKE_INSTALL_LIBDIR}) diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index 2754e4167..5fcf853cc 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -31,9 +31,6 @@ #include "parser/input.h" #include "parser/line_buffer.h" #include "parser/parser_exception.h" -#include "util/bitvector.h" -#include "util/integer.h" -#include "util/rational.h" namespace cvc5 { namespace parser { @@ -178,15 +175,6 @@ public: /** Retrieve an unsigned from the text of a token */ static unsigned tokenToUnsigned( pANTLR3_COMMON_TOKEN token ); - /** Retrieve an Integer from the text of a token */ - static Rational tokenToInteger( pANTLR3_COMMON_TOKEN token ); - - /** Retrieve a Rational from the text of a token */ - static Rational tokenToRational(pANTLR3_COMMON_TOKEN token); - - /** Get a bitvector constant from the text of the number and the size token */ - static BitVector tokenToBitvector(pANTLR3_COMMON_TOKEN number, pANTLR3_COMMON_TOKEN size); - /** Get the ANTLR3 lexer for this input. */ pANTLR3_LEXER getAntlr3Lexer() { return d_lexer; } @@ -270,26 +258,6 @@ inline unsigned AntlrInput::tokenToUnsigned(pANTLR3_COMMON_TOKEN token) { return result; } -inline Rational AntlrInput::tokenToInteger(pANTLR3_COMMON_TOKEN token) { - return Rational( tokenText(token) ); -} - -inline Rational AntlrInput::tokenToRational(pANTLR3_COMMON_TOKEN token) { - return Rational::fromDecimal( tokenText(token) ); -} - -inline BitVector AntlrInput::tokenToBitvector(pANTLR3_COMMON_TOKEN number, pANTLR3_COMMON_TOKEN size) { - std::string number_str = tokenTextSubstr(number, 2); - unsigned sz = tokenToUnsigned(size); - Integer val(number_str); - if(val.modByPow2(sz) != val) { - std::stringstream ss; - ss << "Overflow in bitvector construction (specified bitvector size " << sz << " too small to hold value " << tokenText(number) << ")"; - throw std::invalid_argument(ss.str()); - } - return BitVector(sz, val); -} - } // namespace parser } // namespace cvc5 diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 2ad56d6e4..039eaf0ad 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -551,7 +551,6 @@ api::Term addNots(api::Solver* s, size_t n, api::Term e) { #include "parser/antlr_tracing.h" #include "parser/parser.h" #include "smt/command.h" -#include "util/rational.h" namespace cvc5 { class Expr; @@ -1321,12 +1320,6 @@ restrictedTypePossiblyFunctionLHS[cvc5::api::Sort& t, PARSER_STATE->unimplementedFeature("predicate subtyping not supported in this release"); } - /* subrange types */ - | LBRACKET bound DOTDOT bound RBRACKET - { - PARSER_STATE->unimplementedFeature("subrange typing not supported in this release"); - } - /* tuple types / old-style function types */ | LBRACKET ( type[t,check] { types.push_back(t); } ( COMMA type[t,check] { types.push_back(t); } )* )? RBRACKET @@ -1379,11 +1372,6 @@ parameterization[cvc5::parser::DeclarationCheck check, ( COMMA restrictedType[t,check] { Debug("parser-param") << "t = " << t << std::endl; params.push_back( t ); } )* RBRACKET ; -bound - : UNDERSCORE - | integer -; - typeLetDecl[cvc5::parser::DeclarationCheck check] @init { api::Sort t; @@ -2191,16 +2179,10 @@ simpleTerm[cvc5::api::Term& f] * This is a rational constant! Otherwise the parser interprets it as a tuple * selector! */ | DECIMAL_LITERAL { - Rational r = AntlrInput::tokenToRational($DECIMAL_LITERAL); - std::stringstream strRat; - strRat << r; - f = SOLVER->mkReal(strRat.str()); + f = SOLVER->mkReal(AntlrInput::tokenText($DECIMAL_LITERAL)); } | INTEGER_LITERAL { - Rational r = AntlrInput::tokenToRational($INTEGER_LITERAL); - std::stringstream strRat; - strRat << r; - f = SOLVER->mkInteger(strRat.str()); + f = SOLVER->mkInteger(AntlrInput::tokenText($INTEGER_LITERAL)); } /* bitvector literals */ | HEX_LITERAL @@ -2376,16 +2358,6 @@ numeral returns [unsigned k = 0] ; /** - * Similar to numeral but for arbitrary-precision, signed integer. - */ -integer returns [cvc5::Rational k = 0] - : INTEGER_LITERAL - { $k = AntlrInput::tokenToInteger($INTEGER_LITERAL); } - | MINUS_TOK INTEGER_LITERAL - { $k = -AntlrInput::tokenToInteger($INTEGER_LITERAL); } - ; - -/** * Similar to numeral but for strings. */ str[std::string& s] diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 34fabed0d..c347dc0db 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -109,10 +109,8 @@ namespace cvc5 { #include "parser/antlr_input.h" #include "parser/parser.h" #include "parser/smt2/smt2.h" -#include "util/floatingpoint.h" +#include "util/floatingpoint_size.h" #include "util/hash.h" -#include "util/integer.h" -#include "util/rational.h" using namespace cvc5; using namespace cvc5::parser; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 10396d1dc..9d4267dd2 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -21,7 +21,6 @@ #include "parser/antlr_input.h" #include "parser/parser.h" #include "parser/smt2/smt2_input.h" -#include "util/bitvector.h" // ANTLR defines these, which is really bad! #undef true diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 49b8c37d6..e28ef955c 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -28,7 +28,6 @@ #include "parser/parse_op.h" #include "parser/parser.h" #include "theory/logic_info.h" -#include "util/abstract_value.h" namespace cvc5 { diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 6877306a2..5f078cab7 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -107,8 +107,6 @@ using namespace cvc5::parser; #include "parser/antlr_input.h" #include "parser/parser.h" #include "parser/tptp/tptp.h" -#include "util/integer.h" -#include "util/rational.h" using namespace cvc5; using namespace cvc5::parser; diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt index 6dadbf759..48318012f 100644 --- a/test/api/CMakeLists.txt +++ b/test/api/CMakeLists.txt @@ -37,10 +37,6 @@ macro(cvc4_add_api_test name) add_executable(${name} ${name}.cpp) target_link_libraries(${name} PUBLIC main-test) target_compile_definitions(${name} PRIVATE ${CVC5_API_TEST_FLAGS}) - if(USE_CLN) - target_link_libraries(${name} PRIVATE CLN) - endif() - target_link_libraries(${name} PRIVATE GMP) set_target_properties(${name} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${test_bin_dir}) add_test(api/${name} ${test_bin_dir}/${name}) |