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