diff options
Diffstat (limited to 'include/klee/Solver/SolverStats.h')
| -rw-r--r-- | include/klee/Solver/SolverStats.h | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/include/klee/Solver/SolverStats.h b/include/klee/Solver/SolverStats.h new file mode 100644 index 00000000..dd39043a --- /dev/null +++ b/include/klee/Solver/SolverStats.h @@ -0,0 +1,38 @@ +//===-- SolverStats.h -------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_SOLVERSTATS_H +#define KLEE_SOLVERSTATS_H + +#include "klee/Statistic.h" + +namespace klee { +namespace stats { + + extern Statistic cexCacheTime; + extern Statistic queries; + extern Statistic queriesInvalid; + extern Statistic queriesValid; + extern Statistic queryCacheHits; + extern Statistic queryCacheMisses; + extern Statistic queryCexCacheHits; + extern Statistic queryCexCacheMisses; + extern Statistic queryConstructTime; + extern Statistic queryConstructs; + extern Statistic queryCounterexamples; + extern Statistic queryTime; + +#ifdef KLEE_ARRAY_DEBUG + extern Statistic arrayHashTime; +#endif + +} +} + +#endif /* KLEE_SOLVERSTATS_H */ |