From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 22 Jun 2022 21:55:52 +0000 (-0700)
Subject: Simplify printing of command results (#8902)
X-Git-Tag: cvc5-1.0.1~42
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c1738f508bc9dd7615eaa7b7b4af24acfa46f65c;p=cvc5.git

Simplify printing of command results (#8902)

This moves redundant code from `Command::printResult()` overrides to the
base method. This is a step towards simplifying printing options, which
is needed to fix #8893 (which itself is a step towards a parser API).
---

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 174c47e36..fe02770cf 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -163,7 +163,11 @@ bool Command::interrupted() const
 void Command::invoke(cvc5::Solver* solver, SymbolManager* sm, std::ostream& out)
 {
   invoke(solver, sm);
-  if (!(isMuted() && ok()))
+  if (!ok())
+  {
+    out << *d_commandStatus;
+  }
+  else if (!isMuted())
   {
     printResult(out);
   }
@@ -389,15 +393,7 @@ cvc5::Result CheckSatCommand::getResult() const { return d_result; }
 
 void CheckSatCommand::printResult(std::ostream& out) const
 {
-  if (!ok())
-  {
-    this->Command::printResult(out);
-  }
-  else
-  {
-    Trace("dtview::command") << "* RESULT: " << d_result << std::endl;
-    out << d_result << endl;
-  }
+  out << d_result << endl;
 }
 
 Command* CheckSatCommand::clone() const
@@ -457,14 +453,7 @@ cvc5::Result CheckSatAssumingCommand::getResult() const
 
 void CheckSatAssumingCommand::printResult(std::ostream& out) const
 {
-  if (!ok())
-  {
-    this->Command::printResult(out);
-  }
-  else
-  {
-    out << d_result << endl;
-  }
+  out << d_result << endl;
 }
 
 Command* CheckSatAssumingCommand::clone() const
@@ -760,14 +749,7 @@ void CheckSynthCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
 cvc5::SynthResult CheckSynthCommand::getResult() const { return d_result; }
 void CheckSynthCommand::printResult(std::ostream& out) const
 {
-  if (!ok())
-  {
-    this->Command::printResult(out);
-  }
-  else
-  {
-    out << d_solution.str();
-  }
+  out << d_solution.str();
 }
 
 Command* CheckSynthCommand::clone() const { return new CheckSynthCommand(); }
@@ -1401,14 +1383,7 @@ void SimplifyCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
 cvc5::Term SimplifyCommand::getResult() const { return d_result; }
 void SimplifyCommand::printResult(std::ostream& out) const
 {
-  if (!ok())
-  {
-    this->Command::printResult(out);
-  }
-  else
-  {
-    out << d_result << endl;
-  }
+  out << d_result << endl;
 }
 
 Command* SimplifyCommand::clone() const
@@ -1473,16 +1448,9 @@ void GetValueCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
 cvc5::Term GetValueCommand::getResult() const { return d_result; }
 void GetValueCommand::printResult(std::ostream& out) const
 {
-  if (!ok())
-  {
-    this->Command::printResult(out);
-  }
-  else
-  {
-    options::ioutils::Scope scope(out);
-    options::ioutils::applyDagThresh(out, 0);
-    out << d_result << endl;
-  }
+  options::ioutils::Scope scope(out);
+  options::ioutils::applyDagThresh(out, 0);
+  out << d_result << endl;
 }
 
 Command* GetValueCommand::clone() const
@@ -1545,14 +1513,7 @@ void GetAssignmentCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
 cvc5::Term GetAssignmentCommand::getResult() const { return d_result; }
 void GetAssignmentCommand::printResult(std::ostream& out) const
 {
-  if (!ok())
-  {
-    this->Command::printResult(out);
-  }
-  else
-  {
-    out << d_result << endl;
-  }
+  out << d_result << endl;
 }
 
 Command* GetAssignmentCommand::clone() const
@@ -1596,17 +1557,7 @@ void GetModelCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
   }
 }
 
-void GetModelCommand::printResult(std::ostream& out) const
-{
-  if (!ok())
-  {
-    this->Command::printResult(out);
-  }
-  else
-  {
-    out << d_result;
-  }
-}
+void GetModelCommand::printResult(std::ostream& out) const { out << d_result; }
 
 Command* GetModelCommand::clone() const
 {
@@ -1732,17 +1683,7 @@ void GetProofCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
   }
 }
 
