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.

diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index 26472740e378a086026211d720891aaa61b58a17..da6b1bd58722975ce68a5f713bf79ea175d4b094 100644 (file)
--- 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 2754e4167dbdd9f9edbe9ad39f09a7cd033b3648..5fcf853cc55db012720d14cca6ad5c0f6527fbdb 100644 (file)
--- 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 2ad56d6e460561ded3c1782a9e77295417371d60..039eaf0ad8321aac02034843dbf475e6bc241032 100644 (file)
--- 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 34fabed0dc7c327590c8334a1747530749f44119..c347dc0db0a4b85ba19d9d8fd346b2065dd5b452 100644 (file)
--- 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 10396d1dc63bbde2ee27d98779dba122088b05bb..9d4267dd2b847363e58aaf00cc882fee1d7132fd 100644 (file)
--- 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 49b8c37d655762b6cc284f499e342a8cf605da7c..e28ef955c125b9fdb38cec9d4ede2af00c07e9d0 100644 (file)
--- 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 6877306a2f9fd2c150170d859d998030008d22d4..5f078cab7159ac14be5a14c3df9d60f7feedacfc 100644 (file)
--- 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 6dadbf759229938d92203c79762ea026936b72c1..48318012fe49af30535ca53b1f8f021d9d2973fb 100644 (file)
--- 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})