Added support for flets.

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

2 files changed, 19 insertions, 36 deletions

diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp
index 395241a0..dee3801c 100644
--- a/lib/SMT/SMTParser.cpp
+++ b/lib/SMT/SMTParser.cpp
@@ -72,7 +72,7 @@ void SMTParser::PushVarEnv() {
 }
 
 void SMTParser::PopVarEnv() {
-  cout << "Popping new var env\n";
+  cout << "Popping var env\n";
   varEnvs.pop();
 }
 
@@ -96,10 +96,12 @@ void SMTParser::PushFVarEnv() {
 }
 
 void SMTParser::PopFVarEnv(void) {
+  cout << "Popping fvar env\n";
   fvarEnvs.pop();
 }
 
 void SMTParser::AddFVar(std::string name, ExprHandle val) {
+  cout << "Adding (" << name << ", " << val << ") to current fvar env.\n";
   fvarEnvs.top()[name] = val;
 }
 
diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y
index 2055d0cd..38e58170 100644
--- a/lib/SMT/smtlib.y
+++ b/lib/SMT/smtlib.y
@@ -100,7 +100,7 @@ int smtliberror(const char *s)
 %type <node> an_formula an_logical_formula an_atom prop_atom
 %type <node> an_term basic_term an_fun an_arithmetic_fun an_pred
 %type <str> logic_name status attribute user_value annotation annotations 
-%type <str> var
+%type <str> var fvar
 
 %token <str> NUMERAL_TOK
 %token <str> SYM_TOK
@@ -474,7 +474,6 @@ an_formula:
       $$ = $1;
     }
 
-
   | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK
         { 
 	  PARSER->PushVarEnv();
@@ -486,26 +485,16 @@ an_formula:
       PARSER->PopVarEnv();
     }
 
-
-/*
-  | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_formula RPAREN_TOK
-    {
-      CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5)));
-      $$ = new CVC3::Expr(VC->listExpr("_LET", e, *$7));
-      delete $4;
-      delete $5;
-      delete $7;
-    }
-
-  | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_formula RPAREN_TOK
+  | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK 
+        { 
+	  PARSER->PushFVarEnv();
+	  PARSER->AddFVar(*$4, $5); 
+	} 
+    an_formula annotations
     {
-      CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5)));
-      $$ = new CVC3::Expr(VC->listExpr("_LET", e, *$7));
-      delete $4;
-      delete $5;
-      delete $7;
+      $$ = $8;
+      PARSER->PopFVarEnv();
     }
-*/
 ;
 
 
@@ -563,20 +552,16 @@ prop_atom:
     {
       $$ = ConstantExpr::create(1, 1);
     }
+
   | FALSE_TOK
     { 
       $$ = ConstantExpr::create(0, 1);;
     }
-/*
+
   | fvar
     {
-      $$ = $1;
+      $$ = PARSER->GetFVar(*$1);
     }
-  | pred_symb 
-    {
-      $$ = $1;
-    }
-*/
 ;  
 
 
@@ -859,16 +844,12 @@ basic_term:
     {
       $$ = ConstantExpr::create(1, 1);
     }
+
   | BIT0_TOK
     { 
       $$ = ConstantExpr::create(0, 1);;
     }
-/*
-  | fvar
-    {
-      $$ = $1;
-    }
-*/
+
   | var
     {
       $$ = PARSER->GetVar(*$1);
@@ -1108,13 +1089,13 @@ var:
     }
 ;
 
-/*
+
 fvar:
     DOLLAR_TOK SYM_TOK
     {
       $$ = $2;
     }
 ;
-*/
+
 
 %%