Add setStringInput to the parser APIs (#10230)

This PR:

Updates the functionality of setIncrementalStringInput / appendIncrementalStringInput to a more intuitive behavior where append does not replace the current contents of the input.
Adds setStringInput to the API and updates the interactive shell to use this interface.
Updates the examples
Adds new unit tests

examples/api/java/Parser.java

@@ -35,8 +35,7 @@ public class Parser
     ss += "(assert (> a (+ b c)))\n";
     ss += "(assert (< a b))\n";
     ss += "(assert (> c 0))\n";
-    parser.setIncrementalStringInput(InputLanguage.SMT_LIB_2_6, "MyStream");
-    parser.appendIncrementalStringInput(ss);
+    parser.setStringInput(InputLanguage.SMT_LIB_2_6, ss, "MyStream");
 
     // get the symbol manager of the parser, used when invoking commands below
     SymbolManager sm = parser.getSymbolManager();

examples/api/java/ParserSymbolManager.java

@@ -32,8 +32,7 @@ public class ParserSymbolManager
     ss += "(declare-fun a () Int)\n";
     ss += "(declare-fun b () Int)\n";
     ss += "(declare-fun c () Bool)\n";
-    parser.setIncrementalStringInput(InputLanguage.SMT_LIB_2_6, "MyStream");
-    parser.appendIncrementalStringInput(ss);
+    parser.setStringInput(InputLanguage.SMT_LIB_2_6, ss, "MyStream");
 
     // parse commands until finished
     Command cmd;

examples/api/python/parser.py

@@ -25,8 +25,6 @@ if __name__ == "__main__":
     # construct an input parser associated the solver above
     parser = cvc5.InputParser(slv)
 
-    parser.setIncrementalStringInput(cvc5.InputLanguage.SMT_LIB_2_6, "MyInput")
-
     input = """
         (set-logic QF_LIA)
         (declare-fun a () Int)
@@ -36,7 +34,8 @@ if __name__ == "__main__":
         (assert (< a b))
         (assert (> c 0))
     """
-    parser.appendIncrementalStringInput(input)
+    
+    parser.setStringInput(cvc5.InputLanguage.SMT_LIB_2_6, input, "MyInput")
 
     # get the symbol manager of the parser, used when invoking commands below
     sm = parser.getSymbolManager()

examples/api/python/parser_sym_manager.py

@@ -24,16 +24,15 @@ if __name__ == "__main__":
 
     # construct an input parser associated the solver above
     parser = cvc5.InputParser(slv, sm)
-
-    parser.setIncrementalStringInput(cvc5.InputLanguage.SMT_LIB_2_6, "MyInput")
-
+    
     input = """
         (set-logic QF_LIA)
         (declare-fun a () Int)
         (declare-fun b () Int)
         (declare-fun c () Bool)
     """
-    parser.appendIncrementalStringInput(input)
+    
+    parser.setStringInput(cvc5.InputLanguage.SMT_LIB_2_6, input, "MyInput")
 
     # parse commands until finished
     while True:

include/cvc5/cvc5_parser.h

@@ -147,7 +147,7 @@ std::ostream& operator<<(std::ostream&, const Command&) CVC5_EXPORT;
  * from an input using a parser.
  *
  * After construction, it is expected that an input is first set via e.g.
- * setFileInput, setStreamInput, or setIncrementalStringInput and
+ * setFileInput, setStreamInput, setStringInput or setIncrementalStringInput and
  * appendIncrementalStringInput. Then, the methods nextCommand and
  * nextExpression can be invoked to parse the input.
  *
@@ -209,6 +209,17 @@ class CVC5_EXPORT InputParser
                       std::istream& input,
                       const std::string& name);
 
+  /**
+   * Set the input to the given concrete input string.
+   *
+   * @param lang the input language
+   * @param input The input string
+   * @param name the name of the stream, for use in error messages
+   */
+  void setStringInput(modes::InputLanguage,
+                      const std::string& input,
+                      const std::string& name);
+
   /**
    * Set that we will be feeding strings to this parser via
    * appendIncrementalStringInput below.
@@ -220,8 +231,7 @@ class CVC5_EXPORT InputParser
                                  const std::string& name);
   /**
    * Append string to the input being parsed by this parser. Should be
-   * called after calling setIncrementalStringInput and only after the
-   * previous string (if one was provided) is finished being parsed.
+   * called after calling setIncrementalStringInput.
    *
    * @param input The input string
    */
