CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
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
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
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
Generated on Sat Aug 3 2013 07:58:27 for CVC3 by
1.8.4