summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/parser/CMakeLists.txt6
-rw-r--r--src/parser/antlr_input.h32
-rw-r--r--src/parser/cvc/Cvc.g32
-rw-r--r--src/parser/smt2/Smt2.g4
-rw-r--r--src/parser/smt2/smt2.cpp1
-rw-r--r--src/parser/smt2/smt2.h1
-rw-r--r--src/parser/tptp/Tptp.g2
-rw-r--r--test/api/CMakeLists.txt4
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})
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback