diff options
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/getopt.cpp | 14 | ||||
-rw-r--r-- | src/main/usage.h | 8 |
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 */ |