type checking for define-fun in production builds; related to (and might resolve) bug 212

2 files changed, 19 insertions, 3 deletions

diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 82214bed3..113b8a5f7 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -73,7 +73,9 @@ enum OptionValue {
   UF_THEORY,
   LAZY_DEFINITION_EXPANSION,
   INTERACTIVE,
-  NO_INTERACTIVE
+  NO_INTERACTIVE,
+  PRODUCE_MODELS,
+  PRODUCE_ASSIGNMENTS
 };/* enum OptionValue */
 
 /**
@@ -123,6 +125,8 @@ static struct option cmdlineOptions[] = {
   { "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION },
   { "interactive", no_argument      , NULL, INTERACTIVE },
   { "no-interactive", no_argument   , NULL, NO_INTERACTIVE },
+  { "produce-models", no_argument   , NULL, PRODUCE_MODELS},
+  { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS},
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
 
@@ -288,6 +292,14 @@ throw(OptionException) {
       opts->interactiveSetByUser = true;
       break;
 
+    case PRODUCE_MODELS:
+      opts->produceModels = true;
+      break;
+
+    case PRODUCE_ASSIGNMENTS:
+      opts->produceAssignments = true;
+      break;
+
     case SHOW_CONFIG:
       fputs(Configuration::about().c_str(), stdout);
       printf("\n");
diff --git a/src/main/usage.h b/src/main/usage.h
index 2be5f092e..15a30a426 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -46,8 +46,12 @@ CVC4 options:\n\
    --stats                give statistics on exit\n\
    --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\
    --print-expr-types     print types with variables when printing exprs\n\
-   --uf=morgan|tim        select uninterpreted function theory implementation\n"
-;
+   --uf=morgan|tim        select uninterpreted function theory implementation\n\
+   --interactive          run interactively\n\
+   --no-interactive       do not run interactively\n\
+   --produce-models       support the get-value command\n\
+   --produce-assignments  support the get-assignment command\n\
+   --lazy-definition-expansion expand define-fun lazily\n";
 
 }/* CVC4::main namespace */
 }/* CVC4 namespace */