Lots of parser changes to make Chris happy. Yet more to come later.

5 files changed, 115 insertions, 235 deletions

diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am
index 6f5f1bfd4..96ad9c27f 100644
--- a/src/parser/smt/Makefile.am
+++ b/src/parser/smt/Makefile.am
@@ -24,8 +24,6 @@ ANTLR_STUFF = \
 libparsersmt_la_SOURCES = \
 	smt_lexer.g \
 	smt_parser.g \
-	smt_parser.h \
-	smt_parser.cpp \
 	$(ANTLR_STUFF)
 
 BUILT_SOURCES = $(ANTLR_STUFF)
diff --git a/src/parser/smt/Makefile.in b/src/parser/smt/Makefile.in
index 721ff0e2b..6145b4c4e 100644
--- a/src/parser/smt/Makefile.in
+++ b/src/parser/smt/Makefile.in
@@ -56,7 +56,7 @@ am__objects_1 =
 am__objects_2 = AntlrSmtLexer.lo $(am__objects_1)
 am__objects_3 = AntlrSmtParser.lo
 am__objects_4 = $(am__objects_2) $(am__objects_3)
-am_libparsersmt_la_OBJECTS = smt_parser.lo $(am__objects_4)
+am_libparsersmt_la_OBJECTS = $(am__objects_4)
 libparsersmt_la_OBJECTS = $(am_libparsersmt_la_OBJECTS)
 DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
 depcomp = $(SHELL) $(top_srcdir)/config/depcomp
@@ -249,8 +249,6 @@ ANTLR_STUFF = \
 libparsersmt_la_SOURCES = \
 	smt_lexer.g \
 	smt_parser.g \
-	smt_parser.h \
-	smt_parser.cpp \
 	$(ANTLR_STUFF)
 
 BUILT_SOURCES = $(ANTLR_STUFF)
@@ -310,7 +308,6 @@ distclean-compile:
 
 @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrSmtLexer.Plo@am__quote@
 @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrSmtParser.Plo@am__quote@
