Use constraint sets and separate metadata for timing solver invocation

Decouple ExecutionState from TimingSolver

Instead of providing an execution state to the timing solver use a set of
constraints and an additional object for metadata.

Fixes:
* correct accounting of metadata to a specific state
* accounting of all solver invocations (e.g. solver-getRange was not
accounted)
* allows to invoke the solver without a state (avoids costly copying of
states/constraints)

1 files changed, 3 insertions, 2 deletions

diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index 397b2364..03cad916 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -17,6 +17,7 @@
 #include "klee/Expr/Constraints.h"
 #include "klee/Expr/Expr.h"
 #include "klee/Module/KInstIterator.h"
+#include "klee/Solver/Solver.h"
 #include "klee/System/Time.h"
 
 #include <map>
@@ -96,8 +97,8 @@ public:
 
   /// Statistics and information
 
-  /// @brief Costs for all queries issued for this state, in seconds
-  mutable time::Span queryCost;
+  /// @brief Metadata utilized and collected by solvers for this state
+  mutable SolverQueryMetaData queryMetaData;
 
   /// @brief History of complete path: represents branches taken to
   /// reach/create this state (both concrete and symbolic)