Miscellaneous cleaning of parser (#5369)

diff --git a/src/parser/parser.h b/src/parser/parser.h
index bfeafe78b7d020f3615c7e10a157207f6a3fa933..260ab33cf20f4f9d987c569732de88de5d3c72fd 100644 (file)
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -16,8 +16,8 @@
 
 #include "cvc4parser_public.h"
 
-#ifndef CVC4__PARSER__PARSER_STATE_H
-#define CVC4__PARSER__PARSER_STATE_H
+#ifndef CVC4__PARSER__PARSER_H
+#define CVC4__PARSER__PARSER_H
 
 #include <cassert>
 #include <list>
@@ -25,7 +25,6 @@
 #include <string>
 
 #include "api/cvc4cpp.h"
-#include "expr/expr.h"
 #include "expr/kind.h"
 #include "expr/symbol_table.h"
 #include "parser/input.h"
@@ -36,39 +35,9 @@
 namespace CVC4 {
 
 // Forward declarations
-class BooleanType;
 class Command;
-class FunctionType;
-class Type;
 class ResourceManager;
 
-//for sygus gterm two-pass parsing
-class CVC4_PUBLIC SygusGTerm {
-public:
-  enum{
-    gterm_op,
-    gterm_constant,
-    gterm_variable,
-    gterm_input_variable,
-    gterm_local_variable,
-    gterm_nested_sort,
-    gterm_unresolved,
-    gterm_ignore,
-  };
-  api::Sort d_type;
-  /** The parsed operator */
-  ParseOp d_op;
-  std::vector<api::Term> d_let_vars;
-  unsigned d_gterm_type;
-  std::string d_name;
-  std::vector< SygusGTerm > d_children;
-  
-  unsigned getNumChildren() { return d_children.size(); }
-  void addChild(){
-    d_children.push_back( SygusGTerm() );
-  }
-};
-
 namespace parser {
 
 class Input;

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 7647f8e5313ae80ac01d50e4b2b16ff7aade477b..fe051f0362ef8567f32d0c1f40485d0643903952 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -85,28 +85,12 @@ using namespace CVC4::parser;
 #include "smt/command.h"
 
 namespace CVC4 {
-  class Expr;
 
   namespace api {
     class Term;
     class Sort;
   }
-
-  namespace parser {
-    namespace smt2 {
-      /**
-       * Just exists to provide the uintptr_t constructor that ANTLR
-       * requires.
-       */
-      struct myExpr : public CVC4::api::Term {
-        myExpr() : CVC4::api::Term() {}
-        myExpr(void*) : CVC4::api::Term() {}
-        myExpr(const Expr& e) : CVC4::api::Term(d_solver, e) {}
-        myExpr(const myExpr& e) : CVC4::api::Term(e) {}
-      };/* struct myExpr */
-    }/* CVC4::parser::smt2 namespace */
-  }/* CVC4::parser namespace */
-
+  
 }/* CVC4 namespace */
 
 }/* @parser::includes */
@@ -132,8 +116,6 @@ namespace CVC4 {
 #include "util/hash.h"
 #include "util/integer.h"
 #include "util/rational.h"
-// \todo Review the need for this header
-#include "math.h"
 
 using namespace CVC4;
 using namespace CVC4::parser;
@@ -156,7 +138,7 @@ using namespace CVC4::parser;
  * @return the parsed expression, or the Null Expr if we've reached the
  * end of the input
  */
-parseExpr returns [CVC4::parser::smt2::myExpr expr]
+parseExpr returns [CVC4::api::Term expr = CVC4::api::Term()]
 @declarations {
   CVC4::api::Term expr2;
 }