* Rename SMT parts (printer, parser) to SMT1

* Change --lang smt to mean SMT-LIBv2
* --lang smt1 now means SMT-LIBv1

* SMT-LIBv2 parser now gives helpful error if input looks like v1
* SMT-LIBv1 parser now gives helpful error if input looks like v2
* CVC presentation language parser now gives helpful error if input
  looks like either SMT-LIB v1 or v2

* Other associated changes

(this commit was certified error- and warning-free by the test-and-commit script.)

1 files changed, 0 insertions, 96 deletions

diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h
deleted file mode 100644
index b976a3b6a..000000000
--- a/src/parser/smt/smt_input.h
+++ /dev/null
@@ -1,96 +0,0 @@
-/*********************                                                        */
-/*! \file smt_input.h
- ** \verbatim
- ** Original author: cconway
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
- **
- ** \brief [[ Add file-specific comments here ]].
- **
- ** [[ Add file-specific comments here ]]
- **/
-
-#include "cvc4parser_private.h"
-
-#ifndef __CVC4__PARSER__SMT_INPUT_H
-#define __CVC4__PARSER__SMT_INPUT_H
-
-#include "parser/antlr_input.h"
-#include "parser/smt/generated/SmtLexer.h"
-#include "parser/smt/generated/SmtParser.h"
-
-// extern void SmtParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser);
-
-namespace CVC4 {
-
-class Command;
-class Expr;
-class ExprManager;
-
-namespace parser {
-
-class SmtInput : public AntlrInput {
-
-  /** The ANTLR3 SMT lexer for the input. */
-  pSmtLexer d_pSmtLexer;
-
-  /** The ANTLR3 CVC parser for the input. */
-  pSmtParser d_pSmtParser;
-
-public:
-
-  /**
-   * Create an input.
-   *
-   * @param inputStream the input stream to use
-   */
-  SmtInput(AntlrInputStream& inputStream);
-
-  /** Destructor. Frees the lexer and the parser. */
-  virtual ~SmtInput();
-
-  /** Get the language that this Input is reading. */
-  InputLanguage getLanguage() const throw() {
-    return language::input::LANG_SMTLIB;
-  }
-
-protected:
-
-  /**
-   * Parse a command from the input. Returns <code>NULL</code> if
-   * there is no command there to parse.
-   *
-   * @throws ParserException if an error is encountered during parsing.
-   */
-  Command* parseCommand()
-    throw(ParserException, TypeCheckingException, AssertionException);
-
-  /**
-   * Parse an expression from the input. Returns a null
-   * <code>Expr</code> if there is no expression there to parse.
-   *
-   * @throws ParserException if an error is encountered during parsing.
-   */
-  Expr parseExpr()
-    throw(ParserException, TypeCheckingException, AssertionException);
-
-private:
-
-  /**
-   * Initialize the class. Called from the constructors once the input
-   * stream is initialized.
-   */
-  void init();
-
-};/* class SmtInput */
-
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PARSER__SMT_INPUT_H */