CVC3  2.4.1
lang.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file lang.h
4  * \brief Definition of input and output languages to CVC3
5  *
6  * Author: Mehul Trivedi
7  *
8  * Created: Thu Jul 29 11:56:34 2004
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 #ifndef _cvc3__lang_h_
23 #define _cvc3__lang_h_
24 
25 #include "debug.h"
26 
27 namespace CVC3 {
28 
29  //! Different input languages
30  typedef enum {
31  //! Nice SAL-like language for manually written specs
33  //! SMT-LIB format
35  //! Lisp-like format for automatically generated specs
37 
39  /* @brief AST is only for printing the Expr abstract syntax tree in lisp
40  format; there is no such input language <em>per se</em> */
41 
42  //! for output into Simplify format
44 
45  //! for output in TPTP format
47 
48  //! for output in SPASS format
50 
51  //! SMT-LIB v2 format
53 
54  } InputLanguage;
55 
56  inline bool isPrefix(const std::string& prefix,
57  const std::string& str) {
58  return str.rfind( prefix, 0 ) == 0;
59  }
60 
61  inline InputLanguage getLanguage(const std::string& lang) {
62  if (lang.size() > 0) {
63  if(isPrefix(lang,"presentation")) {
64  return PRESENTATION_LANG;
65  }
66  if(isPrefix(lang, "lisp")) {
67  return LISP_LANG;
68  }
69  if(isPrefix(lang,"ast")) {
70  return AST_LANG;
71  }
72  if(isPrefix(lang,"tptp")) {
73  return TPTP_LANG;
74  }
75  /* Languages starting with 's' must have at least 2 letters,
76  since there's more than one of them. */
77  if(lang.size() > 1) {
78  if(isPrefix(lang,"simplify")) {
79  return SIMPLIFY_LANG;
80  }
81  if(isPrefix(lang,"spass")) {
82  return SPASS_LANG;
83  }
84  if (lang[ lang.length() - 1 ] == '2' &&
85  isPrefix(lang.substr(0,lang.length()-1),"smtlib")) {
86  return SMTLIB_V2_LANG;
87  }
88  if(isPrefix(lang,"smtlib")) {
89  return SMTLIB_LANG;
90  }
91  }
92 
93  }
94 
95  throw Exception("Bad input language specified");
96  return AST_LANG;
97  }
98 
99 } // end of namespace CVC3
100 
101 #endif