diff options
Diffstat (limited to 'src/main')
| -rw-r--r-- | src/main/getopt.cpp | 22 | ||||
| -rw-r--r-- | src/main/main.cpp | 22 | ||||
| -rw-r--r-- | src/main/usage.h | 3 |
3 files changed, 31 insertions, 16 deletions
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 113b8a5f7..8faaefac4 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -30,7 +30,7 @@ #include "util/configuration.h" #include "util/output.h" #include "util/options.h" -#include "parser/parser_options.h" +#include "util/language.h" #include "expr/expr.h" #include "cvc4autoconfig.h" @@ -75,7 +75,8 @@ enum OptionValue { INTERACTIVE, NO_INTERACTIVE, PRODUCE_MODELS, - PRODUCE_ASSIGNMENTS + PRODUCE_ASSIGNMENTS, + NO_EARLY_TYPE_CHECKING };/* enum OptionValue */ /** @@ -127,6 +128,7 @@ static struct option cmdlineOptions[] = { { "no-interactive", no_argument , NULL, NO_INTERACTIVE }, { "produce-models", no_argument , NULL, PRODUCE_MODELS}, { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS}, + { "no-early-type-checking", no_argument, NULL, NO_EARLY_TYPE_CHECKING}, { NULL , no_argument , NULL, '\0' } };/* if you add things to the above, please remember to update usage.h! */ @@ -183,16 +185,16 @@ throw(OptionException) { case 'L': if(!strcmp(optarg, "cvc4") || !strcmp(optarg, "pl")) { - opts->lang = parser::LANG_CVC4; + opts->inputLanguage = language::input::LANG_CVC4; break; } else if(!strcmp(optarg, "smtlib") || !strcmp(optarg, "smt")) { - opts->lang = parser::LANG_SMTLIB; + opts->inputLanguage = language::input::LANG_SMTLIB; break; } else if(!strcmp(optarg, "smtlib2") || !strcmp(optarg, "smt2")) { - opts->lang = parser::LANG_SMTLIB_V2; + opts->inputLanguage = language::input::LANG_SMTLIB_V2; break; } else if(!strcmp(optarg, "auto")) { - opts->lang = parser::LANG_AUTO; + opts->inputLanguage = language::input::LANG_AUTO; break; } @@ -300,12 +302,16 @@ throw(OptionException) { opts->produceAssignments = true; break; + case NO_EARLY_TYPE_CHECKING: + opts->earlyTypeChecking = false; + break; + case SHOW_CONFIG: fputs(Configuration::about().c_str(), stdout); printf("\n"); - printf("version : %s\n", Configuration::getVersionString().c_str()); + printf("version : %s\n", Configuration::getVersionString().c_str()); printf("\n"); - printf("library : %u.%u.%u\n", + printf("library : %u.%u.%u\n", Configuration::getVersionMajor(), Configuration::getVersionMinor(), Configuration::getVersionRelease()); diff --git a/src/main/main.cpp b/src/main/main.cpp index 4f261378d..7fd866112 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -120,7 +120,7 @@ int runCvc4(int argc, char* argv[]) { } // Create the expression manager - ExprManager exprMgr; + ExprManager exprMgr(options.earlyTypeChecking); // Create the SmtEngine SmtEngine smt(&exprMgr, &options); @@ -131,19 +131,19 @@ int runCvc4(int argc, char* argv[]) { ReferenceStat< const char* > s_statFilename("filename", filename); StatisticsRegistry::registerStat(&s_statFilename); - if(options.lang == parser::LANG_AUTO) { + if(options.inputLanguage == language::input::LANG_AUTO) { if( inputFromStdin ) { // We can't do any fancy detection on stdin - options.lang = parser::LANG_CVC4; + options.inputLanguage = language::input::LANG_CVC4; } else { unsigned len = strlen(filename); if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { - options.lang = parser::LANG_SMTLIB_V2; + options.inputLanguage = language::input::LANG_SMTLIB_V2; } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) { - options.lang = parser::LANG_SMTLIB; + options.inputLanguage = language::input::LANG_SMTLIB; } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { - options.lang = parser::LANG_CVC4; + options.inputLanguage = language::input::LANG_CVC4; } } } @@ -167,11 +167,19 @@ int runCvc4(int argc, char* argv[]) { Message.setStream(CVC4::null_os); Warning.setStream(CVC4::null_os); } + + OutputLanguage language = language::toOutputLanguage(options.inputLanguage); + Debug.getStream() << Expr::setlanguage(language); + Trace.getStream() << Expr::setlanguage(language); + Notice.getStream() << Expr::setlanguage(language); + Chat.getStream() << Expr::setlanguage(language); + Message.getStream() << Expr::setlanguage(language); + Warning.getStream() << Expr::setlanguage(language); } ParserBuilder parserBuilder = ParserBuilder(exprMgr, filename) - .withInputLanguage(options.lang) + .withInputLanguage(options.inputLanguage) .withMmap(options.memoryMap) .withChecks(options.semanticChecks && !Configuration::isMuzzledBuild() ) diff --git a/src/main/usage.h b/src/main/usage.h index 15a30a426..ed35e76e8 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -51,7 +51,8 @@ CVC4 options:\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"; + --lazy-definition-expansion expand define-fun lazily\n\ + --no-early-type-checking don't typecheck at Expr creation [non-DEBUG builds never do]\n"; }/* CVC4::main namespace */ }/* CVC4 namespace */ |