parser and core support for SMT-LIBv2 commands get-info, set-option, get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...

2 files changed, 33 insertions, 13 deletions

diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 08bcbaa7c..4af882aa1 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -70,7 +70,9 @@ enum OptionValue {
   STRICT_PARSING,
   DEFAULT_EXPR_DEPTH,
   PRINT_EXPR_TYPES,
-  UF_THEORY
+  UF_THEORY,
+  INTERACTIVE,
+  NO_INTERACTIVE
 };/* enum OptionValue */
 
 /**
@@ -117,6 +119,8 @@ static struct option cmdlineOptions[] = {
   { "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH },
   { "print-expr-types", no_argument , NULL, PRINT_EXPR_TYPES },
   { "uf"         , required_argument, NULL, UF_THEORY },
+  { "interactive", no_argument      , NULL, INTERACTIVE },
+  { "no-interactive", no_argument   , NULL, NO_INTERACTIVE },
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
 
@@ -268,6 +272,16 @@ throw(OptionException) {
       }
       break;
 
+    case INTERACTIVE:
+      opts->interactive = true;
+      opts->interactiveSetByUser = true;
+      break;
+
+    case NO_INTERACTIVE:
+      opts->interactive = false;
+      opts->interactiveSetByUser = true;
+      break;
+
     case SHOW_CONFIG:
       fputs(Configuration::about().c_str(), stdout);
       printf("\n");
diff --git a/src/main/main.cpp b/src/main/main.cpp
index f0c04e5f6..4f261378d 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -110,20 +110,25 @@ int runCvc4(int argc, char* argv[]) {
     throw Exception("Too many input files specified.");
   }
 
+  // If no file supplied we will read from standard input
+  const bool inputFromStdin =
+    firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]);
+
+  // if we're reading from stdin, default to interactive mode
+  if(!options.interactiveSetByUser) {
+    options.interactive = inputFromStdin;
+  }
+
   // Create the expression manager
   ExprManager exprMgr;
 
   // Create the SmtEngine
   SmtEngine smt(&exprMgr, &options);
 
-  // If no file supplied we read from standard input
-  bool inputFromStdin =
-    firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]);
-
   // Auto-detect input language by filename extension
   const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
 
-  ReferenceStat< const char* > s_statFilename("filename",filename);
+  ReferenceStat< const char* > s_statFilename("filename", filename);
   StatisticsRegistry::registerStat(&s_statFilename);
 
   if(options.lang == parser::LANG_AUTO) {
@@ -180,6 +185,9 @@ int runCvc4(int argc, char* argv[]) {
 
   // Parse and execute commands until we are done
   Command* cmd;
+  if( options.interactive ) {
+    // cout << "CVC4> " << flush;
+  }
   while((cmd = parser->nextCommand())) {
     if( !options.parseOnly ) {
       doCommand(smt, cmd);
@@ -238,21 +246,19 @@ void doCommand(SmtEngine& smt, Command* cmd) {
       cout << "Invoking: " << *cmd << endl;
     }
 
-    cmd->invoke(&smt);
+    if(options.verbosity >= 0) {
+      cmd->invoke(&smt, cout);
+    } else {
+      cmd->invoke(&smt);
+    }
 
     QueryCommand *qc = dynamic_cast<QueryCommand*>(cmd);
     if(qc != NULL) {
       lastResult = qc->getResult();
-      if(options.verbosity >= 0) {
-        cout << lastResult << endl;
-      }
     } else {
       CheckSatCommand *csc = dynamic_cast<CheckSatCommand*>(cmd);
       if(csc != NULL) {
         lastResult = csc->getResult();
-        if(options.verbosity >= 0) {
-          cout << lastResult << endl;
-        }
       }
     }
   }