about summary refs log tree commit diff homepage
path: root/lib/SMT/SMTParser.h
diff options
context:
space:
mode:
Diffstat (limited to 'lib/SMT/SMTParser.h')
-rw-r--r--lib/SMT/SMTParser.h21
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
 };
 
 }