diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-11-23 08:55:03 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-23 08:55:03 +0100 |
| commit | 961af5e182f65c976424fd2adc22fc9bd484f73c (patch) | |
| tree | 30cac36f195d0899fa4592c778f4547c830e0615 | |
| parent | 2b4d6997eec82dce3832a449eea00f94af420f8a (diff) | |
Add get-info :time. (#5485)
This PR adds the new info `:time` that can be queried with `(get-info :time)` and returns the spent CPU time (as returned by `std::clock()`.
@pjljvandelaar
Fixes CVC4/CVC4-projects#102
| -rw-r--r-- | src/smt/smt_engine.cpp | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2a0cde015..1d623fdef 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -506,7 +506,7 @@ bool SmtEngine::isValidGetInfoFlag(const std::string& key) const if (key == "all-statistics" || key == "error-behavior" || key == "name" || key == "version" || key == "authors" || key == "status" || key == "reason-unknown" || key == "assertion-stack-levels" - || key == "all-options") + || key == "all-options" || key == "time") { return true; } @@ -578,6 +578,10 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const default: return SExpr(SExpr::Keyword("unknown")); } } + if (key == "time") + { + return SExpr(std::clock()); + } if (key == "reason-unknown") { Result status = d_state->getStatus(); |