@@ -260,10 +270,10 @@ class CVC5_EXPORT InputParser
   std::unique_ptr<SymbolManager> d_allocSm;
   /** Symbol manager */
   SymbolManager* d_sm;
-  /** Incremental string input language */
-  modes::InputLanguage d_istringLang;
-  /** Incremental string name */
-  std::string d_istringName;
+  /** A stringstream, for incremental string inputs */
+  std::stringstream d_istringStream;
+  /** Are we initialized to use the above string stream? */
+  bool d_usingIStringStream;
   /** The parser */
   std::shared_ptr<Parser> d_parser;
 };

src/api/cpp/cvc5_parser.cpp

@@ -152,7 +152,10 @@ std::ostream& operator<<(std::ostream& out, const Command& c)
 /* -------------------------------------------------------------------------- */
 
 InputParser::InputParser(Solver* solver, SymbolManager* sm)
-    : d_solver(solver), d_allocSm(nullptr), d_sm(sm)
+    : d_solver(solver),
+      d_allocSm(nullptr),
+      d_sm(sm),
+      d_usingIStringStream(false)
 {
   initialize();
 }
@@ -197,6 +200,8 @@ void InputParser::initialize()
 
 void InputParser::initializeInternal()
 {
+  // reset to false
+  d_usingIStringStream = false;
   SymManager* sm = d_sm->toSymManager();
   bool slvLogicSet = d_solver->isLogicSet();
   bool smLogicSet = sm->isLogicSet();
@@ -293,6 +298,21 @@ void InputParser::setStreamInput(modes::InputLanguage lang,
   CVC5_API_TRY_CATCH_END;
 }
 
+void InputParser::setStringInput(modes::InputLanguage lang,
+                                 const std::string& input,
+                                 const std::string& name)
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  Trace("parser") << "setStringInput(" << lang << ", ..., " << name << ")"
+                  << std::endl;
+  // initialize the parser
+  d_parser = Parser::mkParser(lang, d_solver, d_sm->toSymManager());
+  initializeInternal();
+  d_parser->setStringInput(input, name);
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
 void InputParser::setIncrementalStringInput(modes::InputLanguage lang,
                                             const std::string& name)
 {
@@ -300,11 +320,13 @@ void InputParser::setIncrementalStringInput(modes::InputLanguage lang,
   //////// all checks before this line
   Trace("parser") << "setIncrementalStringInput(" << lang << ", ..., " << name
                   << ")" << std::endl;
-  d_istringLang = lang;
-  d_istringName = name;
   // initialize the parser
   d_parser = Parser::mkParser(lang, d_solver, d_sm->toSymManager());
   initializeInternal();
+  d_istringStream.str("");
+  d_parser->setStreamInput(d_istringStream, name);
+  // remember that we are using d_istringStream
+  d_usingIStringStream = true;
   ////////
   CVC5_API_TRY_CATCH_END;
 }
@@ -313,9 +335,12 @@ void InputParser::appendIncrementalStringInput(const std::string& input)
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_PARSER_API_CHECK(d_parser != nullptr)
       << "Input to parser not initialized";
+  CVC5_PARSER_API_CHECK(d_usingIStringStream)
+      << "Must call setIncrementalStringInput prior to using "
+         "appendIncrementalStringInput";
   //////// all checks before this line
   Trace("parser") << "appendIncrementalStringInput(...)" << std::endl;
-  d_parser->setStringInput(input, d_istringName);
+  d_istringStream << input;
   ////////
   CVC5_API_TRY_CATCH_END;
 }

src/api/java/io/github/cvc5/InputParser.java

@@ -22,7 +22,7 @@ import io.github.cvc5.modes.InputLanguage;
  * from an input using a parser.
  *
  * After construction, it is expected that an input is first set via e.g.
- * setFileInput, or setIncrementalStringInput and
+ * setFileInput, setStringInput, or setIncrementalStringInput and
  * appendIncrementalStringInput. Then, the methods nextCommand and
  * nextExpression can be invoked to parse the input.
  *
@@ -112,6 +112,19 @@ public class InputParser extends AbstractPointer
 
   private native void setFileInput(long pointer, int langValue, String fileName);
 
+  /**
+   * Set the input to the given concrete input string.
+   *
+   * @param lang The input language.
+   * @param input The input string.
+   * @param name The name of the stream, for use in error messages.
+   */
+  public void setStringInput(InputLanguage lang, String input, String name)
+  {
+    setStringInput(pointer, lang.getValue(), input, name);
+  }
+  private native void setStringInput(long pointer, int langValue, String input, String name);
+
   /**
    * Set that we will be feeding strings to this parser via
    * appendIncrementalStringInput below.
@@ -128,8 +141,7 @@ public class InputParser extends AbstractPointer
 
   /**
    * Append string to the input being parsed by this parser. Should be
-   * called after calling setIncrementalStringInput and only after the
-   * previous string (if one was provided) is finished being parsed.
+   * called after calling setIncrementalStringInput.
    *
    * @param input The input string.
    */

src/api/java/jni/input_parser.cpp

@@ -114,6 +114,32 @@ JNIEXPORT void JNICALL Java_io_github_cvc5_InputParser_setFileInput(
   CVC5_JAVA_API_TRY_CATCH_END(env);
 }
 
+/*
+ * Class:     io_github_cvc5_InputParser
+ * Method:    setStringInput
+ * Signature: (JILjava/lang/String;Ljava/lang/String;)V
+ */
+JNIEXPORT void JNICALL
+Java_io_github_cvc5_InputParser_setStringInput(JNIEnv* env,
+                                               jobject,
+                                               jlong pointer,
+                                               jint langValue,
+                                               jstring jInput,
+                                               jstring jName)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  InputParser* parser = reinterpret_cast<InputParser*>(pointer);
+  modes::InputLanguage lang = static_cast<modes::InputLanguage>(langValue);
+  const char* cInput = env->GetStringUTFChars(jInput, nullptr);
+  std::string sInput(cInput);
+  const char* cName = env->GetStringUTFChars(jName, nullptr);
+  std::string sName(cName);
+  parser->setStringInput(lang, sInput, sName);
+  env->ReleaseStringUTFChars(jName, cName);
+  env->ReleaseStringUTFChars(jName, cInput);
+  CVC5_JAVA_API_TRY_CATCH_END(env);
+}
+
 /*
  * Class:     io_github_cvc5_InputParser
  * Method:    setIncrementalStringInput

src/api/python/cvc5.pxd

@@ -588,8 +588,9 @@ cdef extern from "<cvc5/cvc5_parser.h>" namespace "cvc5::parser":
     cdef cppclass InputParser:
         InputParser(Solver* solver, SymbolManager* sm) except +
         void setFileInput(InputLanguage lang, const string& filename) except +
+        void setStringInput(InputLanguage lang, const string& input, const string& name) except +
         void setIncrementalStringInput(InputLanguage lang, const string& name) except +
         void appendIncrementalStringInput(const string& input) except +
         Command nextCommand() except +
         Term nextTerm() except +
-        bint done() except +
+        bint done() except +

src/api/python/cvc5.pxi

@@ -184,7 +184,7 @@ cdef class InputParser:
         from an input using a parser.
 
         After construction, it is expected that an input is first set via e.g.
-        :py:meth:`setFileInput`, :py:meth:`setStreamInput`, or
+        :py:meth:`setFileInput`, :py:meth:`setStringInput`, or
         :py:meth:`setIncrementalStringInput` and :py:meth:`appendIncrementalStringInput`.
         Then, the methods :py:meth:`nextCommand` and
         :py:meth:`nextExpression` can be invoked to parse the input.
@@ -241,6 +241,16 @@ cdef class InputParser:
         """
         self.cip.setFileInput(<c_InputLanguage> lang.value, filename.encode())
 
+    def setStringInput(self, lang, str input, str name):
+        """
+            Set the input to the given concrete string
+
+            :param lang: The input language (e.g. InputLanguage.SMT_LIB_2_6).
+            :param input: The input string.
+            :param name: The name of the stream, for use in error messages.
+        """
+        self.cip.setStringInput(<c_InputLanguage> lang.value, input.encode(), name.encode())
+
     def setIncrementalStringInput(self, lang, str name):
         """
             Set that we will be feeding strings to this parser via
@@ -254,8 +264,7 @@ cdef class InputParser:
     def appendIncrementalStringInput(self, str input):
         """
             Append string to the input being parsed by this parser. Should be
-            called after calling setIncrementalStringInput and only after the
-            previous string (if one was provided) is finished being parsed.
+            called after calling setIncrementalStringInput.
 
             :param input: The input string.
         """

src/main/interactive_shell.cpp

@@ -46,7 +46,6 @@
 #include "base/output.h"
 #include "main/command_executor.h"
 #include "parser/commands.h"
-#include <cvc5/cvc5_parser.h>
 #include "parser/sym_manager.h"
 #include "theory/logic_info.h"
 
@@ -95,14 +94,13 @@ InteractiveShell::InteractiveShell(main::CommandExecutor* cexec,
   d_parser.reset(
       new cvc5::parser::InputParser(d_solver, cexec->getSymbolManager()));
   std::string langs = d_solver->getOption("input-language");
-  modes::InputLanguage lang;
   if (langs == "LANG_SMTLIB_V2_6")
   {
-    lang = modes::InputLanguage::SMT_LIB_2_6;
+    d_lang = modes::InputLanguage::SMT_LIB_2_6;
   }
   else if (langs == "LANG_SYGUS_V2")
   {
-    lang = modes::InputLanguage::SYGUS_2_1;
+    d_lang = modes::InputLanguage::SYGUS_2_1;
   }
   else
   {
@@ -110,7 +108,6 @@ InteractiveShell::InteractiveShell(main::CommandExecutor* cexec,
   }
 
   // initialize for incremental string input
-  d_parser->setIncrementalStringInput(lang, INPUT_FILENAME);
   d_usingEditline = false;
 #if HAVE_LIBEDITLINE
   if (&d_in == &std::cin && isatty(fileno(stdin)))
@@ -123,7 +120,7 @@ InteractiveShell::InteractiveShell(main::CommandExecutor* cexec,
 #endif /* EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP */
     ::using_history();
 
