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, 7 insertions, 0 deletions

diff --git a/include/klee/Solver/Solver.h b/include/klee/Solver/Solver.h
index 06b9b573..8d5f87d5 100644
--- a/include/klee/Solver/Solver.h
+++ b/include/klee/Solver/Solver.h
@@ -21,6 +21,13 @@ namespace klee {
   class Expr;
   class SolverImpl;
 
+  /// Collection of meta data used by a solver
+  ///
+  struct SolverQueryMetaData {
+    /// @brief Costs for all queries issued for this state, in seconds
+    time::Span queryCost;
+  };
+
   struct Query {
   public:
     const ConstraintSet &constraints;