diff options
| author | Martin Nowack <m.nowack@imperial.ac.uk> | 2019-04-01 14:08:43 +0100 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-07-01 15:52:40 +0100 |
| commit | 8a0f1af7500e10dadd97300f242424917d2e9902 (patch) | |
| tree | 48d86b5a1dca9513e4bd1ba8a96441adc0be5169 /lib/Core/Searcher.cpp | |
| parent | da5d238b5a78b54f89728132d71cfa6f8be16d21 (diff) | |
| download | klee-8a0f1af7500e10dadd97300f242424917d2e9902.tar.gz | |
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)
Diffstat (limited to 'lib/Core/Searcher.cpp')
| -rw-r--r-- | lib/Core/Searcher.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index 6b7e9e49..765784c5 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -214,7 +214,9 @@ double WeightedRandomSearcher::getWeight(ExecutionState *es) { return inv; } case QueryCost: - return (es->queryCost.toSeconds() < .1) ? 1. : 1./ es->queryCost.toSeconds(); + return (es->queryMetaData.queryCost.toSeconds() < .1) + ? 1. + : 1. / es->queryMetaData.queryCost.toSeconds(); case CoveringNew: case MinDistToUncovered: { uint64_t md2u = computeMinDistToUncovered(es->pc, |