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 01:02:41 +0000
committerDaniel Dunbar <daniel@zuster.org>2009-06-09 01:02:41 +0000
commit30fb5607cd7f137aa4a8c52e51f00d2508b4a26d (patch)
tree8b9d1fecacb988048f599c0bd2046cf1f86e90aa /lib/SMT
parent76ce7fc9917af0a106550ac501545f7941d17744 (diff)
downloadklee-30fb5607cd7f137aa4a8c52e51f00d2508b4a26d.tar.gz
Remove lang.h again.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73109 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/SMT')
-rw-r--r--lib/SMT/lang.h71
-rw-r--r--lib/SMT/parser.cpp2
-rw-r--r--lib/SMT/parser.h1
3 files changed, 0 insertions, 74 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.cpp b/lib/SMT/parser.cpp
index fd694536..14cf97c8 100644
--- a/lib/SMT/parser.cpp
+++ b/lib/SMT/parser.cpp
@@ -58,8 +58,6 @@ namespace CVC3 {
   // Internal storage class; I'll use member names without 'd_'s here
   class ParserData {
   public:
-    // Which language to use
-    InputLanguage lang;
     // Is the input given by the file name or as istream?
     bool useName;
     ParserTemp temp;
diff --git a/lib/SMT/parser.h b/lib/SMT/parser.h
index 04c2f73b..5f18ab5f 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 {