Partial merge from kind-backend branch, including Minisat and CNF work to

support incrementality.

Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.

Expected performance change negligible; slightly better on memory:
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!

1 files changed, 11 insertions, 7 deletions

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index a63d6c67b..d8e7df2f2 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -83,7 +83,7 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
                                    const Options& options) :
   d_in(*options.in),
   d_out(*options.out),
-  d_language(options.inputLanguage),
+  d_options(options),
   d_quit(false) {
   ParserBuilder parserBuilder(&exprManager, INPUT_FILENAME, options);
   /* Create parser with bogus input. */
@@ -95,7 +95,7 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
     ::rl_completion_entry_function = commandGenerator;
     ::using_history();
 
-    switch(OutputLanguage lang = toOutputLanguage(d_language)) {
+    switch(OutputLanguage lang = toOutputLanguage(d_options.inputLanguage)) {
     case output::LANG_CVC4:
       d_historyFilename = string(getenv("HOME")) + "/.cvc4_history";
       commandsBegin = cvc_commands;
@@ -166,7 +166,7 @@ Command* InteractiveShell::readCommand() {
   /* Prompt the user for input. */
   if(d_usingReadline) {
 #if HAVE_LIBREADLINE
-    lineBuf = ::readline("CVC4> ");
+    lineBuf = ::readline(d_options.verbosity >= 0 ? "CVC4> " : "");
     if(lineBuf != NULL && lineBuf[0] != '\0') {
       ::add_history(lineBuf);
     }
@@ -174,7 +174,9 @@ Command* InteractiveShell::readCommand() {
     free(lineBuf);
 #endif /* HAVE_LIBREADLINE */
   } else {
-    d_out << "CVC4> " << flush;
+    if(d_options.verbosity >= 0) {
+      d_out << "CVC4> " << flush;
+    }
 
     /* Read a line */
     d_in.get(sb,'\n');
@@ -229,7 +231,7 @@ Command* InteractiveShell::readCommand() {
       input[n] = '\n';
       if(d_usingReadline) {
 #if HAVE_LIBREADLINE
-        lineBuf = ::readline("... > ");
+        lineBuf = ::readline(d_options.verbosity >= 0 ? "... > " : "");
         if(lineBuf != NULL && lineBuf[0] != '\0') {
           ::add_history(lineBuf);
         }
@@ -237,7 +239,9 @@ Command* InteractiveShell::readCommand() {
         free(lineBuf);
 #endif /* HAVE_LIBREADLINE */
       } else {
-        d_out << "... > " << flush;
+        if(d_options.verbosity >= 0) {
+          d_out << "... > " << flush;
+        }
 
         /* Read a line */
         d_in.get(sb,'\n');
@@ -250,7 +254,7 @@ Command* InteractiveShell::readCommand() {
     }
   }
 
-  d_parser->setInput(Input::newStringInput(d_language,input,INPUT_FILENAME));
+  d_parser->setInput(Input::newStringInput(d_options.inputLanguage, input, INPUT_FILENAME));
 
   /* There may be more than one command in the input. Build up a
      sequence. */