CVC3: lang.h Source 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     AST_LANG, 
00038 
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     SIMPLIFY_LANG,
00042     //! for output into Simplify format
00043   } InputLanguage;
00044   
00045   inline InputLanguage getLanguage(const std::string& lang) {
00046     if (lang.size() > 0) {
00047       if(lang[0] == 'p') return PRESENTATION_LANG;
00048       if(lang[0] == 'l') return LISP_LANG;
00049       if(lang[0] == 'a') return AST_LANG;
00050       if(lang[0] == 's') {
00051         if (lang.size() > 1 && lang[1] == 'i') return SIMPLIFY_LANG;
00052         else return SMTLIB_LANG;
00053       }
00054     }
00055 
00056     throw Exception("Bad input language specified");
00057     return AST_LANG;
00058   }
00059 
00060 } // end of namespace CVC3
00061 
00062 #endif