-void GetProofCommand::printResult(std::ostream& out) const
-{
-  if (ok())
-  {
-    out << d_result;
-  }
-  else
-  {
-    this->Command::printResult(out);
-  }
-}
+void GetProofCommand::printResult(std::ostream& out) const { out << d_result; }
 
 Command* GetProofCommand::clone() const
 {
@@ -1786,14 +1727,7 @@ void GetInstantiationsCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
 
 void GetInstantiationsCommand::printResult(std::ostream& out) const
 {
-  if (!ok())
-  {
-    this->Command::printResult(out);
-  }
-  else
-  {
-    out << d_solver->getInstantiations();
-  }
+  out << d_solver->getInstantiations();
 }
 
 Command* GetInstantiationsCommand::clone() const
@@ -1864,23 +1798,16 @@ void GetInterpolantCommand::invoke(Solver* solver, SymbolManager* sm)
 
 void GetInterpolantCommand::printResult(std::ostream& out) const
 {
-  if (!ok())
+  options::ioutils::Scope scope(out);
+  options::ioutils::applyDagThresh(out, 0);
+  if (!d_result.isNull())
   {
-    this->Command::printResult(out);
+    out << "(define-fun " << d_name << " () Bool " << d_result << ")"
+        << std::endl;
   }
   else
   {
-    options::ioutils::Scope scope(out);
-    options::ioutils::applyDagThresh(out, 0);
-    if (!d_result.isNull())
-    {
-      out << "(define-fun " << d_name << " () Bool " << d_result << ")"
-          << std::endl;
-    }
-    else
-    {
-      out << "fail" << std::endl;
-    }
+    out << "fail" << std::endl;
   }
 }
 
@@ -1928,23 +1855,16 @@ void GetInterpolantNextCommand::invoke(Solver* solver, SymbolManager* sm)
 
 void GetInterpolantNextCommand::printResult(std::ostream& out) const
 {
-  if (!ok())
+  options::ioutils::Scope scope(out);
+  options::ioutils::applyDagThresh(out, 0);
+  if (!d_result.isNull())
   {
-    this->Command::printResult(out);
+    out << "(define-fun " << d_name << " () Bool " << d_result << ")"
+        << std::endl;
   }
   else
   {
-    options::ioutils::Scope scope(out);
-    options::ioutils::applyDagThresh(out, 0);
-    if (!d_result.isNull())
-    {
-      out << "(define-fun " << d_name << " () Bool " << d_result << ")"
-          << std::endl;
-    }
-    else
-    {
-      out << "fail" << std::endl;
-    }
+    out << "fail" << std::endl;
   }
 }
 
@@ -2015,23 +1935,16 @@ void GetAbductCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
 
 void GetAbductCommand::printResult(std::ostream& out) const
 {
-  if (!ok())
+  options::ioutils::Scope scope(out);
+  options::ioutils::applyDagThresh(out, 0);
+  if (!d_result.isNull())
   {
-    this->Command::printResult(out);
+    out << "(define-fun " << d_name << " () Bool " << d_result << ")"
+        << std::endl;
   }
   else
   {
-    options::ioutils::Scope scope(out);
-    options::ioutils::applyDagThresh(out, 0);
-    if (!d_result.isNull())
-    {
-      out << "(define-fun " << d_name << " () Bool " << d_result << ")"
-          << std::endl;
-    }
-    else
-    {
-      out << "fail" << std::endl;
-    }
+    out << "fail" << std::endl;
   }
 }
 
@@ -2075,23 +1988,16 @@ void GetAbductNextCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
 
 void GetAbductNextCommand::printResult(std::ostream& out) const
 {
-  if (!ok())
+  options::ioutils::Scope scope(out);
+  options::ioutils::applyDagThresh(out, 0);
+  if (!d_result.isNull())
   {
-    this->Command::printResult(out);
+    out << "(define-fun " << d_name << " () Bool " << d_result << ")"
+        << std::endl;
   }
   else
   {
-    options::ioutils::Scope scope(out);
-    options::ioutils::applyDagThresh(out, 0);
-    if (!d_result.isNull())
-    {
-      out << "(define-fun " << d_name << " () Bool " << d_result << ")"
-          << std::endl;
-    }
-    else
-    {
-      out << "fail" << std::endl;
-    }
+    out << "fail" << std::endl;
   }
 }
 
@@ -2155,14 +2061,7 @@ cvc5::Term GetQuantifierEliminationCommand::getResult() const
 }
 void GetQuantifierEliminationCommand::printResult(std::ostream& out) const
 {
-  if (!ok())
-  {
-    this->Command::printResult(out);
-  }
-  else
-  {
-    out << d_result << endl;
-  }
+  out << d_result << endl;
 }
 
 Command* GetQuantifierEliminationCommand::clone() const
@@ -2214,14 +2113,7 @@ std::vector<cvc5::Term> GetUnsatAssumptionsCommand::getResult() const
 
 void GetUnsatAssumptionsCommand::printResult(std::ostream& out) const
 {
-  if (!ok())
-  {
-    this->Command::printResult(out);
-  }
-  else
-  {
-    container_to_stream(out, d_result, "(", ")\n", " ");
-  }
+  container_to_stream(out, d_result, "(", ")\n", " ");
 }
 
 Command* GetUnsatAssumptionsCommand::clone() const
