about summary refs log tree commit diff homepage
path: root/lib/SMT
diff options
context:
space:
mode:
authorDaniel Dunbar <daniel@zuster.org>2009-06-09 00:40:01 +0000
committerDaniel Dunbar <daniel@zuster.org>2009-06-09 00:40:01 +0000
commitfa01d5e65092ad7a502ff8c76281a45226f6bb62 (patch)
treeaed33edb6b5abefeb2551c45d544a54902c19010 /lib/SMT
parentf9f8e5339018dfbe71c6f67575effd1455468875 (diff)
downloadklee-fa01d5e65092ad7a502ff8c76281a45226f6bb62.tar.gz
Remove lang.h, it is unused.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73105 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/SMT')
-rw-r--r--lib/SMT/lang.h71
-rw-r--r--lib/SMT/parser.h1
2 files changed, 0 insertions, 72 deletions
diff --git a/lib/SMT/lang.h b/lib/SMT/lang.h
deleted file mode 100644
index d4683f96..00000000
--- a/lib/SMT/lang.h
+++ /dev/null
@@ -1,71 +0,0 @@
-/*****************************************************************************/
-/*!
- * \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 4e7f05ba..49199eb5 100644
--- a/lib/SMT/parser.h
+++ b/lib/SMT/parser.h
@@ -29,7 +29,6 @@
 #define _cvc3__parser_h_
 
 #include "exception.h"
-#include "lang.h"
 
 namespace CVC3 {