Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/options/language.cpp	Lines:	42	67	62.7 %
Date:	2021-08-14	Branches:	70	158	44.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Andrew Reynolds, Mathias Preiner
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 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.
 * ****************************************************************************
 *
 * Definition of input and output languages.
 */

#include "options/language.h"

#include <sstream>

#include "base/exception.h"
#include "options/option_exception.h"

namespace cvc5 {
namespace language {

/** define the end points of smt2 languages */
namespace input {
Language LANG_SMTLIB_V2_START = LANG_SMTLIB_V2_6;
Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6;
}
namespace output {
Language LANG_SMTLIB_V2_START = LANG_SMTLIB_V2_6;
Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6;
}

bool isInputLang_smt2(InputLanguage lang)
{
  return lang >= input::LANG_SMTLIB_V2_START
         && lang <= input::LANG_SMTLIB_V2_END;
}

bool isOutputLang_smt2(OutputLanguage lang)
{
  return lang >= output::LANG_SMTLIB_V2_START
         && lang <= output::LANG_SMTLIB_V2_END;
}

bool isInputLang_smt2_6(InputLanguage lang, bool exact)
{
  return exact ? lang == input::LANG_SMTLIB_V2_6
               : (lang >= input::LANG_SMTLIB_V2_6
                  && lang <= input::LANG_SMTLIB_V2_END);
}

bool isOutputLang_smt2_6(OutputLanguage lang, bool exact)
{
  return exact ? lang == output::LANG_SMTLIB_V2_6
               : (lang >= output::LANG_SMTLIB_V2_6
                  && lang <= output::LANG_SMTLIB_V2_END);
}

bool isInputLangSygus(InputLanguage lang)
{
  return lang == input::LANG_SYGUS_V2;
}

bool isOutputLangSygus(OutputLanguage lang)
{
  return lang == output::LANG_SYGUS_V2;
}

InputLanguage toInputLanguage(OutputLanguage language) {
  switch(language) {
  case output::LANG_SMTLIB_V2_6:
  case output::LANG_TPTP:
  case output::LANG_CVC:
  case output::LANG_SYGUS_V2:
    // these entries directly correspond (by design)
    return InputLanguage(int(language));

  default: {
    std::stringstream ss;
    ss << "Cannot map output language `" << language
       << "' to an input language.";
    throw cvc5::Exception(ss.str());
  }
  }/* switch(language) */
}/* toInputLanguage() */

OutputLanguage toOutputLanguage(InputLanguage language) {
  switch(language) {
  case input::LANG_SMTLIB_V2_6:
  case input::LANG_TPTP:
  case input::LANG_CVC:
  case input::LANG_SYGUS_V2:
    // these entries directly correspond (by design)
    return OutputLanguage(int(language));

  default:
    // Revert to the default (AST) language.
    //
    // We used to throw an exception here, but that's not quite right.
    // We often call this while constructing exceptions, for one, and
    // it's better to output SOMETHING related to the original
    // exception rather than mask it with another exception.  Also,
    // the input language isn't always defined---e.g. during the
    // initial phase of the main cvc5 driver while it determines which
    // language is appropriate, and during unit tests.  Also, when
    // users are writing their own code against the library.
    return output::LANG_AST;
  }/* switch(language) */
}/* toOutputLanguage() */

OutputLanguage toOutputLanguage(std::string language)
{
  if (language == "cvc" || language == "pl" || language == "presentation"
      || language == "native" || language == "LANG_CVC")
  {
    return output::LANG_CVC;
  }
  else if (language == "smtlib" || language == "smt" || language == "smtlib2"
           || language == "smt2" || language == "smtlib2.6"
           || language == "smt2.6" || language == "LANG_SMTLIB_V2_6"
           || language == "LANG_SMTLIB_V2")
  {
    return output::LANG_SMTLIB_V2_6;
  }
  else if (language == "tptp" || language == "LANG_TPTP")
  {
    return output::LANG_TPTP;
  }
  else if (language == "sygus" || language == "LANG_SYGUS"
           || language == "sygus2" || language == "LANG_SYGUS_V2")
  {
    return output::LANG_SYGUS_V2;
  }
  else if (language == "ast" || language == "LANG_AST")
  {
    return output::LANG_AST;
  }
  else if (language == "auto" || language == "LANG_AUTO")
  {
    return output::LANG_AUTO;
  }

  throw OptionException(
      std::string("unknown output language `" + language + "'"));
}

InputLanguage toInputLanguage(std::string language) {
  if (language == "cvc" || language == "pl" || language == "presentation"
      || language == "native" || language == "LANG_CVC")
  {
    return input::LANG_CVC;
  }
  else if (language == "smtlib" || language == "smt" || language == "smtlib2"
           || language == "smt2" || language == "smtlib2.6"
           || language == "smt2.6" || language == "LANG_SMTLIB_V2_6"
           || language == "LANG_SMTLIB_V2")
  {
    return input::LANG_SMTLIB_V2_6;
  }
  else if (language == "tptp" || language == "LANG_TPTP")
  {
    return input::LANG_TPTP;
  }
  else if (language == "sygus" || language == "sygus2"
           || language == "LANG_SYGUS" || language == "LANG_SYGUS_V2")
  {
    return input::LANG_SYGUS_V2;
  }
  else if (language == "auto" || language == "LANG_AUTO")
  {
    return input::LANG_AUTO;
  }

  throw OptionException(std::string("unknown input language `" + language + "'"));
}/* toInputLanguage() */

}  // namespace language
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

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