Remove `--(no-)interactive-prompt` (#7022)

This option is mostly redundant: It offers a way to access the
interactive shell without any copyright information or cvc5> prompt
being printed. However, --no-interactive offers the same experience
(except for the features offered by libedit).

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 8c86f03cb9efe263c787ed02233ddee5211740b5..606f18095724d45ba9032f575507acf0aefd8c41 100644 (file)
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -148,9 +148,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
   // Auto-detect input language by filename extension
   std::string filenameStr("<stdin>");
   if (!inputFromStdin) {
-    // Use swap to avoid copying the string
-    // TODO: use std::move() when switching to c++11
-    filenameStr.swap(filenames[0]);
+    filenameStr = std::move(filenames[0]);
   }
   const char* filename = filenameStr.c_str();
 
@@ -217,20 +215,19 @@ int runCvc5(int argc, char* argv[], Options& opts)
       }
       InteractiveShell shell(pExecutor->getSolver(),
                              pExecutor->getSymbolManager());
-      if (opts.driver.interactivePrompt)
+
+      CVC5Message() << Configuration::getPackageName() << " "
+                    << Configuration::getVersionString();
+      if (Configuration::isGitBuild())
       {
-        CVC5Message() << Configuration::getPackageName() << " "
-                      << Configuration::getVersionString();
-        if(Configuration::isGitBuild()) {
-          CVC5Message() << " [" << Configuration::getGitId() << "]";
-        }
-        CVC5Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
-                      << " assertions:"
-                      << (Configuration::isAssertionBuild() ? "on" : "off")
-                      << endl
-                      << endl;
-        CVC5Message() << Configuration::copyright() << endl;
+        CVC5Message() << " [" << Configuration::getGitId() << "]";
       }
+      CVC5Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
+                    << " assertions:"
+                    << (Configuration::isAssertionBuild() ? "on" : "off")
+                    << endl
+                    << endl;
+      CVC5Message() << Configuration::copyright() << endl;
 
       while(true) {
         try {

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 763692d07d1871a834615211d0fb2cef71ce3c27..7a1ee89ab01e39c36373d25362a320e433bcf005 100644 (file)
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -205,9 +205,7 @@ restart:
   if (d_usingEditline)
   {
 #if HAVE_LIBEDITLINE
-    lineBuf = ::readline(d_options.driver.interactivePrompt
-                             ? (line == "" ? "cvc5> " : "... > ")
-                             : "");
+    lineBuf = ::readline(line == "" ? "cvc5> " : "... > ");
     if(lineBuf != NULL && lineBuf[0] != '\0') {
       ::add_history(lineBuf);
     }
@@ -217,13 +215,13 @@ restart:
   }
   else
   {
-    if (d_options.driver.interactivePrompt)
+    if (line == "")
     {
-      if(line == "") {
-        d_out << "cvc5> " << flush;
-      } else {
-        d_out << "... > " << flush;
-      }
+      d_out << "cvc5> " << flush;
+    }
+    else
+    {
+      d_out << "... > " << flush;
     }
 
     /* Read a line */
@@ -291,8 +289,7 @@ restart:
       if (d_usingEditline)
       {
 #if HAVE_LIBEDITLINE
-        lineBuf = ::readline(d_options.driver.interactivePrompt ? "... > "
-                                                                      : "");
+        lineBuf = ::readline("... > ");
         if(lineBuf != NULL && lineBuf[0] != '\0') {
           ::add_history(lineBuf);
         }
@@ -302,10 +299,7 @@ restart:
       }
       else
       {
-        if (d_options.driver.interactivePrompt)
-        {
-          d_out << "... > " << flush;
-        }
+        d_out << "... > " << flush;
 
         /* Read a line */
         stringbuf sb;

diff --git a/src/options/main_options.toml b/src/options/main_options.toml
index 869d411bdf4d9997ed055f3327d0f7dd981b5e55..55f74f50cf15e38969aafb011cda37af1923b7be 100644 (file)
--- a/src/options/main_options.toml
+++ b/src/options/main_options.toml
@@ -70,15 +70,7 @@ public = true
   category   = "regular"
   long       = "interactive"
   type       = "bool"
-  help       = "force interactive/non-interactive mode"
-
-[[option]]
-  name       = "interactivePrompt"
-  category   = "undocumented"
-  long       = "interactive-prompt"
-  type       = "bool"
-  default    = "true"
-  help       = "interactive prompting while in interactive mode"
+  help       = "force interactive shell/non-interactive mode"
 
 [[option]]
   name       = "segvSpin"