Remove (dummy) SMT1 printer (#1854)

diff --git a/src/Makefile.am b/src/Makefile.am
index e9fcb5913c67e2006abd2cdb8b8284694cf18dd4..6cb179b1dfdcd711dc32010d79e5f7e86ded9a60 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -92,8 +92,6 @@ libcvc4_la_SOURCES = \
        printer/ast/ast_printer.h \
        printer/cvc/cvc_printer.cpp \
        printer/cvc/cvc_printer.h \
-       printer/smt1/smt1_printer.cpp \
-       printer/smt1/smt1_printer.h \
        printer/smt2/smt2_printer.cpp \
        printer/smt2/smt2_printer.h \
        printer/tptp/tptp_printer.cpp \

diff --git a/src/options/language.cpp b/src/options/language.cpp
index f76893866475629cfe71aa545113b1bf9f37f255..4c224b95d4151028717f30447929b9b3368cc6e9 100644 (file)
--- a/src/options/language.cpp
+++ b/src/options/language.cpp
@@ -94,6 +94,7 @@ InputLanguage toInputLanguage(OutputLanguage language) {
 OutputLanguage toOutputLanguage(InputLanguage language) {
   switch(language) {
   case input::LANG_SMTLIB_V1:
+    return OutputLanguage(output::LANG_SMTLIB_V2_0);
   case input::LANG_SMTLIB_V2_0:
   case input::LANG_SMTLIB_V2_5:
   case input::LANG_SMTLIB_V2_6:
@@ -127,9 +128,6 @@ OutputLanguage toOutputLanguage(std::string language) {
     return output::LANG_CVC4;
   } else if(language == "cvc3" || language == "LANG_CVC3") {
     return output::LANG_CVC3;
-  } else if(language == "smtlib1" || language == "smt1" ||
-            language == "LANG_SMTLIB_V1") {
-    return output::LANG_SMTLIB_V1;
   } else if(language == "smtlib" || language == "smt" ||
             language == "smtlib2" || language == "smt2" ||
             language == "smtlib2.0" || language == "smt2.0" ||

diff --git a/src/options/language.h b/src/options/language.h
index 2b2e7d5da6aab639f8fd486fbee2c31e398875ec..c573c4aef1c0939ae3d584d12a048fbd228f5910 100644 (file)
--- a/src/options/language.h
+++ b/src/options/language.h
@@ -127,7 +127,7 @@ enum CVC4_PUBLIC Language
   // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE,
   // INCLUDE IT HERE
 
-  /** The SMTLIB v1 output language */
+  /** The SMTLIB v1 output language (unsupported) */
   LANG_SMTLIB_V1 = input::LANG_SMTLIB_V1,
   /** The SMTLIB v2.0 output language */
   LANG_SMTLIB_V2_0 = input::LANG_SMTLIB_V2_0,

diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 4fdd477b9aef9eb90064689ef116ffef2f222995..46f9e074133bfa53aac4c1fcac28122814124046 100644 (file)
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -441,7 +441,6 @@ Languages currently supported as arguments to the --output-lang option:\n\
   auto                           match output language to input language\n\
   cvc4 | presentation | pl       CVC4 presentation language\n\
   cvc3                           CVC3 presentation language\n\
-  smt1 | smtlib1                 SMT-LIB format 1.2\n\
   smt | smtlib | smt2 |\n\
   smt2.0 | smtlib2.0 | smtlib2   SMT-LIB format 2.0\n\
   smt2.5 | smtlib2.5             SMT-LIB format 2.5\n\

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index f9486f017d478aee4e2062ee55caeb4a3ac237c7..43964972536ad37be8910237dac3ac7a9521ad3f 100644 (file)
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -21,7 +21,6 @@
 #include "options/language.h"
 #include "printer/ast/ast_printer.h"
 #include "printer/cvc/cvc_printer.h"
-#include "printer/smt1/smt1_printer.h"
 #include "printer/smt2/smt2_printer.h"
 #include "printer/tptp/tptp_printer.h"
 
@@ -36,9 +35,6 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang)
   using namespace CVC4::language::output;
 
   switch(lang) {
-  case LANG_SMTLIB_V1: // TODO the printer
-    return unique_ptr<Printer>(new printer::smt1::Smt1Printer());
-
   case LANG_SMTLIB_V2_0:
     return unique_ptr<Printer>(
         new printer::smt2::Smt2Printer(printer::smt2::smt2_0_variant));

diff --git a/src/printer/smt1/smt1_printer.cpp b/src/printer/smt1/smt1_printer.cpp
deleted file mode 100644 (file)
index ac3c2f9..0000000
--- a/src/printer/smt1/smt1_printer.cpp
+++ /dev/null
@@ -1,69 +0,0 @@
-/*********************                                                        */
-/*! \file smt1_printer.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 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 The pretty-printer interface for the SMT output language
- **
- ** The pretty-printer interface for the SMT output language.
- **/
-#include "printer/smt1/smt1_printer.h"
-
-#include <iostream>
-#include <string>
-#include <typeinfo>
-#include <vector>
-
-#include "expr/expr.h" // for ExprSetDepth etc..
-#include "expr/node_manager.h" // for VarNameAttr
-#include "options/language.h" // for LANG_AST
-#include "smt/command.h"
-
-using namespace std;
-
-namespace CVC4 {
-namespace printer {
-namespace smt1 {
-
-void Smt1Printer::toStream(
-    std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const
-{
-  n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
-}/* Smt1Printer::toStream() */
-
-void Smt1Printer::toStream(std::ostream& out,
-                           const Command* c,
-                           int toDepth,
-                           bool types,
-                           size_t dag) const
-{
-  c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
-}/* Smt1Printer::toStream() */
-
-void Smt1Printer::toStream(std::ostream& out, const CommandStatus* s) const
-{
-  s->toStream(out, language::output::LANG_SMTLIB_V2_5);
-}/* Smt1Printer::toStream() */
-
-void Smt1Printer::toStream(std::ostream& out, const Model& m) const
-{
-  Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, m);
-}
-
-void Smt1Printer::toStream(std::ostream& out,
-                           const Model& m,
-                           const Command* c) const
-{
-  // shouldn't be called; only the non-Command* version above should be
-  Unreachable();
-}
-
-}/* CVC4::printer::smt1 namespace */
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */

diff --git a/src/printer/smt1/smt1_printer.h b/src/printer/smt1/smt1_printer.h
deleted file mode 100644 (file)
index 560393b..0000000
--- a/src/printer/smt1/smt1_printer.h
+++ /dev/null
@@ -1,57 +0,0 @@
-/*********************                                                        */
-/*! \file smt1_printer.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 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 The pretty-printer interface for the SMT output language
- **
- ** The pretty-printer interface for the SMT output language.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__PRINTER__SMT1_PRINTER_H
-#define __CVC4__PRINTER__SMT1_PRINTER_H
-
-#include <iostream>
-
-#include "printer/printer.h"
-
-namespace CVC4 {
-namespace printer {
-namespace smt1 {
-
-class Smt1Printer : public CVC4::Printer {
- public:
-  using CVC4::Printer::toStream;
-  void toStream(std::ostream& out,
-                TNode n,
-                int toDepth,
-                bool types,
-                size_t dag) const override;
-  void toStream(std::ostream& out,
-                const Command* c,
-                int toDepth,
-                bool types,
-                size_t dag) const override;
-  void toStream(std::ostream& out, const CommandStatus* s) const override;
-  void toStream(std::ostream& out, const Model& m) const override;
-
- private:
-  void toStream(std::ostream& out,
-                const Model& m,
-                const Command* c) const override;
-  void toStream(std::ostream& out, const SExpr& sexpr) const;
-};/* class Smt1Printer */
-
-}/* CVC4::printer::smt1 namespace */
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PRINTER__SMT1_PRINTER_H */