-    if (lang == modes::InputLanguage::SMT_LIB_2_6)
+    if (d_lang == modes::InputLanguage::SMT_LIB_2_6)
     {
       d_historyFilename = string(getenv("HOME")) + "/.cvc5_history_smtlib2";
       commandsBegin = smt2_commands;
@@ -312,7 +309,7 @@ restart:
     }
   }
 
-  d_parser->appendIncrementalStringInput(input);
+  d_parser->setStringInput(d_lang, input, INPUT_FILENAME);
 
   /* There may be more than one command in the input. Build up a
      sequence. */

src/main/interactive_shell.h

@@ -16,6 +16,8 @@
 #ifndef CVC5__INTERACTIVE_SHELL_H
 #define CVC5__INTERACTIVE_SHELL_H
 
+#include <cvc5/cvc5_types.h>
+
 #include <iosfwd>
 #include <memory>
 #include <optional>
@@ -74,6 +76,8 @@ class InteractiveShell
   bool d_isInteractive;
   bool d_quit;
   bool d_usingEditline;
+  /** The language */
+  modes::InputLanguage d_lang;
 
   std::string d_historyFilename;
 

test/unit/api/cpp/input_parser_black.cpp

@@ -94,6 +94,27 @@ TEST_F(TestInputParserBlack, setStreamInput)
 }
 
 TEST_F(TestInputParserBlack, setAndAppendIncrementalStringInput)
