about summary refs log tree commit diff homepage
path: root/lib/SMT
diff options
context:
space:
mode:
authorCristian Cadar <cristic@cs.stanford.edu>2009-06-08 08:10:42 +0000
committerCristian Cadar <cristic@cs.stanford.edu>2009-06-08 08:10:42 +0000
commit9e9d2177ebaeba1e14a29b479de8e6465bb2f162 (patch)
tree06f1e6516e7eb64ac130e03d0619b5cd2b58a2c3 /lib/SMT
parent17af2a1562d9d3c0bfac8a5fa56cb622b95fbacb (diff)
downloadklee-9e9d2177ebaeba1e14a29b479de8e6465bb2f162.tar.gz
Removed support for the PL and Lisp languages.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73060 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/SMT')
-rw-r--r--lib/SMT/parser.cpp55
1 files changed, 0 insertions, 55 deletions
diff --git a/lib/SMT/parser.cpp b/lib/SMT/parser.cpp
index 92693c35..c960c16d 100644
--- a/lib/SMT/parser.cpp
+++ b/lib/SMT/parser.cpp
@@ -29,33 +29,6 @@ using namespace std;
 
 // The communication entry points of the actual parsers
 
-// for presentation language (PL.y and PL.lex)
-extern int PLparse(); 
-extern void *PL_createBuffer(int);
-extern void PL_deleteBuffer(void *);
-extern void PL_switchToBuffer(void *);
-extern int PL_bufSize();
-extern void *PL_bufState();
-void PL_setInteractive(bool);
-
-// for Lisp language (Lisp.y and Lisp.lex)
-extern int Lispparse(); 
-extern void *Lisp_createBuffer(int);
-extern void Lisp_deleteBuffer(void *);
-extern void Lisp_switchToBuffer(void *);
-extern int Lisp_bufSize();
-extern void *LispBufState();
-void Lisp_setInteractive(bool);
-
-// for Lisp language (Lisp.y and Lisp.lex)
-extern int Lispparse(); 
-extern void *Lisp_createBuffer(int);
-extern void Lisp_deleteBuffer(void *);
-extern void Lisp_switchToBuffer(void *);
-extern int Lisp_bufSize();
-extern void *LispBufState();
-void Lisp_setInteractive(bool);
-
 // for smtlib language (smtlib.y and smtlib.lex)
 extern int smtlibparse(); 
 extern void *smtlib_createBuffer(int);
@@ -142,14 +115,6 @@ namespace CVC3 {
   // Initialize the actual parser
   void Parser::initParser() {
     switch(d_data->lang) {
-    case PRESENTATION_LANG:
-      d_data->buffer = PL_createBuffer(PL_bufSize());
-      d_data->temp.lineNum = 1;
-      break;
-    case LISP_LANG:
-      d_data->buffer = Lisp_createBuffer(Lisp_bufSize());
-      d_data->temp.lineNum = 1;
-      break;
     case SMTLIB_LANG:
       d_data->buffer = smtlib_createBuffer(smtlib_bufSize());
       d_data->temp.lineNum = 1;
@@ -161,12 +126,6 @@ namespace CVC3 {
   // Clean up the parser's internal data structures
   void Parser::deleteParser() {
     switch(d_data->lang) {
-    case PRESENTATION_LANG:
-      PL_deleteBuffer(d_data->buffer);
-      break;
-    case LISP_LANG:
-      Lisp_deleteBuffer(d_data->buffer);
-      break;
     case SMTLIB_LANG:
       smtlib_deleteBuffer(d_data->buffer);
       break;
@@ -184,20 +143,6 @@ namespace CVC3 {
     // the parser running
     try {
       switch(d_data->lang) {
-      case PRESENTATION_LANG:
-      	PL_switchToBuffer(d_data->buffer);
-	PL_setInteractive(d_data->temp.interactive);
-	PLparse();
-	// Reset the prompt to the main one
-	d_data->temp.setPrompt1();
-	break;
-      case LISP_LANG:
-        Lisp_switchToBuffer(d_data->buffer);
-	Lisp_setInteractive(d_data->temp.interactive);
-	Lispparse();
-	// Reset the prompt to the main one
-	d_data->temp.setPrompt1();
-	break;
       case SMTLIB_LANG:
         smtlib_switchToBuffer(d_data->buffer);
 	smtlib_setInteractive(d_data->temp.interactive);