Add get-info :time. (#5485)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Mon, 23 Nov 2020 07:55:03 +0000 (08:55 +0100)
committerGitHub <noreply@github.com>
Mon, 23 Nov 2020 07:55:03 +0000 (08:55 +0100)
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

src/smt/smt_engine.cpp

index 2a0cde015ad37db48b46321395335e218dc70c25..1d623fdef874bf3e8ac7b0cbc111483088166f4d 100644 (file)
@@ -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();