+{
+  std::stringstream out;
+  InputParser p(&d_solver);
+  p.setIncrementalStringInput(modes::InputLanguage::SMT_LIB_2_6,
+                              "input_parser_black");
+  Command cmd;
+  p.appendIncrementalStringInput("(set-logic ALL)");
+  p.appendIncrementalStringInput("(declare-fun a () Bool)");
+  p.appendIncrementalStringInput("(declare-fun b () Int)");
+  cmd = p.nextCommand();
+  ASSERT_NE(cmd.isNull(), true);
+  ASSERT_NO_THROW(cmd.invoke(&d_solver, d_symman.get(), out));
+  cmd = p.nextCommand();
+  ASSERT_NE(cmd.isNull(), true);
+  ASSERT_NO_THROW(cmd.invoke(&d_solver, d_symman.get(), out));
+  cmd = p.nextCommand();
+  ASSERT_NE(cmd.isNull(), true);
+  ASSERT_NO_THROW(cmd.invoke(&d_solver, d_symman.get(), out));
+}
+
+TEST_F(TestInputParserBlack, setAndAppendIncrementalStringInputInterleave)
 {
   std::stringstream out;
   InputParser p(&d_solver);
@@ -114,6 +135,28 @@ TEST_F(TestInputParserBlack, setAndAppendIncrementalStringInput)
   ASSERT_NO_THROW(cmd.invoke(&d_solver, d_symman.get(), out));
 }
 
