Revert r73105, I think I was too hasty in killing this.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73107 91177308-0d34-0410-b5e6-96231b3b80d8

2 files changed, 72 insertions, 0 deletions

diff --git a/lib/SMT/lang.h b/lib/SMT/lang.h
new file mode 100644
index 00000000..d4683f96
--- /dev/null
+++ b/lib/SMT/lang.h
@@ -0,0 +1,71 @@
+/*****************************************************************************/
+/*!
+ * \file lang.h
+ * \brief Definition of input and output languages to CVC3
+ * 
+ * Author: Mehul Trivedi
+ * 
+ * Created: Thu Jul 29 11:56:34 2004
+ *
+ * <hr>
+ *
+ * License to use, copy, modify, sell and/or distribute this software
+ * and its documentation for any purpose is hereby granted without
+ * royalty, subject to the terms and conditions defined in the \ref
+ * LICENSE file provided with this distribution.
+ * 
+ * <hr>
+ * 
+ */
+/*****************************************************************************/
+
+#ifndef _cvc3__lang_h_
+#define _cvc3__lang_h_
+
+#include <assert.h>
+#include <stdlib.h>
+
+//#include "debug.h"
+#define FatalAssert(cond, msg) assert(#cond && msg)
+#define DebugAssert(cond, msg) assert(#cond && msg)
+
+namespace CVC3 {
+
+  //! Different input languages
+  typedef enum {
+    //! Nice SAL-like language for manually written specs
+    PRESENTATION_LANG,
+    //! SMT-LIB format
+    SMTLIB_LANG,
+    //! Lisp-like format for automatically generated specs
+    LISP_LANG,
+    AST_LANG,	
+
+    /* @brief AST is only for printing the Expr abstract syntax tree in lisp
+       format; there is no such input language <em>per se</em> */
+    SIMPLIFY_LANG,
+    //! for output into Simplify format
+    TPTP_LANG
+    //! for output in TPTP format
+  } InputLanguage;
+  
+  inline InputLanguage getLanguage(const std::string& lang) {
+    if (lang.size() > 0) {
+      if(lang[0] == 'p') return PRESENTATION_LANG;
+      if(lang[0] == 'l') return LISP_LANG;
+      if(lang[0] == 'a') return AST_LANG;
+      if(lang[0] == 't') return TPTP_LANG;
+      if(lang[0] == 's') {
+        if (lang.size() > 1 && lang[1] == 'i') return SIMPLIFY_LANG;
+        else return SMTLIB_LANG;
+      }
+      
+    }
+
+    throw Exception("Bad input language specified");
+    return AST_LANG;
+  }
+
+} // end of namespace CVC3
+
+#endif
diff --git a/lib/SMT/parser.h b/lib/SMT/parser.h
index 49199eb5..4e7f05ba 100644
--- a/lib/SMT/parser.h
+++ b/lib/SMT/parser.h
@@ -29,6 +29,7 @@
 #define _cvc3__parser_h_
 
 #include "exception.h"
+#include "lang.h"
 
 namespace CVC3 {