Remove SMT1 parser. (#3228)

This commit removes the SMT1 parser infrastructure and adds the SMT2 translations of the SMT1 regression tests. For now this commit removes regression test regress3/pp-regfile.smt since the SMT2 translation has a file size of 887M (vs. 172K for the SMT1 version).

Fixes #2948 and fixes #1313.

12 files changed, 4 insertions, 1535 deletions

diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index 96790f834..78ab82cb4 100644
--- a/src/parser/CMakeLists.txt
+++ b/src/parser/CMakeLists.txt
@@ -37,10 +37,6 @@ set(libcvc4parser_src_files
   parser_builder.cpp
   parser_builder.h
   parser_exception.h
-  smt1/smt1.cpp
-  smt1/smt1.h
-  smt1/smt1_input.cpp
-  smt1/smt1_input.h
   smt2/parse_op.h
   smt2/smt2.cpp
   smt2/smt2.h
@@ -59,7 +55,7 @@ set(libcvc4parser_src_files
 #-----------------------------------------------------------------------------#
 # Generate parsers for all supported languages
 
-foreach(lang Cvc Smt1 Smt2 Tptp)
+foreach(lang Cvc Smt2 Tptp)
   string(TOLOWER ${lang} lang_dir)
   file(MAKE_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/${lang_dir})
   add_custom_command(
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 69cac434a..77efff951 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -30,7 +30,6 @@
 #include "parser/memory_mapped_input_buffer.h"
 #include "parser/parser.h"
 #include "parser/parser_exception.h"
-#include "parser/smt1/smt1_input.h"
 #include "parser/smt2/smt2_input.h"
 #include "parser/smt2/sygus_input.h"
 #include "parser/tptp/tptp_input.h"
@@ -247,9 +246,6 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre
     input = new CvcInput(inputStream);
     break;
   }
-  case LANG_SMTLIB_V1:
-    input = new Smt1Input(inputStream);
-    break;
 
   case LANG_SYGUS:
   case LANG_SYGUS_V2: input = new SygusInput(inputStream); break;
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 3464d967d..038c1f1d0 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -616,7 +616,7 @@ parseCommand returns [CVC4::Command* cmd_return = NULL]
     if(s == "benchmark") {
         PARSER_STATE->parseError(
             "In CVC4 presentation language mode, but SMT-LIBv1 format "
-            "detected.  Use --lang smt1 for SMT-LIBv1 support.");
+            "detected, which is not supported anymore.");
       } else if(s == "set" || s == "get" || s == "declare" ||
                 s == "define" || s == "assert") {
         PARSER_STATE->parseError(
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 4ce99ce9d..28a965278 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -27,7 +27,6 @@
 #include "options/options.h"
 #include "parser/input.h"
 #include "parser/parser.h"
-#include "smt1/smt1.h"
 #include "smt2/smt2.h"
 #include "tptp/tptp.h"
 
@@ -90,9 +89,6 @@ Parser* ParserBuilder::build()
   Parser* parser = NULL;
   switch (d_lang)
   {
-    case language::input::LANG_SMTLIB_V1:
-      parser = new Smt1(d_solver, input, d_strictMode, d_parseOnly);
-      break;
     case language::input::LANG_SYGUS:
     case language::input::LANG_SYGUS_V2:
       parser = new Smt2(d_solver, input, d_strictMode, d_parseOnly);
diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g
deleted file mode 100644
index ca67ec592..000000000
--- a/src/parser/smt1/Smt1.g
+++ /dev/null
@@ -1,893 +0,0 @@
-/* *******************                                                        */
-/*! \file Smt1.g
- ** \verbatim
- ** Top contributors (to current version):
- **   Christopher L. Conway, Morgan Deters, Dejan Jovanovic
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Parser for SMT-LIB input language.
- **
- ** Parser for SMT-LIB input language.
- **/
-
-grammar Smt1;
-
-options {
-  // C output for antlr
-  language = 'C';
-
-  // Skip the default error handling, just break with exceptions
-  // defaultErrorHandler = false;
-
-  // Only lookahead of <= k requested (disable for LL* parsing)
-  // Note that CVC4's BoundedTokenBuffer requires a fixed k !
-  // If you change this k, change it also in smt1_input.cpp !
-  k = 2;
-}/* options */
-
-@header {
-/**
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.
- **/
-}/* @header */
-
-@lexer::includes {
-
-/** This suppresses warnings about the redefinition of token symbols between
-  * different parsers. The redefinitions should be harmless as long as no
-  * client: (a) #include's the lexer headers for two grammars AND (b) uses the
-  * token symbol definitions.
-  */
-#pragma GCC system_header
-
-#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
-/* This improves performance by ~10 percent on big inputs.
- * This option is only valid if we know the input is ASCII (or some 8-bit encoding).
- * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16.
- * Otherwise, we have to let the lexer detect the encoding at runtime.
- */
-#  define ANTLR3_INLINE_INPUT_ASCII
-#  define ANTLR3_INLINE_INPUT_8BIT
-#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
-
-#include "parser/antlr_tracing.h"
-}/* @lexer::includes */
-
-@parser::includes {
-
-#include <algorithm>
-#include <memory>
-#include <stdint.h>
-
-#include "smt/command.h"
-#include "parser/parser.h"
-#include "parser/antlr_tracing.h"
-
-namespace CVC4 {
-  class Expr;
-
-  namespace parser {
-    namespace smt1 {
-      /**
-       * Just exists to provide the uintptr_t constructor that ANTLR
-       * requires.
-       */
-      struct myExpr : public CVC4::Expr {
-        myExpr() : CVC4::Expr() {}
-        myExpr(void*) : CVC4::Expr() {}
-        myExpr(const Expr& e) : CVC4::Expr(e) {}
-        myExpr(const myExpr& e) : CVC4::Expr(e) {}
-      };/* struct myExpr */
-
-      /**
-       * Just exists to provide the uintptr_t constructor that ANTLR
-       * requires.
-       */
-      struct myType : public CVC4::Type {
-        myType() : CVC4::Type() {}
-        myType(void*) : CVC4::Type() {}
-        myType(const Type& t) : CVC4::Type(t) {}
-        myType(const myType& t) : CVC4::Type(t) {}
-      };/* struct myType */
-    }/* CVC4::parser::smt1 namespace */
-  }/* CVC4::parser namespace */
-}/* CVC4 namespace */
-
-}/* @parser::includes */
-
-@parser::postinclude {
-
-#include <vector>
-
-#include "base/output.h"
-#include "expr/expr.h"
-#include "expr/kind.h"
-#include "expr/type.h"
-#include "parser/antlr_input.h"
-#include "parser/parser.h"
-#include "parser/smt1/smt1.h"
-#include "util/integer.h"
-#include "util/rational.h"
-
-using namespace CVC4;
-using namespace CVC4::parser;
-
-/* These need to be macros so they can refer to the PARSER macro, which will be defined
- * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
-#undef PARSER_STATE
-#define PARSER_STATE ((Smt1*)PARSER->super)
-#undef EXPR_MANAGER
-#define EXPR_MANAGER PARSER_STATE->getExprManager()
-#undef MK_EXPR
-#define MK_EXPR EXPR_MANAGER->mkExpr
-#undef MK_CONST
-#define MK_CONST EXPR_MANAGER->mkConst
-
-}/* @parser::postinclude */
-
-
-/**
- * Parses an expression.
- * @return the parsed expression
- */
-parseExpr returns [CVC4::parser::smt1::myExpr expr]
-  : annotatedFormula[expr]
-  | EOF
-  ;
-
-/**
- * Parses a command (the whole benchmark)
- * @return the command of the benchmark
- */
-parseCommand returns [CVC4::Command* cmd_return = NULL]
-@declarations {
-  std::unique_ptr<CVC4::Command> cmd;
-}
-@after {
-  cmd_return = cmd.release();
-}
-  : b = benchmark[&cmd]
-  | LPAREN_TOK c=IDENTIFIER
-    { std::string s = AntlrInput::tokenText($c);
-      if(s == "set" || s == "get") {
-        PARSER_STATE->parseError(std::string("In SMT-LIBv1 mode, expected keyword `benchmark', but it looks like you're writing SMT-LIBv2.  Use --lang smt for SMT-LIBv2."));
-      } else {
-        PARSER_STATE->parseError(std::string("expected keyword `benchmark', got `" + s + "'"));
-      }
-    }
-  ;
-
-/**
- * Matches the whole SMT-LIB benchmark.
- * @return the sequence command containing the whole problem
- */
-benchmark [std::unique_ptr<CVC4::Command>* cmd]
-  : LPAREN_TOK BENCHMARK_TOK IDENTIFIER benchAttributes[cmd] RPAREN_TOK
-  | EOF
-  ;
-
-/**
- * Matches a sequence of benchmark attributes and returns a pointer to a
- * command sequence.
- * @return the command sequence
- */
-benchAttributes [std::unique_ptr<CVC4::Command>* cmd]
-@init {
-  std::unique_ptr<CVC4::CommandSequence> cmd_seq(new CommandSequence());
-  std::unique_ptr<CVC4::Command> attribute;
-}
-@after {
-  cmd->reset(cmd_seq.release());
-}
-  : (benchAttribute[&attribute]
-     { if (attribute) cmd_seq->addCommand(attribute.release()); }
-    )+
-  ;
-
-/**
- * Matches a benchmark attribute, such as ':logic', ':formula', and returns
- * a corresponding command
- * @return a command corresponding to the attribute
- */
-benchAttribute [std::unique_ptr<CVC4::Command>* smt_command]
-@declarations {
-  std::string name;
-  BenchmarkStatus b_status;
-  Expr expr;
-  std::unique_ptr<CVC4::CommandSequence> command_seq;
-  std::unique_ptr<CVC4::Command> declaration_command;
-}
-  : LOGIC_TOK identifier[name,CHECK_NONE,SYM_VARIABLE]
-    { PARSER_STATE->preemptCommand(new SetBenchmarkLogicCommand(name));
-      PARSER_STATE->setLogic(name);
-      smt_command->reset(new EmptyCommand());
-    }
-  | ASSUMPTION_TOK annotatedFormula[expr]
-    { smt_command->reset(new AssertCommand(expr)); }
-  | FORMULA_TOK annotatedFormula[expr]
-    { smt_command->reset(new CheckSatCommand(expr)); }
-  | STATUS_TOK status[b_status]
-    { smt_command->reset(new SetBenchmarkStatusCommand(b_status)); }
-  | EXTRAFUNS_TOK LPAREN_TOK
-    { command_seq.reset(new CommandSequence()); }
-    ( functionDeclaration[&declaration_command]
-      { command_seq->addCommand(declaration_command.release()); }
-    )+ RPAREN_TOK
-      { smt_command->reset(command_seq.release()); }
-  | EXTRAPREDS_TOK LPAREN_TOK
-    { command_seq.reset(new CommandSequence()); }
-    ( predicateDeclaration[&declaration_command]
-      { command_seq->addCommand(declaration_command.release()); }
-    )+ RPAREN_TOK
-      { smt_command->reset(command_seq.release()); }
-  | EXTRASORTS_TOK LPAREN_TOK
-      { command_seq.reset(new CommandSequence()); }
-    ( sortDeclaration[&declaration_command]
-      { command_seq->addCommand(declaration_command.release()); }
-    )+ RPAREN_TOK
-      { smt_command->reset(command_seq.release()); }
-  | NOTES_TOK STRING_LITERAL
-    { smt_command->reset(
-          new CommentCommand(AntlrInput::tokenText($STRING_LITERAL))); }
-  | annotation[smt_command]
-  ;
-
-/**
- * Matches an annotated formula.
- * @return the expression representing the formula
- */
-annotatedFormula[CVC4::Expr& expr]
-@init {
-  Debug("parser") << "annotated formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
-  Kind kind;
-  std::string name;
-  std::vector<Expr> args; /* = getExprVector(); */
-  std::vector<Expr> args2;
-  Expr op; /* Operator expression FIXME: move away kill it */
-}
-  : /* a built-in operator application */
-    LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr]
-    { if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) {
-        /* Unary AND/OR can be replaced with the argument.
-	 * It just so happens expr should already be the only argument. */
-        assert( expr == args[0] );
-      } else if( CVC4::kind::isAssociative(kind) &&
-                 args.size() > EXPR_MANAGER->maxArity(kind) ) {
-    	/* Special treatment for associative operators with lots of children */
-        expr = EXPR_MANAGER->mkAssociative(kind,args);
-      } else if(!PARSER_STATE->strictModeEnabled() &&
-                kind == CVC4::kind::MINUS && args.size() == 1) {
-        /* Special fix-up for unary minus improperly used in some benchmarks */
-        expr = MK_EXPR(CVC4::kind::UMINUS, args[0]);
-      } else {
-        PARSER_STATE->checkArity(kind, args.size());
-        expr = MK_EXPR(kind, args);
-      }
-    }
-    termAnnotation[expr]* RPAREN_TOK
-
-  | /* A quantifier */
-    LPAREN_TOK
-    ( FORALL_TOK { kind = kind::FORALL; } | EXISTS_TOK { kind = kind::EXISTS; } )
-    { PARSER_STATE->pushScope(); }
-    ( LPAREN_TOK let_identifier[name,CHECK_NONE] t=sortSymbol RPAREN_TOK
-      { args.push_back(PARSER_STATE->mkBoundVar(name, t)); }
-    )+
-    annotatedFormula[expr]
-    { args2.push_back( MK_EXPR( kind::BOUND_VAR_LIST, args ) );
-      args2.push_back(expr);
-      expr = MK_EXPR(kind, args2);
-    }
-    termAnnotation[expr]* RPAREN_TOK
-    { PARSER_STATE->popScope(); }
-
-  | /* A non-built-in function application */
-
-    // Semantic predicate not necessary if parenthesized subexpressions
-    // are disallowed
-    // { isFunction(LT(2)->getText()) }?
-    LPAREN_TOK
-    parameterizedOperator[op]
-    annotatedFormulas[args,expr]
-    // TODO: check arity
-    { expr = MK_EXPR(op,args); }
-    termAnnotation[expr]* RPAREN_TOK
-
-  | /* An ite expression */
-    LPAREN_TOK ITE_TOK
-    annotatedFormula[expr]
-    { args.push_back(expr); }
-    annotatedFormula[expr]
-    { args.push_back(expr); }
-    annotatedFormula[expr]
-    { args.push_back(expr);
-      expr = MK_EXPR(CVC4::kind::ITE, args); }
-    termAnnotation[expr]* RPAREN_TOK
-
-  | /* a let/flet binding */
-    LPAREN_TOK
-    ( LET_TOK LPAREN_TOK let_identifier[name,CHECK_UNDECLARED]
-      | FLET_TOK LPAREN_TOK flet_identifier[name,CHECK_UNDECLARED] )
-    annotatedFormula[expr] RPAREN_TOK
-    { PARSER_STATE->pushScope();
-      PARSER_STATE->defineVar(name,expr); }
-    annotatedFormula[expr]
-    termAnnotation[expr]* RPAREN_TOK
-    { PARSER_STATE->popScope(); }
-
-    /* constants */
-  | TRUE_TOK          { expr = MK_CONST(bool(true)); }
-  | FALSE_TOK         { expr = MK_CONST(bool(false)); }
-  | NUMERAL_TOK
-    { expr = MK_CONST( AntlrInput::tokenToInteger($NUMERAL_TOK) ); }
-  | RATIONAL_TOK
-    { // FIXME: This doesn't work because an SMT rational is not a
-      // valid GMP rational string
-      expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL_TOK) ); }
-  | n = BITVECTOR_BV_CONST '[' size = NUMERAL_TOK ']'
-    { expr = MK_CONST( AntlrInput::tokenToBitvector($n, $size) ); }
-  | n = BITVECTOR1_BV_CONST
-    { unsigned int bit = AntlrInput::tokenText($n)[3] - '0';
-      expr = MK_CONST( BitVector(1, bit) );
-    }
-    // NOTE: Theory constants go here
-    /* TODO: quantifiers, arithmetic constants */
-
-  | /* a variable */
-    ( identifier[name,CHECK_DECLARED,SYM_VARIABLE]
-      | let_identifier[name,CHECK_DECLARED]
-      | flet_identifier[name,CHECK_DECLARED] )
-    { expr = PARSER_STATE->getVariable(name); }
-  ;
-
-/**
- * Matches a sequence of annotated formulas and puts them into the
- * formulas vector.
- * @param formulas the vector to fill with formulas
- * @param expr an Expr reference for the elements of the sequence
- */
-/* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every
- * time through this rule. */
-annotatedFormulas[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr]
-  : ( annotatedFormula[expr] { formulas.push_back(expr); } )+
-  ;
-
-/**
-* Matches a builtin operator symbol and sets kind to its associated Expr kind.
-*/
-builtinOp[CVC4::Kind& kind]
-@init {
-  Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl;
-}
-  : NOT_TOK      { $kind = CVC4::kind::NOT;     }
-  | IMPLIES_TOK  { $kind = CVC4::kind::IMPLIES; }
-  | AND_TOK      { $kind = CVC4::kind::AND;     }
-  | OR_TOK       { $kind = CVC4::kind::OR;      }
-  | XOR_TOK      { $kind = CVC4::kind::XOR;     }
-  | IFF_TOK      { $kind = CVC4::kind::EQUAL;   }
-  | EQUAL_TOK    { $kind = CVC4::kind::EQUAL;   }
-  | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; }
-  // Arithmetic
-  | GREATER_THAN_TOK
-                 { $kind = CVC4::kind::GT; }
-  | GREATER_THAN_TOK EQUAL_TOK
-                 { $kind = CVC4::kind::GEQ; }
-  | LESS_THAN_TOK EQUAL_TOK
-                 { $kind = CVC4::kind::LEQ; }
-  | LESS_THAN_TOK
-                 { $kind = CVC4::kind::LT; }
-  | PLUS_TOK     { $kind = CVC4::kind::PLUS; }
-  | STAR_TOK     { $kind = CVC4::kind::MULT; }
-  | TILDE_TOK    { $kind = CVC4::kind::UMINUS; }
-  | MINUS_TOK    { $kind = CVC4::kind::MINUS; }
-  | DIV_TOK      { $kind = CVC4::kind::DIVISION; }
-  // Bit-vectors
-  | CONCAT_TOK   { $kind = CVC4::kind::BITVECTOR_CONCAT; }
-  | BVAND_TOK    { $kind = CVC4::kind::BITVECTOR_AND;    }
-  | BVOR_TOK     { $kind = CVC4::kind::BITVECTOR_OR;     }
-  | BVXOR_TOK    { $kind = CVC4::kind::BITVECTOR_XOR;    }
-  | BVNOT_TOK    { $kind = CVC4::kind::BITVECTOR_NOT;    }
-  | BVNAND_TOK   { $kind = CVC4::kind::BITVECTOR_NAND;   }
-  | BVNOR_TOK    { $kind = CVC4::kind::BITVECTOR_NOR;    }
-  | BVXNOR_TOK   { $kind = CVC4::kind::BITVECTOR_XNOR;   }
-  | BVCOMP_TOK   { $kind = CVC4::kind::BITVECTOR_COMP;   }
-  | BVMUL_TOK    { $kind = CVC4::kind::BITVECTOR_MULT;   }
-  | BVADD_TOK    { $kind = CVC4::kind::BITVECTOR_PLUS;   }
-  | BVSUB_TOK    { $kind = CVC4::kind::BITVECTOR_SUB;    }
-  | BVNEG_TOK    { $kind = CVC4::kind::BITVECTOR_NEG;    }
-  | BVUDIV_TOK   { $kind = CVC4::kind::BITVECTOR_UDIV;   }
-  | BVUREM_TOK   { $kind = CVC4::kind::BITVECTOR_UREM;   }
-  | BVSDIV_TOK   { $kind = CVC4::kind::BITVECTOR_SDIV;   }
-  | BVSREM_TOK   { $kind = CVC4::kind::BITVECTOR_SREM;   }
-  | BVSMOD_TOK   { $kind = CVC4::kind::BITVECTOR_SMOD;   }
-  | BVSHL_TOK    { $kind = CVC4::kind::BITVECTOR_SHL;    }
-  | BVLSHR_TOK   { $kind = CVC4::kind::BITVECTOR_LSHR;   }
-  | BVASHR_TOK   { $kind = CVC4::kind::BITVECTOR_ASHR;   }
-  | BVULT_TOK    { $kind = CVC4::kind::BITVECTOR_ULT;    }
-  | BVULE_TOK    { $kind = CVC4::kind::BITVECTOR_ULE;    }
-  | BVUGT_TOK    { $kind = CVC4::kind::BITVECTOR_UGT;    }
-  | BVUGE_TOK    { $kind = CVC4::kind::BITVECTOR_UGE;    }
-  | BVSLT_TOK    { $kind = CVC4::kind::BITVECTOR_SLT;    }
-  | BVSLE_TOK    { $kind = CVC4::kind::BITVECTOR_SLE;    }
-  | BVSGT_TOK    { $kind = CVC4::kind::BITVECTOR_SGT;    }
-  | BVSGE_TOK    { $kind = CVC4::kind::BITVECTOR_SGE;    }
-  // arrays
-  | SELECT_TOK   { $kind = CVC4::kind::SELECT; }
-  | STORE_TOK    { $kind = CVC4::kind::STORE; }
-  // NOTE: Theory operators go here
-  ;
-
-/**
- * Matches an operator.
- */
-parameterizedOperator[CVC4::Expr& op]
-  : functionSymbol[op]
-  | bitVectorOperator[op]
-  ;
-
-/**
- * Matches a bit-vector operator (the ones parametrized by numbers)
- */
-bitVectorOperator[CVC4::Expr& op]
-  : EXTRACT_TOK '[' n1 = NUMERAL_TOK ':' n2 = NUMERAL_TOK ']'
-    { op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1), AntlrInput::tokenToUnsigned($n2))); }
-  | REPEAT_TOK '[' n = NUMERAL_TOK ']'
-    { op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); }
-  | ZERO_EXTEND_TOK '[' n = NUMERAL_TOK ']'
-    { op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); }
-  | SIGN_EXTEND_TOK '[' n = NUMERAL_TOK ']'
-    { op = MK_CONST(BitVectorSignExtend(AntlrInput::tokenToUnsigned($n))); }
-  | ROTATE_LEFT_TOK '[' n = NUMERAL_TOK ']'
-    { op = MK_CONST(BitVectorRotateLeft(AntlrInput::tokenToUnsigned($n))); }
-  | ROTATE_RIGHT_TOK '[' n = NUMERAL_TOK ']'
-    { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); }
-  ;
-
-/**
- * Matches a (possibly undeclared) predicate identifier (returning the string).
- * @param check what kind of check to do with the symbol
- */
-predicateName[std::string& name, CVC4::parser::DeclarationCheck check]
-  :  functionName[name,check]
-  ;
-
-/**
- * Matches a (possibly undeclared) function identifier (returning the string)
- * @param check what kind of check to do with the symbol
- */
-functionName[std::string& name, CVC4::parser::DeclarationCheck check]
-  :  identifier[name,check,SYM_VARIABLE]
-  ;
-
-/**
- * Matches an previously declared function symbol (returning an Expr)
- */
-functionSymbol[CVC4::Expr& fun]
-@declarations {
-	std::string name;
-}
-  : functionName[name,CHECK_DECLARED]
-    { fun = PARSER_STATE->getVariable(name);
-      PARSER_STATE->checkFunctionLike(fun); }
-  ;
-
-/**
- * Matches an attribute name from the input (:attribute_name).
- */
-attribute[std::string& s]
-  : ATTR_IDENTIFIER
-    { s = AntlrInput::tokenText($ATTR_IDENTIFIER); }
-  ;
-
-functionDeclaration[std::unique_ptr<CVC4::Command>* smt_command]
-@declarations {
-  std::string name;
-  std::vector<Type> sorts;
-}
-  : LPAREN_TOK functionName[name,CHECK_UNDECLARED]
-      t = sortSymbol // require at least one sort
-    { sorts.push_back(t); }
-      sortList[sorts] RPAREN_TOK
-    { if( sorts.size() == 1 ) {
-        assert( t == sorts[0] );
-      } else {
-        t = EXPR_MANAGER->mkFunctionType(sorts);
-      }
-      Expr func = PARSER_STATE->mkVar(name, t);
-      smt_command->reset(new DeclareFunctionCommand(name, func, t));
-    }
-  ;
-
-/**
- * Matches the declaration of a predicate and declares it
- */
-predicateDeclaration[std::unique_ptr<CVC4::Command>* smt_command]
-@declarations {
-  std::string name;
-  std::vector<Type> p_sorts;
-}
-  : LPAREN_TOK predicateName[name,CHECK_UNDECLARED] sortList[p_sorts] RPAREN_TOK
-    { Type t;
-      if( p_sorts.empty() ) {
-        t = EXPR_MANAGER->booleanType();
-      } else {
-        t = EXPR_MANAGER->mkPredicateType(p_sorts);
-      }
-      Expr func = PARSER_STATE->mkVar(name, t);
-      smt_command->reset(new DeclareFunctionCommand(name, func, t));
-    }
-  ;
-
-sortDeclaration[std::unique_ptr<CVC4::Command>* smt_command]
-@declarations {
-  std::string name;
-}
-  : sortName[name,CHECK_UNDECLARED]
-    { Debug("parser") << "sort decl: '" << name << "'" << std::endl;
-      Type type = PARSER_STATE->mkSort(name);
-      smt_command->reset(new DeclareTypeCommand(name, 0, type));
-    }
-  ;
-
-/**
- * Matches a sequence of sort symbols and fills them into the given vector.
- */
-sortList[std::vector<CVC4::Type>& sorts]
-  : ( t = sortSymbol { sorts.push_back(t); })*
-  ;
-
-/**
- * Matches the sort symbol, which can be an arbitrary identifier.
- * @param check the check to perform on the name
- */
-sortName[std::string& name, CVC4::parser::DeclarationCheck check]
-  : identifier[name,check,SYM_SORT]
-  ;
-
-sortSymbol returns [CVC4::parser::smt1::myType t]
-@declarations {
-  std::string name;
-}
-  : sortName[name,CHECK_NONE]
-  	{ $t = PARSER_STATE->getSort(name); }
-  | BITVECTOR_TOK '[' NUMERAL_TOK ']' {
-  	$t = EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned($NUMERAL_TOK));
-    }
-  /* attaching 'Array' to '[' allows us to parse regular 'Array' correctly in
-   * e.g. QF_AX, and also 'Array[m:n]' in e.g. QF_AUFBV */
-  | 'Array[' n1=NUMERAL_TOK ':' n2=NUMERAL_TOK ']' {
-        $t = EXPR_MANAGER->mkArrayType(EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned(n1)),
-                                       EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned(n2)));
-    }
-  ;
-
-/**
- * Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'.
- */
-status[ CVC4::BenchmarkStatus& status ]
-  : SAT_TOK       { $status = SMT_SATISFIABLE;    }
-  | UNSAT_TOK     { $status = SMT_UNSATISFIABLE;  }
-  | UNKNOWN_TOK   { $status = SMT_UNKNOWN;        }
-  ;
-
-/**
- * Matches an annotation, which is an attribute name, with an optional user
- * value.
- */
-annotation[std::unique_ptr<CVC4::Command>* smt_command]
-@init {
-  std::string key, value;
-  std::vector<Expr> pats;
-  Expr pat;
-}
-  : PATTERN_ANNOTATION_BEGIN
-    { PARSER_STATE->warning(":pat not supported here; ignored"); }
-    annotatedFormulas[pats,pat] '}'
-  | attribute[key]
-    ( userValue[value]
-      { smt_command->reset(
-            new SetInfoCommand(key.c_str() + 1, SExpr(value))); }
-    | { smt_command->reset(
-            new EmptyCommand(std::string("annotation: ") + key)); }
-    )
-  ;
-
-/**
- * Matches an annotation, which is an attribute name, with an optional user
- * value.
- */
-termAnnotation[CVC4::Expr& expr]
-@init {
-  std::string key, value;
-  std::vector<Expr> pats;
-  Expr pat;
-}
-  : PATTERN_ANNOTATION_BEGIN annotatedFormulas[pats,pat] '}'
-    { if(expr.getKind() == kind::FORALL || expr.getKind() == kind::EXISTS) {
-        pat = MK_EXPR(kind::INST_PATTERN, pats);
-        if(expr.getNumChildren() == 3) {
-          // we have other user patterns attached to the quantifier
-          // already; add this one to the existing list
-          pats = expr[2].getChildren();
-          pats.push_back(pat);
-          expr = MK_EXPR(expr.getKind(), expr[0], expr[1], MK_EXPR(kind::INST_PATTERN_LIST, pats));
-        } else {
-          // this is the only user pattern for the quantifier
-          expr = MK_EXPR(expr.getKind(), expr[0], expr[1], MK_EXPR(kind::INST_PATTERN_LIST, pat));
-        }
-      } else {
-        PARSER_STATE->warning(":pat only supported on quantifiers");
-      }
-    }
-  | ':pat'
-    { PARSER_STATE->warning("expected an instantiation pattern after :pat"); }
-  | attribute[key] userValue[value]?
-    { PARSER_STATE->attributeNotSupported(key); }
-  ;
-
-/**
- * Matches an identifier and sets the string reference parameter id.
- * @param id string to hold the identifier
- * @param check what kinds of check to do on the symbol
- * @param type the intended namespace for the identifier
- */
-identifier[std::string& id,
-		   CVC4::parser::DeclarationCheck check,
-           CVC4::parser::SymbolType type]
-  : IDENTIFIER
-    { id = AntlrInput::tokenText($IDENTIFIER);
-      Debug("parser") << "identifier: " << id
-                      << " check? " << check
-                      << " type? " << type << std::endl;
-      PARSER_STATE->checkDeclaration(id, check, type); }
-  ;
-
-/**
- * Matches a let-bound identifier and sets the string reference parameter id.
- * @param id string to hold the identifier
- * @param check what kinds of check to do on the symbol
- */
-let_identifier[std::string& id,
-    		   CVC4::parser::DeclarationCheck check]
-  : LET_IDENTIFIER
-    { id = AntlrInput::tokenText($LET_IDENTIFIER);
-      Debug("parser") << "let_identifier: " << id
-                      << " check? " << check << std::endl;
-      PARSER_STATE->checkDeclaration(id, check, SYM_VARIABLE); }
-  ;
-
-/**
- * Matches an flet-bound identifier and sets the string reference parameter id.
- * @param id string to hold the identifier
- * @param check what kinds of check to do on the symbol
- */
-flet_identifier[std::string& id,
-    		    CVC4::parser::DeclarationCheck check]
-  : FLET_IDENTIFIER
-    { id = AntlrInput::tokenText($FLET_IDENTIFIER);
-      Debug("parser") << "flet_identifier: " << id
-                      << " check? " << check << std::endl;
-      PARSER_STATE->checkDeclaration(id, check); }
-  ;
-
-// Base SMT-LIB tokens
-ASSUMPTION_TOK  : ':assumption';
-BENCHMARK_TOK   : 'benchmark';
-EXTRAFUNS_TOK   : ':extrafuns';
-EXTRAPREDS_TOK  : ':extrapreds';
-EXTRASORTS_TOK  : ':extrasorts';
-FALSE_TOK       : 'false';
-FLET_TOK        : 'flet';
-FORMULA_TOK     : ':formula';
-ITE_TOK         : 'ite' | 'if_then_else';
-LET_TOK         : 'let';
-LOGIC_TOK       : ':logic';
-LPAREN_TOK      : '(';
-NOTES_TOK       : ':notes';
-RPAREN_TOK      : ')';
-SAT_TOK         : 'sat';
-STATUS_TOK      : ':status';
-THEORY_TOK      : 'theory';
-TRUE_TOK        : 'true';
-UNKNOWN_TOK     : 'unknown';
-UNSAT_TOK       : 'unsat';
-
-// operators (NOTE: theory symbols go here)
-AMPERSAND_TOK     : '&';
-AND_TOK           : 'and';
-AT_TOK            : '@';
-DISTINCT_TOK      : 'distinct';
-DIV_TOK           : '/';
-EQUAL_TOK         : '=';
-EXISTS_TOK        : 'exists';
-FORALL_TOK        : 'forall';
-GREATER_THAN_TOK  : '>';
-IFF_TOK           : 'iff';
-IMPLIES_TOK       : 'implies';
-LESS_THAN_TOK     : '<';
-MINUS_TOK         : '-';
-NOT_TOK           : 'not';
-OR_TOK            : 'or';
-PERCENT_TOK       : '%';
-PIPE_TOK          : '|';
-PLUS_TOK          : '+';
-POUND_TOK         : '#';
-SELECT_TOK        : 'select';
-STAR_TOK          : '*';
-STORE_TOK         : 'store';
-TILDE_TOK         : '~';
-XOR_TOK           : 'xor';
-
-// Bitvector tokens
-BITVECTOR_TOK     : 'BitVec';
-CONCAT_TOK        : 'concat';
-EXTRACT_TOK       : 'extract';
-BVAND_TOK         : 'bvand';
-BVOR_TOK          : 'bvor';
-BVXOR_TOK         : 'bvxor';
-BVNOT_TOK         : 'bvnot';
-BVNAND_TOK        : 'bvnand';
-BVNOR_TOK         : 'bvnor';
-BVXNOR_TOK        : 'bvxnor';
-BVCOMP_TOK        : 'bvcomp';
-BVMUL_TOK         : 'bvmul';
-BVADD_TOK         : 'bvadd';
-BVSUB_TOK         : 'bvsub';
-BVNEG_TOK         : 'bvneg';
-BVUDIV_TOK        : 'bvudiv';
-BVUREM_TOK        : 'bvurem';
-BVSDIV_TOK        : 'bvsdiv';
-BVSREM_TOK        : 'bvsrem';
-BVSMOD_TOK        : 'bvsmod';
-BVSHL_TOK         : 'bvshl';
-BVLSHR_TOK        : 'bvlshr';
-BVASHR_TOK        : 'bvashr';
-BVULT_TOK         : 'bvult';
-BVULE_TOK         : 'bvule';
-BVUGT_TOK         : 'bvugt';
-BVUGE_TOK         : 'bvuge';
-BVSLT_TOK         : 'bvslt';
-BVSLE_TOK         : 'bvsle';
-BVSGT_TOK         : 'bvsgt';
-BVSGE_TOK         : 'bvsge';
-REPEAT_TOK        : 'repeat';
-ZERO_EXTEND_TOK   : 'zero_extend';
-SIGN_EXTEND_TOK   : 'sign_extend';
-ROTATE_LEFT_TOK   : 'rotate_left';
-ROTATE_RIGHT_TOK  : 'rotate_right';
-
-/**
- * Matches a bit-vector constant of the form bv123
- */
-BITVECTOR_BV_CONST
-  : 'bv' DIGIT+
-  ;
-
-/**
- * Matches a bit-vector constant of the form bit(0|1)
- */
-BITVECTOR1_BV_CONST
-  : 'bit0' | 'bit1'
-  ;
-
-
-/**
- * Matches an identifier from the input. An identifier is a sequence of letters,
- * digits and "_", "'", "." symbols, starting with a letter.
- */
-IDENTIFIER
-  :  ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*
-  ;
-
-/**
- * Matches an identifier starting with a colon.
- */
-ATTR_IDENTIFIER
-  :  ':' IDENTIFIER
-  ;
-
-/**
- * Matches an identifier starting with a question mark.
- */
-LET_IDENTIFIER
-  : '?' IDENTIFIER
-  ;
-
-/**
- * Matches an identifier starting with a dollar sign.
- */
-FLET_IDENTIFIER
-  : '$' IDENTIFIER
-  ;
-
-/**
- * Matches the value of user-defined annotations or attributes. The
- * only constraint imposed on a user-defined value is that it start
- * with an open brace and end with closed brace.
- */
-userValue[std::string& s]
-  : USER_VALUE
-    { s = AntlrInput::tokenText($USER_VALUE);
-      assert(*s.begin() == '{');
-      assert(*s.rbegin() == '}');
-      // trim whitespace
-      s.erase(s.begin(), s.begin() + 1);
-      s.erase(s.begin(), std::find_if(s.begin(), s.end(), std::not1(std::ptr_fun<int, int>(std::isspace))));
-      s.erase(s.end() - 1);
-      s.erase(std::find_if(s.rbegin(), s.rend(), std::not1(std::ptr_fun<int, int>(std::isspace))).base(), s.end());
-    }
-  ;
-
-PATTERN_ANNOTATION_BEGIN
-  : ':pat' (' ' | '\t' | '\f' | '\r' | '\n')* '{'
-  ;
-
-USER_VALUE
-  : '{' ('\\{' | '\\}' | ~('{' | '}'))* '}'
-  ;
-
-/**
- * Matches and skips whitespace in the input.
- */
-WHITESPACE
-  : (' ' | '\t' | '\f' | '\r' | '\n')+
-    { SKIP(); }
-  ;
-
-/**
- * Matches a numeral from the input (non-empty sequence of digits).
- */
-NUMERAL_TOK
-  : DIGIT+
-  ;
-
-RATIONAL_TOK
-  : DIGIT+ '.' DIGIT+
-  ;
-
-/**
- * Matches a double quoted string literal. Escaping is supported, and escape
- * character '\' has to be escaped.
- */
-STRING_LITERAL
-  :  '"' (ESCAPE | ~('"'|'\\'))* '"'
-  ;
-
-/**
- * Matches the comments and ignores them
- */
-COMMENT
-  : ';' (~('\n' | '\r'))*
-    { SKIP(); }
-  ;
-
-
-/**
- * Matches any letter ('a'-'z' and 'A'-'Z').
- */
-fragment
-ALPHA
-  :  'a'..'z'
-  |  'A'..'Z'
-  ;
-
-/**
- * Matches the digits (0-9)
- */
-fragment DIGIT :   '0'..'9';
-// fragment NON_ZERO_DIGIT : '1'..'9';
-// fragment NUMERAL_SEQ : '0' | NON_ZERO_DIGIT DIGIT*;
-
-/**
- * Matches an allowed escaped character.
- */
-fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r');
-
diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp
deleted file mode 100644
index 979880f8b..000000000
--- a/src/parser/smt1/smt1.cpp
+++ /dev/null
@@ -1,336 +0,0 @@
-/*********************                                                        */
-/*! \file smt1.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Christopher L. Conway, Morgan Deters, Dejan Jovanovic
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** Definitions of SMT-LIB (v1) constants.
- **/
-
-#include "parser/smt1/smt1.h"
-
-#include "api/cvc4cpp.h"
-#include "expr/type.h"
-#include "parser/parser.h"
-#include "smt/command.h"
-
-namespace CVC4 {
-namespace parser {
-
-std::unordered_map<std::string, Smt1::Logic> Smt1::newLogicMap() {
-  std::unordered_map<std::string, Smt1::Logic> logicMap;
-  logicMap["AUFLIA"] = AUFLIA;
-  logicMap["AUFLIRA"] = AUFLIRA;
-  logicMap["AUFNIRA"] = AUFNIRA;
-  logicMap["LRA"] = LRA;
-  logicMap["QF_AX"] = QF_AX;
-  logicMap["QF_BV"] = QF_BV;
-  logicMap["QF_IDL"] = QF_IDL;
-  logicMap["QF_LIA"] = QF_LIA;
-  logicMap["QF_LRA"] = QF_LRA;
-  logicMap["QF_NIA"] = QF_NIA;
-  logicMap["QF_NRA"] = QF_NRA;
-  logicMap["QF_RDL"] = QF_RDL;
-  logicMap["QF_S"] = QF_S;
-  logicMap["QF_SAT"] = QF_SAT;
-  logicMap["QF_UF"] = QF_UF;
-  logicMap["QF_UFIDL"] = QF_UFIDL;
-  logicMap["QF_UFBV"] = QF_UFBV;
-  logicMap["QF_UFLRA"] = QF_UFLRA;
-  logicMap["QF_UFLIA"] = QF_UFLIA;
-  logicMap["QF_UFLIRA"] = QF_UFLIRA;
-  logicMap["QF_UFNIA"] = QF_UFNIA;
-  logicMap["QF_UFNIRA"] = QF_UFNIRA;
-  logicMap["QF_UFNRA"] = QF_UFNRA;
-  logicMap["QF_ABV"] = QF_ABV;
-  logicMap["QF_AUFBV"] = QF_AUFBV;
-  logicMap["QF_AUFBVLIA"] = QF_AUFBVLIA;
-  logicMap["QF_AUFBVLRA"] = QF_AUFBVLRA;
-  logicMap["QF_UFNIRA"] = QF_UFNIRA;
-  logicMap["QF_AUFLIA"] = QF_AUFLIA;
-  logicMap["QF_AUFLIRA"] = QF_AUFLIRA;
-  logicMap["SAT"] = SAT;
-  logicMap["UFNIA"] = UFNIA;
-  logicMap["UFNIRA"] = UFNIRA;
-  logicMap["UFLRA"] = UFLRA;
-  logicMap["QF_ALL_SUPPORTED"] = QF_ALL_SUPPORTED;
-  logicMap["ALL_SUPPORTED"] = ALL_SUPPORTED;
-  logicMap["QF_ALL"] = QF_ALL_SUPPORTED;
-  logicMap["ALL"] = ALL_SUPPORTED;
-  logicMap["HORN"] = ALL_SUPPORTED;
-  return logicMap;
-}
-
-Smt1::Logic Smt1::toLogic(const std::string& name) {
-  static std::unordered_map<std::string, Smt1::Logic> logicMap = newLogicMap();
-  return logicMap[name];
-}
-
-Smt1::Smt1(api::Solver* solver, Input* input, bool strictMode, bool parseOnly)
-    : Parser(solver, input, strictMode, parseOnly), d_logic(UNSET)
-{
-  // Boolean symbols are always defined
-  addOperator(kind::AND);
-  addOperator(kind::EQUAL);
-  addOperator(kind::IMPLIES);
-  addOperator(kind::ITE);
-  addOperator(kind::NOT);
-  addOperator(kind::OR);
-  addOperator(kind::XOR);
-}
-
-void Smt1::addArithmeticOperators() {
-  addOperator(kind::PLUS);
-  addOperator(kind::MINUS);
-  addOperator(kind::UMINUS);
-  addOperator(kind::MULT);
-  addOperator(kind::LT);
-  addOperator(kind::LEQ);
-  addOperator(kind::GT);
-  addOperator(kind::GEQ);
-}
-
-void Smt1::addTheory(Theory theory) {
-  switch(theory) {
-  case THEORY_ARRAYS:
-  case THEORY_ARRAYS_EX: {
-    Type indexType = mkSort("Index");
-    Type elementType = mkSort("Element");
-    DeclarationSequence* seq = new DeclarationSequence();
-    seq->addCommand(new DeclareTypeCommand("Index", 0, indexType));
-    seq->addCommand(new DeclareTypeCommand("Element", 0, elementType));
-    preemptCommand(seq);
-
-    defineType("Array", getExprManager()->mkArrayType(indexType, elementType));
-
-    addOperator(kind::SELECT);
-    addOperator(kind::STORE);
-    break;
-  }
-
-  case THEORY_BITVECTOR_ARRAYS_EX: {
-    // We don't define the "Array" symbol in this case;
-    // the parser creates the Array[m:n] types on the fly.
-    addOperator(kind::SELECT);
-    addOperator(kind::STORE);
-    break;
-  }
-
-  case THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX: {
-    defineType("Array1", getExprManager()->mkArrayType(getSort("Int"), getSort("Real")));
-    defineType("Array2", getExprManager()->mkArrayType(getSort("Int"), getSort("Array1")));
-    addOperator(kind::SELECT);
-    addOperator(kind::STORE);
-    break;
-  }
-
-  case THEORY_INT_ARRAYS:
-  case THEORY_INT_ARRAYS_EX: {
-    defineType("Array", getExprManager()->mkArrayType(getExprManager()->integerType(), getExprManager()->integerType()));
-    addOperator(kind::SELECT);
-    addOperator(kind::STORE);
-    break;
-  }
-
-  case THEORY_EMPTY: {
-    Type sort = mkSort("U");
-    preemptCommand(new DeclareTypeCommand("U", 0, sort));
-    break;
-  }
-
-  case THEORY_REALS_INTS:
-    defineType("Real", getExprManager()->realType());
-    // falling-through on purpose, to add Ints part of RealsInts
-
-  case THEORY_INTS:
-    defineType("Int", getExprManager()->integerType());
-    addArithmeticOperators();
-    break;
-
-  case THEORY_REALS:
-    defineType("Real", getExprManager()->realType());
-    addArithmeticOperators();
-    break;
-
-  case THEORY_BITVECTORS:
-    break;
-
-  case THEORY_QUANTIFIERS:
-    break;
-
-  default:
-    std::stringstream ss;
-    ss << "internal error: unsupported theory " << theory;
-    throw ParserException(ss.str());
-  }
-}
-
-bool Smt1::logicIsSet() { return d_logic != UNSET; }
-
-void Smt1::setLogic(const std::string& name) {
-  d_logic = toLogic(logicIsForced() ? getForcedLogic() : name);
-
-  switch(d_logic) {
-  case UNSET:
-      throw ParserException("Logic cannot remain UNSET after being set.");
-      break;
-
-    case QF_S:
-      throw ParserException(
-          "Strings theory unsupported in SMT-LIBv1 front-end; try SMT-LIBv2.");
-      break;
-
-    case QF_AX:
-      addTheory(THEORY_ARRAYS_EX);
-      break;
-
-    case QF_IDL:
-    case QF_LIA:
-    case QF_NIA:
-      addTheory(THEORY_INTS);
-      break;
-
-    case QF_RDL:
-    case QF_LRA:
-    case QF_NRA:
-      addTheory(THEORY_REALS);
-      break;
-
-    case QF_SAT:
-      /* no extra symbols needed */
-      break;
-    case SAT:
-      addTheory(THEORY_QUANTIFIERS);
-      break;
-
-    case QF_UFIDL:
-    case QF_UFLIA:
-    case QF_UFNIA:  // nonstandard logic
-      addTheory(THEORY_INTS);
-      addOperator(kind::APPLY_UF);
-      break;
-
-    case QF_UFLRA:
-    case QF_UFNRA:
-      addTheory(THEORY_REALS);
-      addOperator(kind::APPLY_UF);
-      break;
-
-    case QF_UFLIRA:  // nonstandard logic
-    case QF_UFNIRA:  // nonstandard logic
-      addTheory(THEORY_INTS);
-      addTheory(THEORY_REALS);
-      addOperator(kind::APPLY_UF);
-      break;
-
-    case QF_UF:
-      addTheory(THEORY_EMPTY);
-      addOperator(kind::APPLY_UF);
-      break;
-
-    case QF_BV:
-      addTheory(THEORY_BITVECTORS);
-      break;
-
-    case QF_ABV:  // nonstandard logic
-      addTheory(THEORY_BITVECTOR_ARRAYS_EX);
-      addTheory(THEORY_BITVECTORS);
-      break;
-
-    case QF_UFBV:
-      addOperator(kind::APPLY_UF);
-      addTheory(THEORY_BITVECTORS);
-      break;
-
-    case QF_AUFBV:
-      addOperator(kind::APPLY_UF);
-      addTheory(THEORY_BITVECTOR_ARRAYS_EX);
-      addTheory(THEORY_BITVECTORS);
-      break;
-
-    case QF_AUFBVLIA:  // nonstandard logic
-      addOperator(kind::APPLY_UF);
-      addTheory(THEORY_ARRAYS_EX);
-      addTheory(THEORY_BITVECTORS);
-      addTheory(THEORY_INTS);
-      break;
-
-    case QF_AUFBVLRA:  // nonstandard logic
-      addOperator(kind::APPLY_UF);
-      addTheory(THEORY_ARRAYS_EX);
-      addTheory(THEORY_BITVECTORS);
-      addTheory(THEORY_REALS);
-      break;
-
-    case QF_AUFLIA:
-      addTheory(THEORY_INT_ARRAYS_EX);  // nonstandard logic
-      addOperator(kind::APPLY_UF);
-      addTheory(THEORY_INTS);
-      break;
-
-    case QF_AUFLIRA:  // nonstandard logic
-      addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX);
-      addOperator(kind::APPLY_UF);
-      addTheory(THEORY_INTS);
-      addTheory(THEORY_REALS);
-      break;
-
-    case ALL_SUPPORTED:  // nonstandard logic
-      addTheory(THEORY_QUANTIFIERS);
-      /* fall through */
-    case QF_ALL_SUPPORTED:  // nonstandard logic
-      addTheory(THEORY_ARRAYS_EX);
-      addOperator(kind::APPLY_UF);
-      addTheory(THEORY_INTS);
-      addTheory(THEORY_REALS);
-      addTheory(THEORY_BITVECTORS);
-      break;
-
-    case AUFLIA:
-      addOperator(kind::APPLY_UF);
-      addTheory(THEORY_INTS);
-      addTheory(THEORY_INT_ARRAYS_EX);
-      addTheory(THEORY_QUANTIFIERS);
-      break;
-
-    case AUFLIRA:
-    case AUFNIRA:
-      addOperator(kind::APPLY_UF);
-      addTheory(THEORY_INTS);
-      addTheory(THEORY_REALS);
-      addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX);
-      addTheory(THEORY_QUANTIFIERS);
-      break;
-
-    case LRA:
-      addTheory(THEORY_REALS);
-      addTheory(THEORY_QUANTIFIERS);
-      break;
-
-    case UFNIA:
-      addOperator(kind::APPLY_UF);
-      addTheory(THEORY_INTS);
-      addTheory(THEORY_QUANTIFIERS);
-      break;
-    case UFNIRA:
-      addOperator(kind::APPLY_UF);
-      addTheory(THEORY_INTS);
-      addTheory(THEORY_REALS);
-      addTheory(THEORY_QUANTIFIERS);
-      break;
-
-    case UFLRA:
-      addOperator(kind::APPLY_UF);
-      addTheory(THEORY_REALS);
-      addTheory(THEORY_QUANTIFIERS);
-      break;
-  }
-}/* Smt1::setLogic() */
-
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
diff --git a/src/parser/smt1/smt1.h b/src/parser/smt1/smt1.h
deleted file mode 100644
index 32867e692..000000000
--- a/src/parser/smt1/smt1.h
+++ /dev/null
@@ -1,133 +0,0 @@
-/*********************                                                        */
-/*! \file smt1.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Christopher L. Conway, Morgan Deters, Aina Niemetz
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** Definitions of SMT constants.
- **/
-
-#include "cvc4parser_private.h"
-
-#ifndef CVC4__PARSER__SMT1_H
-#define CVC4__PARSER__SMT1_H
-
-#include <string>
-#include <unordered_map>
-
-#include "parser/parser.h"
-
-namespace CVC4 {
-
-class SExpr;
-
-namespace api {
-class Solver;
-}
-
-namespace parser {
-
-class Smt1 : public Parser {
-  friend class ParserBuilder;
-
-public:
- enum Logic {
-   UNSET = 0,  // This indicates that the logic has not been set.
-   AUFLIA,     // +p and -p?
-   AUFLIRA,
-   AUFNIRA,
-   LRA,
-   QF_ABV,
-   QF_AUFBV,
-   QF_AUFBVLIA,
-   QF_AUFBVLRA,
-   QF_AUFLIA,
-   QF_AUFLIRA,
-   QF_AX,
-   QF_BV,
-   QF_IDL,
-   QF_LIA,
-   QF_LRA,
-   QF_NIA,
-   QF_NRA,
-   QF_RDL,
-   QF_S,  // nonstandard (for string theory)
-   QF_SAT,
-   QF_UF,
-   QF_UFIDL,
-   QF_UFBV,
-   QF_UFLIA,
-   QF_UFNIA,  // nonstandard
-   QF_UFLRA,
-   QF_UFLIRA,  // nonstandard
-   QF_UFNIRA,  // nonstandard
-   QF_UFNRA,
-   SAT,
-   UFLRA,
-   UFNIRA,  // nonstandard
-   UFNIA,
-   QF_ALL_SUPPORTED,  // nonstandard
-   ALL_SUPPORTED      // nonstandard
- };
-
- enum Theory {
-   THEORY_ARRAYS,
-   THEORY_ARRAYS_EX,
-   THEORY_BITVECTORS,
-   THEORY_BITVECTORS_32,
-   THEORY_BITVECTOR_ARRAYS_EX,
-   THEORY_EMPTY,
-   THEORY_INTS,
-   THEORY_INT_ARRAYS,
-   THEORY_INT_ARRAYS_EX,
-   THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX,
-   THEORY_REALS,
-   THEORY_REALS_INTS,
-   THEORY_STRINGS,
-   THEORY_QUANTIFIERS,
-   THEORY_CARDINALITY_CONSTRAINT
- };
-
-private:
-  Logic d_logic;
-
-protected:
- Smt1(api::Solver* solver,
-      Input* input,
-      bool strictMode = false,
-      bool parseOnly = false);
-
-public:
-  /**
-   * Add theory symbols to the parser state.
-   *
-   * @param theory the theory to open (e.g., Core, Ints)
-   */
-  void addTheory(Theory theory);
-
-  bool logicIsSet() override;
-
-  /**
-   * Sets the logic for the current benchmark. Declares any logic and theory symbols.
-   *
-   * @param name the name of the logic (e.g., QF_UF, AUFLIA)
-   */
-  void setLogic(const std::string& name);
-
-  static Logic toLogic(const std::string& name);
-
-private:
-
-  void addArithmeticOperators();
-  static std::unordered_map<std::string, Logic> newLogicMap();
-};/* class Smt1 */
-
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
-
-#endif /* CVC4__PARSER__SMT1_H */
diff --git a/src/parser/smt1/smt1_input.cpp b/src/parser/smt1/smt1_input.cpp
deleted file mode 100644
index b8f476687..000000000
--- a/src/parser/smt1/smt1_input.cpp
+++ /dev/null
@@ -1,70 +0,0 @@
-/*********************                                                        */
-/*! \file smt1_input.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Christopher L. Conway
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  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 "parser/smt1/smt1_input.h"
-
-#include <antlr3.h>
-
-#include "expr/expr_manager.h"
-#include "parser/input.h"
-#include "parser/parser.h"
-#include "parser/parser_exception.h"
-#include "parser/smt1/Smt1Lexer.h"
-#include "parser/smt1/Smt1Parser.h"
-
-namespace CVC4 {
-namespace parser {
-
-/* Use lookahead=2 */
-Smt1Input::Smt1Input(AntlrInputStream& inputStream) :
-  AntlrInput(inputStream, 2) {
-  pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
-  assert( input != NULL );
-
-  d_pSmt1Lexer = Smt1LexerNew(input);
-  if( d_pSmt1Lexer == NULL ) {
-    throw ParserException("Failed to create SMT lexer.");
-  }
-
-  setAntlr3Lexer( d_pSmt1Lexer->pLexer );
-
-  pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
-  assert( tokenStream != NULL );
-
-  d_pSmt1Parser = Smt1ParserNew(tokenStream);
-  if( d_pSmt1Parser == NULL ) {
-    throw ParserException("Failed to create SMT parser.");
-  }
-
-  setAntlr3Parser(d_pSmt1Parser->pParser);
-}
-
-
-Smt1Input::~Smt1Input() {
-  d_pSmt1Lexer->free(d_pSmt1Lexer);
-  d_pSmt1Parser->free(d_pSmt1Parser);
-}
-
-Command* Smt1Input::parseCommand() {
-  return d_pSmt1Parser->parseCommand(d_pSmt1Parser);
-}
-
-Expr Smt1Input::parseExpr() {
-  return d_pSmt1Parser->parseExpr(d_pSmt1Parser);
-}
-
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
diff --git a/src/parser/smt1/smt1_input.h b/src/parser/smt1/smt1_input.h
deleted file mode 100644
index fcdc63ee2..000000000
--- a/src/parser/smt1/smt1_input.h
+++ /dev/null
@@ -1,85 +0,0 @@
-/*********************                                                        */
-/*! \file smt1_input.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Christopher L. Conway, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  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__SMT1_INPUT_H
-#define CVC4__PARSER__SMT1_INPUT_H
-
-#include "parser/antlr_input.h"
-#include "parser/smt1/Smt1Lexer.h"
-#include "parser/smt1/Smt1Parser.h"
-
-// extern void Smt1ParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser);
-
-namespace CVC4 {
-
-class Command;
-class Expr;
-class ExprManager;
-
-namespace parser {
-
-class Smt1Input : public AntlrInput {
-
-  /** The ANTLR3 SMT lexer for the input. */
-  pSmt1Lexer d_pSmt1Lexer;
-
-  /** The ANTLR3 CVC parser for the input. */
-  pSmt1Parser d_pSmt1Parser;
-
-public:
-
-  /**
-   * Create an input.
-   *
-   * @param inputStream the input stream to use
-   */
-  Smt1Input(AntlrInputStream& inputStream);
-
-  /** Destructor. Frees the lexer and the parser. */
-  virtual ~Smt1Input();
-
- 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() override;
-
-  /**
-   * 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() override;
-
- private:
-  /**
-   * Initialize the class. Called from the constructors once the input
-   * stream is initialized.
-   */
-  void init();
-
-};/* class Smt1Input */
-
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
-
-#endif /* CVC4__PARSER__SMT1_INPUT_H */
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 1d07969ff..c6b7de42c 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -542,8 +542,8 @@ command [std::unique_ptr<CVC4::Command>* cmd]
     { std::string id = AntlrInput::tokenText($SIMPLE_SYMBOL);
       if(id == "benchmark") {
         PARSER_STATE->parseError(
-            "In SMT-LIBv2 mode, but got something that looks like SMT-LIBv1. "
-            "Use --lang smt1 for SMT-LIBv1.");
+            "In SMT-LIBv2 mode, but got something that looks like SMT-LIBv1, "
+            "which is not supported anymore.");
       } else {
         PARSER_STATE->parseError("expected SMT-LIBv2 command, got `" + id +
                                  "'.");
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 436e15d32..1ca9ee2c8 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -19,7 +19,6 @@
 #include "options/options.h"
 #include "parser/antlr_input.h"
 #include "parser/parser.h"
-#include "parser/smt1/smt1.h"
 #include "parser/smt2/smt2_input.h"
 #include "printer/sygus_print_callback.h"
 #include "util/bitvector.h"
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 7c7f290a5..83628d215 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -27,7 +27,6 @@
 
 #include "api/cvc4cpp.h"
 #include "parser/parser.h"
-#include "parser/smt1/smt1.h"
 #include "parser/smt2/parse_op.h"
 #include "smt/command.h"
 #include "theory/logic_info.h"