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
32     PRESENTATION_LANG,
33     //! SMT-LIB format
34     SMTLIB_LANG,
35     //! Lisp-like format for automatically generated specs
36     LISP_LANG,
37 
38     AST_LANG,
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
43     SIMPLIFY_LANG,
44 
45     //! for output in TPTP format
46     TPTP_LANG,
47 
48     //! for output in SPASS format
49     SPASS_LANG,
50 
51     //! SMT-LIB v2 format
52     SMTLIB_V2_LANG
53 
54   } InputLanguage;
55 
isPrefix(const std::string & prefix,const std::string & str)56   inline bool isPrefix(const std::string& prefix,
57                        const std::string& str) {
58     return str.rfind( prefix, 0 ) == 0;
59   }
60 
getLanguage(const std::string & lang)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
102