From a06ec9eb224c437523f3bff0ac6f6437d924f36a Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 19 Apr 2021 11:30:04 +0200 Subject: [PATCH] Remove linking against gmp and cln in tests and parser (#6376) Finally, we no longer need to link against GMP and CLN for the parser and the tests. To actually achieve this, this PR also removes some dead code and unused includes from some parser files. --- src/parser/CMakeLists.txt | 6 ------ src/parser/antlr_input.h | 32 -------------------------------- src/parser/cvc/Cvc.g | 32 ++------------------------------ src/parser/smt2/Smt2.g | 4 +--- src/parser/smt2/smt2.cpp | 1 - src/parser/smt2/smt2.h | 1 - src/parser/tptp/Tptp.g | 2 -- 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 $) -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 @@ -2375,16 +2357,6 @@ numeral returns [unsigned k = 0] { $k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); } ; -/** - * 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. */ 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}) -- 2.30.2