Fix (get-info :authors) (#7373)
authorGereon Kremer <nafur42@gmail.com>
Thu, 14 Oct 2021 23:38:21 +0000 (16:38 -0700)
committerGitHub <noreply@github.com>
Thu, 14 Oct 2021 23:38:21 +0000 (16:38 -0700)
This PR fixes calling (get-info :authors). It used to (try to) print the whole about() information, but failed to do so because the string needed to be turned into an s-expression. However, about() is not properly escaped.
We now simply print the cvc5 authors.
It also fixes isValidGetInfoFlag() which was missing filename.

Fixes #7362.

src/smt/solver_engine.cpp

index 911e0a960aed1ec739560e26ba35b802306100a0..e928dcade1c7868ef90d316909df1ad993f9fbac 100644 (file)
@@ -417,10 +417,10 @@ void SolverEngine::setInfo(const std::string& key, const std::string& value)
 
 bool SolverEngine::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 == "time")
+  if (key == "all-statistics" || key == "error-behavior" || key == "filename"
+      || key == "name" || key == "version" || key == "authors"
+      || key == "status" || key == "time" || key == "reason-unknown"
+      || key == "assertion-stack-levels" || key == "all-options")
   {
     return true;
   }
@@ -455,7 +455,7 @@ std::string SolverEngine::getInfo(const std::string& key) const
   }
   if (key == "authors")
   {
-    return toSExpr(Configuration::about());
+    return toSExpr("the " + Configuration::getName() + " authors");
   }
   if (key == "status")
   {