GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/options/language.cpp Lines: 45 71 63.4 %
Date: 2021-03-23 Branches: 71 164 43.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file language.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Andrew Reynolds, Mathias Preiner
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 "options/language.h"
18
19
#include <sstream>
20
21
#include "base/exception.h"
22
#include "options/option_exception.h"
23
24
namespace CVC4 {
25
namespace language {
26
27
/** define the end points of smt2 languages */
28
namespace input {
29
Language LANG_SMTLIB_V2_START = LANG_SMTLIB_V2_6;
30
Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6;
31
}
32
namespace output {
33
Language LANG_SMTLIB_V2_START = LANG_SMTLIB_V2_6;
34
Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6;
35
}
36
37
9966
bool isInputLang_smt2(InputLanguage lang)
38
{
39
9966
  return lang >= input::LANG_SMTLIB_V2_START
40
9966
         && lang <= input::LANG_SMTLIB_V2_END;
41
}
42
43
13653
bool isOutputLang_smt2(OutputLanguage lang)
44
{
45
13653
  return lang >= output::LANG_SMTLIB_V2_START
46
13653
         && lang <= output::LANG_SMTLIB_V2_END;
47
}
48
49
562465
bool isInputLang_smt2_6(InputLanguage lang, bool exact)
50
{
51
1124930
  return exact ? lang == input::LANG_SMTLIB_V2_6
52
               : (lang >= input::LANG_SMTLIB_V2_6
53
1124930
                  && lang <= input::LANG_SMTLIB_V2_END);
54
}
55
56
bool isOutputLang_smt2_6(OutputLanguage lang, bool exact)
57
{
58
  return exact ? lang == output::LANG_SMTLIB_V2_6
59
               : (lang >= output::LANG_SMTLIB_V2_6
60
                  && lang <= output::LANG_SMTLIB_V2_END);
61
}
62
63
88659
bool isInputLangSygus(InputLanguage lang)
64
{
65
88659
  return lang == input::LANG_SYGUS_V2;
66
}
67
68
bool isOutputLangSygus(OutputLanguage lang)
69
{
70
  return lang == output::LANG_SYGUS_V2;
71
}
72
73
InputLanguage toInputLanguage(OutputLanguage language) {
74
  switch(language) {
75
  case output::LANG_SMTLIB_V2_6:
76
  case output::LANG_TPTP:
77
  case output::LANG_CVC4:
78
  case output::LANG_SYGUS_V2:
79
    // these entries directly correspond (by design)
80
    return InputLanguage(int(language));
81
82
  default: {
83
    std::stringstream ss;
84
    ss << "Cannot map output language `" << language
85
       << "' to an input language.";
86
    throw CVC4::Exception(ss.str());
87
  }
88
  }/* switch(language) */
89
}/* toInputLanguage() */
90
91
6138
OutputLanguage toOutputLanguage(InputLanguage language) {
92
6138
  switch(language) {
93
6138
  case input::LANG_SMTLIB_V2_6:
94
  case input::LANG_TPTP:
95
  case input::LANG_CVC4:
96
  case input::LANG_SYGUS_V2:
97
    // these entries directly correspond (by design)
98
6138
    return OutputLanguage(int(language));
99
100
  default:
101
    // Revert to the default (AST) language.
102
    //
103
    // We used to throw an exception here, but that's not quite right.
104
    // We often call this while constructing exceptions, for one, and
105
    // it's better to output SOMETHING related to the original
106
    // exception rather than mask it with another exception.  Also,
107
    // the input language isn't always defined---e.g. during the
108
    // initial phase of the main CVC4 driver while it determines which
109
    // language is appropriate, and during unit tests.  Also, when
110
    // users are writing their own code against the library.
111
    return output::LANG_AST;
112
  }/* switch(language) */
113
}/* toOutputLanguage() */
114
115
86
OutputLanguage toOutputLanguage(std::string language) {
116
328
  if(language == "cvc4" || language == "pl" ||
117
320
     language == "presentation" || language == "native" ||
118
78
     language == "LANG_CVC4") {
119
8
    return output::LANG_CVC4;
120
78
  } else if(language == "cvc3" || language == "LANG_CVC3") {
121
    return output::LANG_CVC3;
122
  }
123
234
  else if (language == "smtlib" || language == "smt" || language == "smtlib2"
124
78
           || language == "smt2" || language == "smtlib2.6"
125
62
           || language == "smt2.6" || language == "LANG_SMTLIB_V2_6"
126
140
           || language == "LANG_SMTLIB_V2")
127
  {
128
16
    return output::LANG_SMTLIB_V2_6;
129
62
  } else if(language == "tptp" || language == "LANG_TPTP") {
130
    return output::LANG_TPTP;
131
  }
132
186
  else if (language == "sygus" || language == "LANG_SYGUS"
133
124
           || language == "sygus2" || language == "LANG_SYGUS_V2")
134
  {
135
    return output::LANG_SYGUS_V2;
136
  }
137
62
  else if (language == "ast" || language == "LANG_AST")
138
  {
139
62
    return output::LANG_AST;
140
  }
141
  else if (language == "auto" || language == "LANG_AUTO")
142
  {
143
    return output::LANG_AUTO;
144
  }
145
146
  throw OptionException(std::string("unknown output language `" + language + "'"));
147
}/* toOutputLanguage() */
148
149
653
InputLanguage toInputLanguage(std::string language) {
150
2590
  if(language == "cvc4" || language == "pl" ||
151
2579
     language == "presentation" || language == "native" ||
152
642
     language == "LANG_CVC4") {
153
11
    return input::LANG_CVC4;
154
2568
  } else if(language == "smtlib" || language == "smt" ||
155
1689
            language == "smtlib2" || language == "smt2" ||
156
1171
            language == "smtlib2.6" || language == "smt2.6" ||
157
1364
            language == "LANG_SMTLIB_V2_6" || language == "LANG_SMTLIB_V2") {
158
281
    return input::LANG_SMTLIB_V2_6;
159
361
  } else if(language == "tptp" || language == "LANG_TPTP") {
160
    return input::LANG_TPTP;
161
1083
  } else if(language == "sygus" || language == "sygus2" ||
162
361
          language == "LANG_SYGUS" || language == "LANG_SYGUS_V2") {
163
361
    return input::LANG_SYGUS_V2;
164
  }
165
  else if (language == "auto" || language == "LANG_AUTO")
166
  {
167
    return input::LANG_AUTO;
168
  }
169
170
  throw OptionException(std::string("unknown input language `" + language + "'"));
171
}/* toInputLanguage() */
172
173
}/* CVC4::language namespace */
174
}/* CVC4 namespace */