Half-bake decision clustering

1 files changed, 13 insertions, 3 deletions

diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index af3a3778..89819157 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -15,7 +15,6 @@
 #ifndef KLEE_EXECUTOR_H
 #define KLEE_EXECUTOR_H
 
-#include "Differentiator.h"
 #include "ExecutionState.h"
 #include "UserSearcher.h"
 
@@ -109,6 +108,12 @@ public:
   RNG theRNG;
 
 private:
+  typedef std::vector<std::string> TestArgs;
+  /// :rev (:var val) stdout
+  typedef std::map<std::uint64_t,
+                   std::pair<std::map<std::string, std::string>,
+                             std::string>> TestOuts;
+
   std::unique_ptr<KModule> kmodule;
   InterpreterHandler *interpreterHandler;
   Searcher *searcher;
@@ -119,7 +124,7 @@ private:
   std::set<ExecutionState*, ExecutionStateIDCompare> states;
   std::set<ExecutionState*, ExecutionStateIDCompare> exitStates;
   std::map<std::uint64_t, std::string> metaEnvVars;
-  std::vector<Differentiator> diffTests;
+  std::map<TestArgs, TestOuts> diffTests;
   StatsTracker *statsTracker;
   TreeStreamWriter *pathWriter, *symPathWriter;
   SpecialFunctionHandler *specialFunctionHandler;
@@ -602,7 +607,12 @@ public:
   MergingSearcher *getMergingSearcher() const { return mergingSearcher; };
   void setMergingSearcher(MergingSearcher *ms) { mergingSearcher = ms; };
 };
-  
+
+/// Return if name matches arg\d\d
+bool isSymArg(std::string);
+
+/// Return if name matches out!.*\d
+bool isSymOut(std::string);
 } // End klee namespace
 
 #endif /* KLEE_EXECUTOR_H */