@@ -2268,26 +2160,19 @@ void GetUnsatCoreCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
 
 void GetUnsatCoreCommand::printResult(std::ostream& out) const
 {
-  if (!ok())
+  if (d_solver->getOption("print-unsat-cores-full") == "true")
   {
-    this->Command::printResult(out);
+    // use the assertions
+    UnsatCore ucr(termVectorToNodes(d_result));
+    ucr.toStream(out);
   }
   else
   {
-    if (d_solver->getOption("print-unsat-cores-full") == "true")
-    {
-      // use the assertions
-      UnsatCore ucr(termVectorToNodes(d_result));
-      ucr.toStream(out);
-    }
-    else
-    {
-      // otherwise, use the names
-      std::vector<std::string> names;
-      d_sm->getExpressionNames(d_result, names, true);
-      UnsatCore ucr(names);
-      ucr.toStream(out);
-    }
+    // otherwise, use the names
+    std::vector<std::string> names;
+    d_sm->getExpressionNames(d_result, names, true);
+    UnsatCore ucr(names);
+    ucr.toStream(out);
   }
 }
 
@@ -2342,30 +2227,23 @@ void GetDifficultyCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
 
 void GetDifficultyCommand::printResult(std::ostream& out) const
 {
-  if (!ok())
-  {
-    this->Command::printResult(out);
-  }
-  else
+  out << "(" << std::endl;
+  for (const std::pair<const cvc5::Term, cvc5::Term>& d : d_result)
   {
-    out << "(" << std::endl;
-    for (const std::pair<const cvc5::Term, cvc5::Term>& d : d_result)
+    out << "(";
+    // use name if it has one
+    std::string name;
+    if (d_sm->getExpressionName(d.first, name, true))
     {
-      out << "(";
-      // use name if it has one
-      std::string name;
-      if (d_sm->getExpressionName(d.first, name, true))
-      {
-        out << name;
-      }
-      else
-      {
-        out << d.first;
-      }
-      out << " " << d.second << ")" << std::endl;
+      out << name;
     }
-    out << ")" << std::endl;
+    else
+    {
+      out << d.first;
+    }
+    out << " " << d.second << ")" << std::endl;
   }
+  out << ")" << std::endl;
 }
 
 const std::map<cvc5::Term, cvc5::Term>& GetDifficultyCommand::getDifficultyMap()
@@ -2417,19 +2295,12 @@ void GetLearnedLiteralsCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
 
 void GetLearnedLiteralsCommand::printResult(std::ostream& out) const
 {
-  if (!ok())
+  out << "(" << std::endl;
+  for (const cvc5::Term& lit : d_result)
   {
-    this->Command::printResult(out);
-  }
-  else
-  {
-    out << "(" << std::endl;
-    for (const cvc5::Term& lit : d_result)
-    {
-      out << lit << std::endl;
-    }
-    out << ")" << std::endl;
+    out << lit << std::endl;
   }
+  out << ")" << std::endl;
 }
 
 const std::vector<cvc5::Term>& GetLearnedLiteralsCommand::getLearnedLiterals()
@@ -2481,14 +2352,7 @@ void GetAssertionsCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
 std::string GetAssertionsCommand::getResult() const { return d_result; }
 void GetAssertionsCommand::printResult(std::ostream& out) const
 {
-  if (!ok())
-  {
-    this->Command::printResult(out);
-  }
-  else
-  {
-    out << d_result;
-  }
+  out << d_result;
 }
 
 Command* GetAssertionsCommand::clone() const
@@ -2625,11 +2489,7 @@ void GetInfoCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
 std::string GetInfoCommand::getResult() const { return d_result; }
 void GetInfoCommand::printResult(std::ostream& out) const
 {
-  if (!ok())
-  {
-    this->Command::printResult(out);
-  }
-  else if (d_result != "")
+  if (d_result != "")
   {
     out << d_result << endl;
   }
@@ -2720,11 +2580,7 @@ void GetOptionCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
 std::string GetOptionCommand::getResult() const { return d_result; }
 void GetOptionCommand::printResult(std::ostream& out) const
 {
-  if (!ok())
-  {
-    this->Command::printResult(out);
-  }
-  else if (d_result != "")
+  if (d_result != "")
   {
     out << d_result << endl;
   }
diff --git a/src/smt/command.h b/src/smt/command.h
index beffab0d6..e17105f1e 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -185,7 +185,6 @@ class CVC5_EXPORT Command
 
   /** Get the command status (it's NULL if we haven't run yet). */
   const CommandStatus* getCommandStatus() const { return d_commandStatus; }
-  virtual void printResult(std::ostream& out) const;
 
   /**
    * Clone this Command (make a shallow copy).
@@ -215,6 +214,12 @@ class CVC5_EXPORT Command
   static void resetSolver(cvc5::Solver* solver);
 
  protected:
+  /**
+   * Print the result of running the command. This method is only called if the
+   * command ran successfully.
+   */
+  virtual void printResult(std::ostream& out) const;
+
   // These methods rely on Command being a friend of classes in the API.
   // Subclasses of command should use these methods for conversions,
   // which is currently necessary for e.g. printing commands.