-@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/smt_parser.Plo@am__quote@
 
 .cpp.o:
 @am__fastdepCXX_TRUE@	$(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $<
diff --git a/src/parser/smt/smt_parser.cpp b/src/parser/smt/smt_parser.cpp
deleted file mode 100644
index 8c5773e32..000000000
--- a/src/parser/smt/smt_parser.cpp
+++ /dev/null
@@ -1,79 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** smt_parser.cpp
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): dejan
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.
- **
- ** SMT-LIB language parser implementation.
- **/
-
-#include <iostream>
-#include <fstream>
-
-#include "parser/parser.h"
-#include "util/command.h"
-#include "util/Assert.h"
-#include "parser/parser_exception.h"
-#include "parser/antlr_parser.h"
-#include "parser/smt/smt_parser.h"
-#include "parser/smt/generated/AntlrSmtParser.hpp"
-#include "parser/smt/generated/AntlrSmtLexer.hpp"
-
-using namespace std;
-
-namespace CVC4 {
-namespace parser {
-
-Command* SmtParser::parseNextCommand() throw(ParserException) {
-  Command* cmd = 0;
-  if(!done()) {
-    try {
-      cmd = d_antlr_parser->benchmark();
-      setDone();
-    } catch(antlr::ANTLRException& e) {
-      setDone();
-      throw ParserException(e.toString());
-    }
-  }
-  return cmd;
-}
-
-Expr SmtParser::parseNextExpression() throw(ParserException) {
-  Expr result;
-  if(!done()) {
-    try {
-      result = d_antlr_parser->an_formula();
-    } catch(antlr::ANTLRException& e) {
-      setDone();
-      throw ParserException(e.toString());
-    }
-  }
-  return result;
-}
-
-SmtParser::~SmtParser() {
-  delete d_antlr_parser;
-  delete d_antlr_lexer;
-}
-
-SmtParser::SmtParser(ExprManager* em, istream& input, const char* file_name) :
-  Parser(em), d_input(input) {
-  if(!d_input) {
-    throw ParserException(string("Read error") +
-                          ((file_name != NULL) ? (string(" on ") + file_name) : ""));
-  }
-  d_antlr_lexer = new AntlrSmtLexer(input);
-  d_antlr_lexer->setFilename(file_name);
-  d_antlr_parser = new AntlrSmtParser(*d_antlr_lexer);
-  d_antlr_parser->setExpressionManager(d_expr_manager);
-  d_antlr_parser->setFilename(file_name);
-}
-
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index 6e0051821..f7045fa7e 100644
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -27,6 +27,108 @@ options {
   defaultErrorHandler = false;      // Skip the defaul error handling, just break with exceptions
   k = 2;
 }
+
+/**
+ * Parses an expression.
+ * @return the parsed expression
+ */
+parseExpr returns [CVC4::Expr expr]
+  : expr = annotatedFormula
+  ;
+
+/**
+ * Parses a command (the whole benchmark)
+ * @return the command of the benchmark
+ */
+parseCommand returns [CVC4::Command* cmd]
+  : cmd = benchmark
+  ; 
+ 
+/**
+ * Matches the whole SMT-LIB benchmark.
+ * @return the sequence command containing the whole problem
+ */  
+benchmark returns [Command* cmd]
+  : LPAREN BENCHMARK IDENTIFIER cmd = benchAttributes RPAREN
+  | EOF { cmd = 0; } 
+  ;
+
+/**
+ * Matchecs sequence of benchmark attributes and returns a pointer to a command 
+ * sequence command.
+ * @return the command sequence 
+ */
+benchAttributes returns [CVC4::CommandSequence* cmd_seq = new CommandSequence()]
+{
+  Command* cmd;
+}
+  : (cmd = benchAttribute { if (cmd) cmd_seq->addCommand(cmd); } )+ 
+  ;
+  
+/**
+ * Matches a benchmark attribute, sucha as ':logic', ':formula', and returns 
+ * a corresponding command
+ * @retrurn a command corresponding to the attribute
+ */
+benchAttribute returns [ Command* smt_command = 0]
+{
+  Expr formula;  
+  string logic; 
+  SetBenchmarkStatusCommand::BenchmarkStatus b_status = SetBenchmarkStatusCommand::SMT_UNKNOWN;
+}
+  : C_LOGIC       logic = identifier                  { smt_command = new SetBenchmarkLogicCommand(logic);   }      
+  | C_ASSUMPTION  formula = annotatedFormula          { smt_command = new AssertCommand(formula);   }       
+  | C_FORMULA     formula = annotatedFormula          { smt_command = new CheckSatCommand(formula); }
+  | C_STATUS      b_status = status                   { smt_command = new SetBenchmarkStatusCommand(b_status); }        
+  | C_EXTRAPREDS  LPAREN (pred_symb_decl)+ RPAREN  
+  | C_NOTES       STRING_LITERAL        
+  | annotation
+  ;
+
+/**
+ * Matches an identifier and returns a string.
+ * @param check what kinds of check to do on the symbol
+ * @return the id string
+ */
+identifier[DeclarationCheck check = CHECK_NONE] returns [std::string id]
+  : x:IDENTIFIER { checkDeclation(x->getText(), check) }?
+    { 
+      id = x->getText(); 
+    } 
+    exception catch [antlr::SemanticException& ex] {
+      switch (check) {
+        case CHECK_DECLARED: rethrow(ex, "Symbol " + id + " not declared");
+        case CHECK_UNDECLARED: rethrow(ex, "Symbol " + id + " already declared");
+        default: throw ex;
+      }          
+    }    
+  ;
+
+/** 
+ * Matches an annotated formula.
+ * @return the expression representing the formula 
+ */
+annotatedFormula returns [CVC4::Expr formula] 
+{ 
+  Kind kind; 
+  vector<Expr> children;
+}
+  :  formula = annotatedAtom 
+  |  LPAREN kind = boolConnective annotatedFormulas[children] RPAREN { formula = mkExpr(kind, children);  }    
+  ;
+
+/**
+ * Matches an annotated proposition atom, which is either a propositional atom 
+ * or built of other atoms using a predicate symbol.  
+ */
+annotatedAtom returns [CVC4::Expr atom] 
+  : atom = propositionalAtom  
+  ;
+
+
+
+
+
  
 /**
  * Matches an attribute name from the input (:attribute_name).
@@ -34,7 +136,7 @@ options {
 attribute 
   :  C_IDENTIFIER
   ;
-  
+   
 /**
  * Matches the sort symbol, which can be an arbitrary identifier.
  */
@@ -60,7 +162,7 @@ pred_symb returns [std::string p]
 /**
  * Matches a propositional atom. 
  */
-prop_atom returns [CVC4::Expr atom]
+propositionalAtom returns [CVC4::Expr atom]
 {
   std::string p;
 } 
@@ -71,22 +173,11 @@ prop_atom returns [CVC4::Expr atom]
    | TRUE          { atom = getTrueExpr(); }
    | FALSE         { atom = getFalseExpr(); }
    ;
-    
-/**
- * Matches an annotated proposition atom, which is either a propositional atom 
- * or built of other atoms using a predicate symbol. Annotation can be added if
- * enclosed in brackets. The prop_atom rule from the original SMT grammar is inlined
- * here in order to get rid of the ugly antlr non-determinism warnings. 
- */
- // [chris 12/15/2009] FIXME: Where is the annotation? 
-an_atom returns [CVC4::Expr atom] 
-  : atom = prop_atom  
-  ;
-  
+      
 /**
  * Matches on of the unary Boolean connectives.  
  */
-bool_connective returns [CVC4::Kind kind]
+boolConnective returns [CVC4::Kind kind]
   : NOT      { kind = CVC4::NOT;     } 
   | IMPLIES  { kind = CVC4::IMPLIES; }
   | AND      { kind = CVC4::AND;     }
@@ -94,24 +185,12 @@ bool_connective returns [CVC4::Kind kind]
   | XOR      { kind = CVC4::XOR;     }
   | IFF      { kind = CVC4::IFF;     }
   ;
-  
-/** 
- * Matches an annotated formula. 
- */
-an_formula returns [CVC4::Expr formula] 
-{ 
-  Kind kind; 
-  vector<Expr> children;
-}
-  :  formula = an_atom 
-  |  LPAREN kind = bool_connective an_formulas[children] RPAREN { formula = newExpression(kind, children);  }    
-  ;
-  
-an_formulas[std::vector<Expr>& formulas]
+    
+annotatedFormulas[std::vector<Expr>& formulas]
 {
   Expr f;
 }
-  : ( f = an_formula { formulas.push_back(f); } )+
+  : ( f = annotatedFormula { formulas.push_back(f); } )+
   ;
    
 /**
@@ -138,44 +217,8 @@ sort_symbs[std::vector<std::string>& sorts]
 /**
  * Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'.
  */
-status returns [ AntlrParser::BenchmarkStatus status ]
-  : SAT       { status = SMT_SATISFIABLE;    }
-  | UNSAT     { status = SMT_UNSATISFIABLE;  }
-  | UNKNOWN   { status = SMT_UNKNOWN;        }
-  ;
-  
-/**
- * Matches a benchmark attribute, sucha as ':logic', ':formula', etc.
- */
-bench_attribute returns [ Command* smt_command = 0]
-{
-  BenchmarkStatus b_status = SMT_UNKNOWN;
-  Expr formula;  
-  vector<string> sorts;
-}
-  : C_LOGIC       IDENTIFIER      
-  | C_ASSUMPTION  formula = an_formula                { smt_command = new AssertCommand(formula);   }       
-  | C_FORMULA     formula = an_formula                { smt_command = new CheckSatCommand(formula); }
-  | C_STATUS      b_status = status                   { setBenchmarkStatus(b_status);               }        
-  | C_EXTRASORTS  LPAREN sort_symbs[sorts] RPAREN     { addExtraSorts(sorts);                       }     
-  | C_EXTRAPREDS  LPAREN (pred_symb_decl)+ RPAREN  
-  | C_NOTES       STRING_LITERAL        
-  | annotation
-  ;
-
-/**
- * Returns a pointer to a command sequence command.
- */
-bench_attributes returns [CVC4::CommandSequence* cmd_seq = new CommandSequence()]
-{
-  Command* cmd;
-}
-  : (cmd = bench_attribute { if (cmd) cmd_seq->addCommand(cmd); } )+ 
-  ;
-  
-/**
- * Matches the whole SMT-LIB benchmark.
- */  
-benchmark returns [Command* cmd]
-  : LPAREN BENCHMARK IDENTIFIER cmd = bench_attributes RPAREN 
-  ;
+status returns [ SetBenchmarkStatusCommand::BenchmarkStatus status ]
+  : SAT       { status = SetBenchmarkStatusCommand::SMT_SATISFIABLE;    }
+  | UNSAT     { status = SetBenchmarkStatusCommand::SMT_UNSATISFIABLE;  }
+  | UNKNOWN   { status = SetBenchmarkStatusCommand::SMT_UNKNOWN;        }
+  ;
\ No newline at end of file
diff --git a/src/parser/smt/smt_parser.h b/src/parser/smt/smt_parser.h
deleted file mode 100644
index 21c278a37..000000000
--- a/src/parser/smt/smt_parser.h
+++ /dev/null
@@ -1,79 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** smt_parser.h
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): cconway, dejan
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.
- **
- ** SMT-LIB language parser abstraction.
- **/
-
-#ifndef __CVC4__PARSER__SMT_PARSER_H
-#define __CVC4__PARSER__SMT_PARSER_H
-
-#include <string>
-#include <iostream>
-#include <fstream>
-#include "cvc4_config.h"
-#include "parser/parser_exception.h"
-#include "parser/parser.h"
-
-namespace CVC4 {
-namespace parser {
-
-/**
- * The SMT parser.
- */
-class CVC4_PUBLIC SmtParser : public Parser {
-
-public:
-
-  /**
-   * Construct the parser that uses the given expression manager and input stream.
-   * @param em the expression manager to use
-   * @param input the input stream to parse
-   * @param file_name the name of the file (for diagnostic output)
-   */
-  SmtParser(ExprManager* em, std::istream& input, const char* file_name = "");
-
-  /**
-   * Destructor.
-   */
-  ~SmtParser();
-
-  /**
-   * Parses the next command. By default, the SMT-LIB parser produces
-   * one CommandSequence command. If parsing is successful, we should
-   * be done after the first call to this command.
-   * @return the CommandSequence command that includes the whole
-   * benchmark
-   */
-  Command* parseNextCommand() throw(ParserException);
-
-  /**
-   * Parses the next complete expression of the stream.
-   * @return the expression parsed
-   */
-  Expr parseNextExpression() throw(ParserException);
-
-protected:
-
-  /** The ANTLR smt lexer */
-  AntlrSmtLexer* d_antlr_lexer;
-
-  /** The ANTLR smt parser */
-  AntlrSmtParser* d_antlr_parser;
-
-  /** The file stream we might be using */
-  std::istream& d_input;
-};
-
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PARSER__SMT_PARSER_H */