diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-08 23:12:28 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-08 23:12:28 +0000 |
commit | e63abd23b45a078a42cafb277a4817abb4d044a1 (patch) | |
tree | 43b8aaccc9b49887280e0c77471c5346eb1cf9c4 /src/main | |
parent | fccdb4cbe2cde7c34e82f33e9de850a046fef888 (diff) |
* (define-fun...) now has proper type checking in non-debug builds
(resolves bug #212)
* also closed some other type checking loopholes in SmtEngine
* small fixes to define-sort (resolves bug #214)
* infrastructural support for printing expressions in languages
other than the internal representation language using an IO
manipulator, e.g.:
cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << expr;
main() sets the output language for all streams to correspond to
the input language
* support delaying type checking in debug builds, so that one can debug
the type checker itself (before it was difficult, because debug builds did
all the type checking on Node creation!): new command-line flag
--no-early-type-checking (only makes sense for debug builds)
* disallowed copy-construction of ExprManager and NodeManager, and made other
constructors explicit; previously it was easy to unintentionally create
duplicate managers, with really weird results (i.e., disappearing
attributes!)
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 */ |