Added support for LET expressions. Added simple environment support

to SMTParser.


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

1 files changed, 20 insertions, 1 deletions

diff --git a/lib/SMT/SMTParser.h b/lib/SMT/SMTParser.h
index edc1258f..ea5c34e5 100644
--- a/lib/SMT/SMTParser.h
+++ b/lib/SMT/SMTParser.h
@@ -16,7 +16,8 @@
 #include <cassert>
 #include <iostream>
 #include <map>
-#include <cstring>
+#include <stack>
+#include <string>
 
 namespace klee {
 namespace expr {
@@ -53,6 +54,24 @@ class SMTParser : public klee::expr::Parser {
   void Init(void);
 
   int Error(const std::string& s);
+
+
+  typedef std::map<const std::string, ExprHandle> VarEnv;
+  typedef std::map<const std::string, ExprHandle> FVarEnv;
+
+  std::stack<VarEnv> varEnvs;
+  std::stack<FVarEnv> fvarEnvs;
+ 
+
+  void PushVarEnv(void);
+  void PopVarEnv(void);
+  void AddVar(std::string name, ExprHandle val); // to current var env
+  ExprHandle GetVar(std::string name); // from current var env
+
+  void PushFVarEnv(void);
+  void PopFVarEnv(void);
+  void AddFVar(std::string name, ExprHandle val); // to current fvar env
+  ExprHandle GetFVar(std::string name); // from current fvar env
 };
 
 }