summaryrefslogtreecommitdiff
path: root/src/options/language.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/options/language.h')
-rw-r--r--src/options/language.h18
1 files changed, 1 insertions, 17 deletions
diff --git a/src/options/language.h b/src/options/language.h
index d0bdc6e77..0a0f63ca6 100644
--- a/src/options/language.h
+++ b/src/options/language.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Andrew Reynolds, Francois Bobot
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
@@ -56,10 +56,6 @@ enum CVC4_PUBLIC Language
LANG_TPTP,
/** The CVC4 input language */
LANG_CVC4,
- /** The Z3-str input language */
- LANG_Z3STR,
- /** The SyGuS input language version 1.0 */
- LANG_SYGUS_V1,
/** The SyGuS input language version 2.0 */
LANG_SYGUS_V2,
@@ -91,10 +87,6 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
case LANG_CVC4:
out << "LANG_CVC4";
break;
- case LANG_Z3STR:
- out << "LANG_Z3STR";
- break;
- case LANG_SYGUS_V1: out << "LANG_SYGUS_V1"; break;
case LANG_SYGUS_V2: out << "LANG_SYGUS_V2"; break;
default:
out << "undefined_input_language";
@@ -132,10 +124,6 @@ enum CVC4_PUBLIC Language
LANG_TPTP = input::LANG_TPTP,
/** The CVC4 output language */
LANG_CVC4 = input::LANG_CVC4,
- /** The Z3-str output language */
- LANG_Z3STR = input::LANG_Z3STR,
- /** The sygus output language version 1.0 */
- LANG_SYGUS_V1 = input::LANG_SYGUS_V1,
/** The sygus output language version 2.0 */
LANG_SYGUS_V2 = input::LANG_SYGUS_V2,
@@ -167,10 +155,6 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
case LANG_CVC4:
out << "LANG_CVC4";
break;
- case LANG_Z3STR:
- out << "LANG_Z3STR";
- break;
- case LANG_SYGUS_V1: out << "LANG_SYGUS_V1"; break;
case LANG_SYGUS_V2: out << "LANG_SYGUS_V2"; break;
case LANG_AST:
out << "LANG_AST";
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback