GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/options/language.h Lines: 16 37 43.2 %
Date: 2021-03-23 Branches: 4 13 30.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file language.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Andrew Reynolds, Francois Bobot
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Definition of input and output languages
13
 **
14
 ** Definition of input and output languages.
15
 **/
16
17
#include "cvc4_public.h"
18
19
#ifndef CVC4__LANGUAGE_H
20
#define CVC4__LANGUAGE_H
21
22
#include <ostream>
23
#include <string>
24
25
#include "cvc4_export.h"
26
27
namespace CVC4 {
28
namespace language {
29
30
namespace input {
31
32
enum CVC4_EXPORT Language
33
{
34
  // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
35
36
  /** Auto-detect the language */
37
  LANG_AUTO = -1,
38
39
  // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,9]
40
  // AND SHOULD CORRESPOND IN PLACEMENT WITH OUTPUTLANGUAGE
41
  //
42
  // EVEN IF A LANGUAGE ISN'T CURRENTLY SUPPORTED AS AN INPUT OR
43
  // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE,
44
  // INCLUDE IT HERE
45
46
  /** The SMTLIB v2.6 input language, with support for the strings standard */
47
  LANG_SMTLIB_V2_6 = 0,
48
  /** Backward-compatibility for enumeration naming */
49
  LANG_SMTLIB_V2 = LANG_SMTLIB_V2_6,
50
  /** The TPTP input language */
51
  LANG_TPTP,
52
  /** The CVC4 input language */
53
  LANG_CVC4,
54
  /** The SyGuS input language version 2.0 */
55
  LANG_SYGUS_V2,
56
57
  // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10
58
  // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES
59
60
  /** LANG_MAX is > any valid InputLanguage id */
61
  LANG_MAX
62
}; /* enum Language */
63
64
inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_EXPORT;
65
29
inline std::ostream& operator<<(std::ostream& out, Language lang) {
66
29
  switch(lang) {
67
  case LANG_AUTO:
68
    out << "LANG_AUTO";
69
    break;
70
18
  case LANG_SMTLIB_V2_6:
71
18
    out << "LANG_SMTLIB_V2_6";
72
18
    break;
73
  case LANG_TPTP:
74
    out << "LANG_TPTP";
75
    break;
76
11
  case LANG_CVC4:
77
11
    out << "LANG_CVC4";
78
11
    break;
79
  case LANG_SYGUS_V2: out << "LANG_SYGUS_V2"; break;
80
  default:
81
    out << "undefined_input_language";
82
  }
83
29
  return out;
84
}
85
86
}/* CVC4::language::input namespace */
87
88
namespace output {
89
90
enum CVC4_EXPORT Language
91
{
92
  // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
93
94
  /** Match the output language to the input language */
95
  LANG_AUTO = -1,
96
97
  // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,9]
98
  // AND SHOULD CORRESPOND IN PLACEMENT WITH INPUTLANGUAGE
99
  //
100
  // EVEN IF A LANGUAGE ISN'T CURRENTLY SUPPORTED AS AN INPUT OR
101
  // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE,
102
  // INCLUDE IT HERE
103
104
  /** The SMTLIB v2.6 output language, with support for the strings standard */
105
  LANG_SMTLIB_V2_6 = input::LANG_SMTLIB_V2_6,
106
  /** Backward-compatibility for enumeration naming */
107
  LANG_SMTLIB_V2 = input::LANG_SMTLIB_V2,
108
  /** The TPTP output language */
109
  LANG_TPTP = input::LANG_TPTP,
110
  /** The CVC4 output language */
111
  LANG_CVC4 = input::LANG_CVC4,
112
  /** The sygus output language version 2.0 */
113
  LANG_SYGUS_V2 = input::LANG_SYGUS_V2,
114
115
  // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10
116
  // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES
117
118
  /** The AST output language */
119
  LANG_AST = 10,
120
  /** The CVC3-compatibility output language */
121
  LANG_CVC3,
122
123
  /** LANG_MAX is > any valid OutputLanguage id */
124
  LANG_MAX
125
}; /* enum Language */
126
127
inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_EXPORT;
128
12
inline std::ostream& operator<<(std::ostream& out, Language lang) {
129
12
  switch(lang) {
130
8
  case LANG_SMTLIB_V2_6: out << "LANG_SMTLIB_V2_6"; break;
131
  case LANG_TPTP:
132
    out << "LANG_TPTP";
133
    break;
134
4
  case LANG_CVC4:
135
4
    out << "LANG_CVC4";
136
4
    break;
137
  case LANG_SYGUS_V2: out << "LANG_SYGUS_V2"; break;
138
  case LANG_AST:
139
    out << "LANG_AST";
140
    break;
141
  case LANG_CVC3:
142
    out << "LANG_CVC3";
143
    break;
144
  default:
145
    out << "undefined_output_language";
146
  }
147
12
  return out;
148
}
149
150
}/* CVC4::language::output namespace */
151
152
}/* CVC4::language namespace */
153
154
typedef language::input::Language InputLanguage;
155
typedef language::output::Language OutputLanguage;
156
157
namespace language {
158
159
/** Is the language a variant of the smtlib version 2 language? */
160
bool isInputLang_smt2(InputLanguage lang) CVC4_EXPORT;
161
bool isOutputLang_smt2(OutputLanguage lang) CVC4_EXPORT;
162
163
/**
164
  * Is the language smtlib 2.6 or above? If exact=true, then this method returns
165
  * false if the input language is not exactly SMT-LIB 2.6.
166
  */
167
bool isInputLang_smt2_6(InputLanguage lang, bool exact = false) CVC4_EXPORT;
168
bool isOutputLang_smt2_6(OutputLanguage lang, bool exact = false) CVC4_EXPORT;
169
170
/** Is the language a variant of the SyGuS input language? */
171
bool isInputLangSygus(InputLanguage lang) CVC4_EXPORT;
172
bool isOutputLangSygus(OutputLanguage lang) CVC4_EXPORT;
173
174
InputLanguage toInputLanguage(OutputLanguage language) CVC4_EXPORT;
175
OutputLanguage toOutputLanguage(InputLanguage language) CVC4_EXPORT;
176
InputLanguage toInputLanguage(std::string language) CVC4_EXPORT;
177
OutputLanguage toOutputLanguage(std::string language) CVC4_EXPORT;
178
179
}/* CVC4::language namespace */
180
}/* CVC4 namespace */
181
182
#endif /* CVC4__LANGUAGE_H */