CVC3

lang.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file lang.h
00004  * \brief Definition of input and output languages to CVC3
00005  * 
00006  * Author: Mehul Trivedi
00007  * 
00008  * Created: Thu Jul 29 11:56:34 2004
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  * 
00019  */
00020 /*****************************************************************************/
00021 
00022 #ifndef _cvc3__lang_h_
00023 #define _cvc3__lang_h_
00024 
00025 #include "debug.h"
00026 
00027 namespace CVC3 {
00028 
00029   //! Different input languages
00030   typedef enum {
00031     //! Nice SAL-like language for manually written specs
00032     PRESENTATION_LANG,
00033     //! SMT-LIB format
00034     SMTLIB_LANG,
00035     //! Lisp-like format for automatically generated specs
00036     LISP_LANG,
00037 
00038     AST_LANG, 
00039     /* @brief AST is only for printing the Expr abstract syntax tree in lisp
00040        format; there is no such input language <em>per se</em> */
00041 
00042     //! for output into Simplify format
00043     SIMPLIFY_LANG,
00044     
00045     //! for output in TPTP format
00046     TPTP_LANG,
00047     
00048     //! for output in SPASS format
00049     SPASS_LANG,
00050 
00051     //! SMT-LIB v2 format
00052     SMTLIB_V2_LANG
00053 
00054   } InputLanguage;
00055   
00056   inline bool isPrefix(const std::string& prefix,
00057                        const std::string& str) {
00058     return str.rfind( prefix, 0 ) == 0;
00059   }
00060 
00061   inline InputLanguage getLanguage(const std::string& lang) {
00062     if (lang.size() > 0) {
00063       if(isPrefix(lang,"presentation")) {
00064         return PRESENTATION_LANG;
00065       }
00066       if(isPrefix(lang, "lisp")) {
00067         return LISP_LANG;
00068       }
00069       if(isPrefix(lang,"ast")) {
00070         return AST_LANG;
00071       }
00072       if(isPrefix(lang,"tptp")) {
00073         return TPTP_LANG;
00074       }
00075       /* Languages starting with 's' must have at least 2 letters,
00076          since there's more than one of them. */
00077       if(lang.size() > 1) {
00078         if(isPrefix(lang,"simplify")) {
00079           return SIMPLIFY_LANG;
00080         } 
00081         if(isPrefix(lang,"spass")) {
00082           return SPASS_LANG;
00083   } 
00084         if (lang[ lang.length() - 1 ] == '2' &&
00085             isPrefix(lang.substr(0,lang.length()-1),"smtlib")) { 
00086           return SMTLIB_V2_LANG;
00087   }
00088         if(isPrefix(lang,"smtlib")) {
00089           return SMTLIB_LANG;
00090         }
00091       }
00092       
00093     }
00094 
00095     throw Exception("Bad input language specified");
00096     return AST_LANG;
00097   }
00098 
00099 } // end of namespace CVC3
00100 
00101 #endif