diff options
| -rw-r--r-- | src/main/driver_unified.cpp | 27 | ||||
| -rw-r--r-- | src/main/interactive_shell.cpp | 24 | ||||
| -rw-r--r-- | src/options/main_options.toml | 10 |
3 files changed, 22 insertions, 39 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 8c86f03cb..606f18095 100644 --- 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 763692d07..7a1ee89ab 100644 --- 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 869d411bd..55f74f50c 100644 --- 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" |