+TEST_F(TestInputParserBlack, appendIncrementalNoSet)
+{
+  InputParser p(&d_solver);
+  ASSERT_THROW(p.appendIncrementalStringInput("(set-logic ALL)"),
+               CVC5ApiException);
+}
+
+TEST_F(TestInputParserBlack, setStringInput)
+{
+  std::stringstream out;
+  InputParser p(&d_solver);
+  Command cmd;
+  p.setStringInput(modes::InputLanguage::SMT_LIB_2_6,
+                   "(set-logic ALL)",
+                   "input_parser_black");
+  cmd = p.nextCommand();
+  ASSERT_NE(cmd.isNull(), true);
+  ASSERT_NO_THROW(cmd.invoke(&d_solver, d_symman.get(), out));
+  cmd = p.nextCommand();
+  ASSERT_EQ(cmd.isNull(), true);
+}
+
 TEST_F(TestInputParserBlack, nextCommand)
 {
   InputParser p(&d_solver);
@@ -124,6 +167,17 @@ TEST_F(TestInputParserBlack, nextCommand)
   ASSERT_EQ(cmd.isNull(), true);
 }
 
+TEST_F(TestInputParserBlack, nextCommandNoInput)
+{
+  InputParser p(&d_solver);
+  p.setIncrementalStringInput(modes::InputLanguage::SMT_LIB_2_6,
+                              "input_parser_black");
+  Command cmd = p.nextCommand();
+  ASSERT_EQ(cmd.isNull(), true);
+  Term t = p.nextTerm();
+  ASSERT_EQ(t.isNull(), true);
+}
+
 TEST_F(TestInputParserBlack, nextTerm)
 {
   InputParser p(&d_solver);
@@ -140,20 +194,20 @@ TEST_F(TestInputParserBlack, nextTerm2)
   p.setIncrementalStringInput(modes::InputLanguage::SMT_LIB_2_6,
                               "input_parser_black");
   // parse a declaration command
-  p.appendIncrementalStringInput("(declare-fun a () Int)");
+  p.appendIncrementalStringInput("(declare-fun a () Int)\n");
   Command cmd = p.nextCommand();
   ASSERT_NE(cmd.isNull(), true);
   ASSERT_NO_THROW(cmd.invoke(&d_solver, d_symman.get(), out));
   // now parse some terms
   Term t;
-  p.appendIncrementalStringInput("45");
+  p.appendIncrementalStringInput("45\n");
   ASSERT_NO_THROW(t = p.nextTerm());
   ASSERT_EQ(t.isNull(), false);
-  p.appendIncrementalStringInput("(+ a 1)");
+  p.appendIncrementalStringInput("(+ a 1)\n");
   ASSERT_NO_THROW(t = p.nextTerm());
   ASSERT_EQ(t.isNull(), false);
   ASSERT_EQ(t.getKind(), Kind::ADD);
-  p.appendIncrementalStringInput("(+ b 1)");
+  p.appendIncrementalStringInput("(+ b 1)\n");
   ASSERT_THROW(t = p.nextTerm(), ParserException);
 }
 

test/unit/api/java/InputParserTest.java

@@ -60,6 +60,28 @@ class InputParserTest extends ParserTest
 
   @Test
   void setAndAppendIncrementalStringInput()
