From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Mon, 19 Apr 2021 09:30:04 +0000 (+0200)
Subject: Remove linking against gmp and cln in tests and parser (#6376)
X-Git-Tag: cvc5-1.0.0~1887
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a06ec9eb224c437523f3bff0ac6f6437d924f36a;p=cvc5.git

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 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
@@ -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})