From: Tim King <taking@cs.nyu.edu>
Date: Tue, 7 Nov 2017 18:35:42 +0000 (-0800)
Subject:  Removing an unused member from Tptp. Initializing members of Tptp. (#1326)
X-Git-Tag: cvc5-1.0.0~5501
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a2746472fb95b523dc838376c84467751f6ef764;p=cvc5.git

 Removing an unused member from Tptp. Initializing members of Tptp. (#1326)

* Removing an unused member from Tptp. Initializing members of Tptp.

* Removing delcaration for myPopCharStream.
---

diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index e49315609..af675dec1 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -29,8 +29,11 @@
 namespace CVC4 {
 namespace parser {
 
-Tptp::Tptp(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
-  Parser(exprManager,input,strictMode,parseOnly) {
+Tptp::Tptp(ExprManager* exprManager, Input* input, bool strictMode,
+           bool parseOnly)
+    : Parser(exprManager, input, strictMode, parseOnly),
+      d_cnf(false),
+      d_fof(false) {
   addTheory(Tptp::THEORY_CORE);
 
   /* Try to find TPTP dir */
@@ -135,14 +138,6 @@ bool newInputStream(std::string fileName, pANTLR3_LEXER lexer, std::vector< pANT
   return true;
 }
 
-/* overridden popCharStream for the lexer - necessary if we had symbol
- * filtering in file inclusion.
-void Tptp::myPopCharStream(pANTLR3_LEXER lexer) {
-  ((Tptp*)lexer->super)->d_oldPopCharStream(lexer);
-  ((Tptp*)lexer->super)->popScope();
-}
-*/
-
 void Tptp::includeFile(std::string fileName) {
   // security for online version
   if(!canIncludeFile()) {
@@ -153,15 +148,6 @@ void Tptp::includeFile(std::string fileName) {
   AntlrInput * ai = static_cast<AntlrInput *>(getInput());
   pANTLR3_LEXER lexer = ai->getAntlr3Lexer();
 
-  // set up popCharStream - would be necessary for handling symbol
-  // filtering in inclusions
-  /*
-  if(d_oldPopCharStream == NULL) {
-    d_oldPopCharStream = lexer->popCharStream;
-    lexer->popCharStream = myPopCharStream;
-  }
-  */
-
   // push the inclusion scope; will be popped by our special popCharStream
   // would be necessary for handling symbol filtering in inclusions
   //pushScope();
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index 1cc9c2d7f..c955d152e 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -146,9 +146,6 @@ class Tptp : public Parser {
 
   bool d_cnf; // in a cnf formula
   bool d_fof; // in an fof formula
-
-  static void myPopCharStream(pANTLR3_LEXER lexer);
-  void (*d_oldPopCharStream)(pANTLR3_LEXER);
 };/* class Tptp */