+  {
+    InputParser p = new InputParser(d_solver);
+    p.setIncrementalStringInput(InputLanguage.SMT_LIB_2_6, "input_parser_black");
+    p.appendIncrementalStringInput("(set-logic ALL)");
+    p.appendIncrementalStringInput("(declare-fun a () Bool)");
+    p.appendIncrementalStringInput("(declare-fun b () Int)");
+
+    final Command cmd1 = p.nextCommand();
+    assertNotEquals(cmd1.isNull(), true);
+    assertDoesNotThrow(() -> cmd1.invoke(d_solver, d_symman));
+
+    final Command cmd2 = p.nextCommand();
+    assertNotEquals(cmd2.isNull(), true);
+    assertDoesNotThrow(() -> cmd2.invoke(d_solver, d_symman));
+
+    final Command cmd3 = p.nextCommand();
+    assertNotEquals(cmd3.isNull(), true);
+    assertDoesNotThrow(() -> cmd3.invoke(d_solver, d_symman));
+  }
+
+  @Test
+  void setAndAppendIncrementalStringInputInterleave()
   {
     InputParser p = new InputParser(d_solver);
     p.setIncrementalStringInput(InputLanguage.SMT_LIB_2_6, "input_parser_black");
@@ -80,6 +102,25 @@ class InputParserTest extends ParserTest
     assertDoesNotThrow(() -> cmd3.invoke(d_solver, d_symman));
   }
 
+  @Test
+  void appendIncrementalNoSet()
+  {
+    InputParser p = new InputParser(d_solver);
+    assertThrows(CVC5ApiException.class, () -> p.appendIncrementalStringInput("(set-logic ALL)"));
+  }
+
+  @Test
+  void setStringInput()
+  {
+    InputParser p = new InputParser(d_solver);
+    p.setStringInput(InputLanguage.SMT_LIB_2_6, "(set-logic ALL)", "input_parser_black");
+    final Command cmd1 = p.nextCommand();
+    assertNotEquals(cmd1.isNull(), true);
+    assertDoesNotThrow(() -> cmd1.invoke(d_solver, d_symman));
+    final Command cmd2 = p.nextCommand();
+    assertEquals(cmd2.isNull(), true);
+  }
+
   @Test
   void nextCommand()
   {
@@ -91,6 +132,17 @@ class InputParserTest extends ParserTest
     assertEquals(cmd.isNull(), true);
   }
 
+  @Test
+  void nextCommandNoInput()
+  {
+    InputParser p = new InputParser(d_solver);
+    p.setIncrementalStringInput(InputLanguage.SMT_LIB_2_6, "input_parser_black");
+    Command cmd = p.nextCommand();
+    assertEquals(cmd.isNull(), true);
+    Term t = p.nextTerm();
+    assertEquals(t.isNull(), true);
+  }
+
   @Test
   void nextTerm()
   {
@@ -107,26 +159,26 @@ class InputParserTest extends ParserTest
     InputParser p = new InputParser(d_solver, d_symman);
     p.setIncrementalStringInput(InputLanguage.SMT_LIB_2_6, "input_parser_black");
     // parse a declaration command
-    p.appendIncrementalStringInput("(declare-fun a () Int)");
+    p.appendIncrementalStringInput("(declare-fun a () Int)\n");
     final Command cmd1 = p.nextCommand();
     assertNotEquals(cmd1.isNull(), true);
     assertDoesNotThrow(() -> cmd1.invoke(d_solver, d_symman));
     // now parse some terms
 
-    p.appendIncrementalStringInput("45");
+    p.appendIncrementalStringInput("45\n");
     assertDoesNotThrow(() -> {
       Term t = p.nextTerm();
       assertEquals(t.isNull(), false);
     });
 
-    p.appendIncrementalStringInput("(+ a 1)");
+    p.appendIncrementalStringInput("(+ a 1)\n");
     assertDoesNotThrow(() -> {
       Term t = p.nextTerm();
       assertEquals(t.isNull(), false);
       assertEquals(t.getKind(), Kind.ADD);
     });
 
-    p.appendIncrementalStringInput("(+ b 1)");
+    p.appendIncrementalStringInput("(+ b 1)\n");
     assertThrows(CVC5ParserException.class, () -> { Term t = p.nextTerm(); });
   }
 

test/unit/api/python/test_input_parser.py

@@ -43,6 +43,26 @@ def test_set_file_input(solver):
         p.setFileInput(cvc5.InputLanguage.SMT_LIB_2_6, "nonexistent.smt2")
 
 def test_set_and_append_incremental_string_input(solver):
