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...

1 files changed, 15 insertions, 1 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");