Fixes for uncovered parser API methods (cvc5#10082)

Fixes nightly builds.
ajreynol · Oct 4, 2023 · 3621c2c · 3621c2c
1 parent 74443f1
commit 3621c2c
Show file tree

Hide file tree

Showing 7 changed files with 17 additions and 19 deletions.
diff --git a/include/cvc5/cvc5_parser.h b/include/cvc5/cvc5_parser.h
@@ -101,8 +101,6 @@ class CVC5_EXPORT Command
   Command();
   Command(const Command& cmd);
 
-  virtual ~Command();
-
   /**
    * Invoke the command on the solver and symbol manager sm, prints the result
    * to output stream out.
@@ -132,7 +130,7 @@ class CVC5_EXPORT Command
    */
   bool isNull() const;
 
- protected:
+ private:
   /**
    * Constructor.
    * @param n The internal command that is to be wrapped by this command.
@@ -146,7 +144,6 @@ class CVC5_EXPORT Command
 }; /* class Command */
 
 std::ostream& operator<<(std::ostream&, const Command&) CVC5_EXPORT;
-std::ostream& operator<<(std::ostream&, const Command*) CVC5_EXPORT;
 
 /**
  * This class is the main interface for retrieving commands and expressions

diff --git a/src/api/cpp/cvc5_parser.cpp b/src/api/cpp/cvc5_parser.cpp
@@ -98,8 +98,6 @@ Command::Command(const Command& cmd) { d_cmd = cmd.d_cmd; }
 
 Command::Command(std::shared_ptr<Cmd> cmd) : d_cmd(cmd) {}
 
-Command::~Command() {}
-
 bool Command::isNull() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
@@ -153,19 +151,6 @@ std::ostream& operator<<(std::ostream& out, const Command& c)
   return out;
 }
 
-std::ostream& operator<<(std::ostream& out, const Command* c)
-{
-  if (c == nullptr)
-  {
-    out << "null";
-  }
-  else
-  {
-    out << *c;
-  }
-  return out;
-}
-
 /* -------------------------------------------------------------------------- */
 /* InputParser                                                                */
 /* -------------------------------------------------------------------------- */

diff --git a/test/unit/api/cpp/command_black.cpp b/test/unit/api/cpp/command_black.cpp
@@ -70,6 +70,9 @@ TEST_F(TestCommandBlack, toString)
   ASSERT_NE(cmd.isNull(), true);
   // note normalizes wrt whitespace
   ASSERT_EQ(cmd.toString(), "(set-logic QF_LIA)\n");
+  std::stringstream ss;
+  ss << cmd;
+  ASSERT_EQ(cmd.toString(), ss.str());
 }
 
 TEST_F(TestCommandBlack, getCommandName)

diff --git a/test/unit/api/cpp/input_parser_black.cpp b/test/unit/api/cpp/input_parser_black.cpp
@@ -63,6 +63,14 @@ TEST_F(TestInputParserBlack, getSymbolManager)
   ASSERT_EQ(p2.getSymbolManager(), d_symman.get());
 }
 
+TEST_F(TestInputParserBlack, setFileInput)
+{
+  InputParser p(&d_solver);
+  ASSERT_THROW(
+      p.setFileInput(modes::InputLanguage::SMT_LIB_2_6, "nonexistent.smt2"),
+      CVC5ApiException);
+}
+
 TEST_F(TestInputParserBlack, setStreamInput)
 {
   InputParser p(&d_solver);
@@ -71,6 +79,7 @@ TEST_F(TestInputParserBlack, setStreamInput)
   ss << "(declare-fun a () Bool)" << std::endl;
   ss << "(declare-fun b () Int)" << std::endl;
   p.setStreamInput(modes::InputLanguage::SMT_LIB_2_6, ss, "input_parser_black");
+  ASSERT_EQ(p.done(), false);
   Command cmd;
   std::stringstream out;
   while (true)
@@ -82,6 +91,7 @@ TEST_F(TestInputParserBlack, setStreamInput)
     }
     ASSERT_NO_THROW(cmd.invoke(&d_solver, d_symman.get(), out));
   }
+  ASSERT_EQ(p.done(), true);
 }
 
 TEST_F(TestInputParserBlack, setAndAppendIncrementalStringInput)

diff --git a/test/unit/api/cpp/types_black.cpp b/test/unit/api/cpp/types_black.cpp
@@ -37,6 +37,7 @@ TEST_F(TestApiTypes, printEnum)
   ss << cvc5::modes::LearnedLitType::PREPROCESS;
   ss << cvc5::modes::ProofComponent::FULL;
   ss << cvc5::modes::FindSynthTarget::ENUM;
+  ss << cvc5::modes::InputLanguage::SMT_LIB_2_6;
 }
 
 }  // namespace test

diff --git a/test/unit/api/java/UncoveredTest.cpp b/test/unit/api/java/UncoveredTest.cpp
@@ -99,6 +99,7 @@ TEST_F(TestApiBlackUncovered, streaming_operators)
   ss << cvc5::modes::ProofComponent::FULL;
   ss << cvc5::modes::FindSynthTarget::ENUM;
   ss << cvc5::ProofRule::ASSUME;
+  ss << cvc5::modes::InputLanguage::SMT_LIB_2_6;
   ss << cvc5::Result();
   ss << cvc5::Op();
   ss << cvc5::SynthResult();

diff --git a/test/unit/api/python/test_uncovered.cpp b/test/unit/api/python/test_uncovered.cpp
@@ -50,6 +50,7 @@ TEST_F(TestApiBlackUncovered, streaming_operators)
   ss << cvc5::modes::ProofComponent::FULL;
   ss << cvc5::modes::FindSynthTarget::ENUM;
   ss << cvc5::ProofRule::ASSUME;
+  ss << cvc5::modes::InputLanguage::SMT_LIB_2_6;
   ss << cvc5::Result();
   ss << cvc5::Op();
   ss << cvc5::SynthResult();