From 0da7412d643890e299cc83d8f09b8b90d0ae94bd Mon Sep 17 00:00:00 2001
From: Cristian Cadar <cristic@cs.stanford.edu>
Date: Thu, 25 Jun 2009 05:42:37 +0000
Subject: Added support for flets.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74167 91177308-0d34-0410-b5e6-96231b3b80d8
---
 lib/SMT/SMTParser.cpp |  4 +++-
 lib/SMT/smtlib.y      | 51 ++++++++++++++++-----------------------------------
 2 files changed, 19 insertions(+), 36 deletions(-)

(limited to 'lib/SMT')

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;
     }
 ;
-*/
+
 
 %%
-- 
cgit 1.4.1