|
ROSE
0.11.145.0
|
SMT solver statistics.
Solver statistics get accumulted into the class statistics only when the solver is destroyed or the solver's resetStatistics method is invoked.
Definition at line 96 of file SmtSolver.h.
#include <Rose/BinaryAnalysis/SmtSolver.h>
Public Member Functions | |
| void | print (std::ostream &, const std::string &prefix="") const |
Public Attributes | |
| size_t | ncalls = 0 |
| Number of times satisfiable() was called. More... | |
| size_t | input_size = 0 |
| Bytes of input generated for satisfiable(). More... | |
| size_t | output_size = 0 |
| Amount of output produced by the SMT solver. More... | |
| size_t | memoizationHits = 0 |
| Number of times memoization supplied a result. More... | |
| size_t | nSolversCreated = 0 |
| Number of solvers created. More... | |
| size_t | nSolversDestroyed = 0 |
| Number of solvers destroyed. More... | |
| double | prepareTime = 0.0 |
| Total time in seconds spent creating assertions before solving. More... | |
| double | longestPrepareTime = 0.0 |
| Longest of times added to prepareTime. More... | |
| double | solveTime = 0.0 |
| Total time in seconds spent in solver's solve function. More... | |
| double | longestSolveTime = 0.0 |
| Longest of times added to the solveTime total. More... | |
| double | evidenceTime = 0.0 |
| Total time in seconds to retrieve evidence of satisfiability. More... | |
| double | longestEvidenceTime = 0.0 |
| Longest of times added to evidenceTime. More... | |
| size_t | nSatisfied = 0 |
| Number of times the solver returned "satisified". More... | |
| size_t | nUnsatisfied = 0 |
| Number of times the solver returned "unsatisfied". More... | |
| size_t | nUnknown = 0 |
| Number of times the solver returned "unknown". More... | |
| size_t Rose::BinaryAnalysis::SmtSolver::Stats::ncalls = 0 |
Number of times satisfiable() was called.
Definition at line 97 of file SmtSolver.h.
| size_t Rose::BinaryAnalysis::SmtSolver::Stats::input_size = 0 |
Bytes of input generated for satisfiable().
Definition at line 98 of file SmtSolver.h.
| size_t Rose::BinaryAnalysis::SmtSolver::Stats::output_size = 0 |
Amount of output produced by the SMT solver.
Definition at line 99 of file SmtSolver.h.
| size_t Rose::BinaryAnalysis::SmtSolver::Stats::memoizationHits = 0 |
Number of times memoization supplied a result.
Definition at line 100 of file SmtSolver.h.
| size_t Rose::BinaryAnalysis::SmtSolver::Stats::nSolversCreated = 0 |
| size_t Rose::BinaryAnalysis::SmtSolver::Stats::nSolversDestroyed = 0 |
| double Rose::BinaryAnalysis::SmtSolver::Stats::prepareTime = 0.0 |
Total time in seconds spent creating assertions before solving.
Definition at line 103 of file SmtSolver.h.
| double Rose::BinaryAnalysis::SmtSolver::Stats::longestPrepareTime = 0.0 |
Longest of times added to prepareTime.
Definition at line 104 of file SmtSolver.h.
| double Rose::BinaryAnalysis::SmtSolver::Stats::solveTime = 0.0 |
Total time in seconds spent in solver's solve function.
Definition at line 105 of file SmtSolver.h.
| double Rose::BinaryAnalysis::SmtSolver::Stats::longestSolveTime = 0.0 |
Longest of times added to the solveTime total.
Definition at line 106 of file SmtSolver.h.
| double Rose::BinaryAnalysis::SmtSolver::Stats::evidenceTime = 0.0 |
Total time in seconds to retrieve evidence of satisfiability.
Definition at line 107 of file SmtSolver.h.
| double Rose::BinaryAnalysis::SmtSolver::Stats::longestEvidenceTime = 0.0 |
Longest of times added to evidenceTime.
Definition at line 108 of file SmtSolver.h.
| size_t Rose::BinaryAnalysis::SmtSolver::Stats::nSatisfied = 0 |
Number of times the solver returned "satisified".
Definition at line 109 of file SmtSolver.h.
| size_t Rose::BinaryAnalysis::SmtSolver::Stats::nUnsatisfied = 0 |
Number of times the solver returned "unsatisfied".
Definition at line 110 of file SmtSolver.h.
| size_t Rose::BinaryAnalysis::SmtSolver::Stats::nUnknown = 0 |
Number of times the solver returned "unknown".
Definition at line 111 of file SmtSolver.h.
1.8.10