+    sm = SymbolManager(solver)
+    p = InputParser(solver, sm)
+    p.setIncrementalStringInput(cvc5.InputLanguage.SMT_LIB_2_6, "test_input_parser")
+    p.appendIncrementalStringInput("(set-logic ALL)")
+    p.appendIncrementalStringInput("(declare-fun a () Bool)")
+    p.appendIncrementalStringInput("(declare-fun b () Int)")
+    cmd = p.nextCommand()
+    assert cmd.isNull() is not True
+    with does_not_raise():
+        cmd.invoke(solver, sm)
+    cmd = p.nextCommand()
+    assert cmd.isNull() is not True
+    with does_not_raise():
+        cmd.invoke(solver, sm)
+    cmd = p.nextCommand()
+    assert cmd.isNull() is not True
+    with does_not_raise():
+        cmd.invoke(solver, sm)
+
+def test_set_and_append_incremental_string_input_interleave(solver):
     sm = SymbolManager(solver)
     p = InputParser(solver, sm)
     p.setIncrementalStringInput(cvc5.InputLanguage.SMT_LIB_2_6, "test_input_parser")
@@ -62,13 +82,30 @@ def test_set_and_append_incremental_string_input(solver):
     with does_not_raise():
         cmd.invoke(solver, sm)
 
-# def test_next_command_no_input(solver):
-#     p = InputParser(solver)
-#     p.setIncrementalStringInput(cvc5.InputLanguage.SMT_LIB_2_6, "test_input_parser")
-#     cmd = p.nextCommand()
-#     assert cmd.isNull() is True
-#     t = p.nextTerm()
-#     assert cmd.isNull() is True
+def test_append_incremental_no_set(solver):
+    sm = SymbolManager(solver)
+    p = InputParser(solver, sm)
+    with pytest.raises(RuntimeError):
+        p.appendIncrementalStringInput("(set-logic ALL)")
+
+def test_set_string_input(solver):
+    sm = SymbolManager(solver)
+    p = InputParser(solver, sm)
+    p.setStringInput(cvc5.InputLanguage.SMT_LIB_2_6, "(set-logic ALL)", "test_input_parser")
+    cmd = p.nextCommand()
+    assert cmd.isNull() is False
+    with does_not_raise():
+        cmd.invoke(solver, sm)
+    cmd = p.nextCommand()
+    assert cmd.isNull() is True
+
+def test_next_command_no_input(solver):
+    p = InputParser(solver)
+    p.setIncrementalStringInput(cvc5.InputLanguage.SMT_LIB_2_6, "test_input_parser")
+    cmd = p.nextCommand()
+    assert cmd.isNull() is True
+    t = p.nextTerm()
+    assert cmd.isNull() is True
 
 def test_next_term(solver):
     p = InputParser(solver)
@@ -89,16 +126,16 @@ def test_next_term2(solver):
         cmd.invoke(solver, sm)
     # now parse some terms
     t = None
-    p.appendIncrementalStringInput("45")
+    p.appendIncrementalStringInput("45\n")
     with does_not_raise():
         t = p.nextTerm()
     assert t.isNull() is False
-    p.appendIncrementalStringInput("(+ a 1)")
+    p.appendIncrementalStringInput("(+ a 1)\n")
     with does_not_raise():
         t = p.nextTerm()
     assert t.isNull() is False
     assert t.getKind() == cvc5.Kind.ADD
-    p.appendIncrementalStringInput("(+ b 1)")
+    p.appendIncrementalStringInput("(+ b 1)\n")
     with pytest.raises(RuntimeError):
         t = p.nextTerm()
 

test/unit/test_with_smt_parser.h

@@ -61,8 +61,7 @@ class TestWithSmtParser : public TestInternal
    */
   void doCommand(const std::string& s)
   {
-    d_ip->setIncrementalStringInput(modes::InputLanguage::SMT_LIB_2_6, "temp");
-    d_ip->appendIncrementalStringInput(s);
+    d_ip->setStringInput(modes::InputLanguage::SMT_LIB_2_6, s, "temp");
     auto command = d_ip->nextCommand();
     command.invoke(&d_solver, d_symman.get(), std::cout);
   }
@@ -72,8 +71,7 @@ class TestWithSmtParser : public TestInternal
    */
   Node parseNode(const std::string& s)
   {
-    d_ip->setIncrementalStringInput(modes::InputLanguage::SMT_LIB_2_6, "temp");
-    d_ip->appendIncrementalStringInput(s);
+    d_ip->setStringInput(modes::InputLanguage::SMT_LIB_2_6, s, "temp");
     return *d_ip->nextTerm().d_node;
   }