From: Christopher L. Conway Date: Wed, 20 Oct 2010 21:49:34 +0000 (+0000) Subject: Changing --no-early-type-checking to --no-type-checking X-Git-Tag: cvc5-1.0.0~8794 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=91829206b4783a532453eab3c69de83b8b510286;p=cvc5.git Changing --no-early-type-checking to --no-type-checking Disabling type checking when --no-checking is given (Fixes: #221) --- diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 57aa84a57..5ddeced5d 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -128,7 +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}, + { "no-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! */ diff --git a/src/main/main.cpp b/src/main/main.cpp index fd7c1b303..8f790c211 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -123,15 +123,18 @@ int runCvc4(int argc, char* argv[]) { const bool inputFromStdin = firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]); - // if we're reading from stdin, default to interactive mode - // [chris 10/20/10] The expected behavior of interactive is - // different from the expected behavior of file input from - // stdin, due to EOL escapes in interactive mode - + // if we're reading from stdin on a TTY, default to interactive mode if(!options.interactiveSetByUser) { options.interactive = inputFromStdin && isatty(fileno(stdin)); } + /* Early type checking can be turned off by --no-type-checking OR + --no-checking. We're assuming that earlyTypeChecking is not + explicitly set by the user. */ + if(options.earlyTypeChecking) { + options.earlyTypeChecking = options.semanticChecks; + } + // Create the expression manager ExprManager exprMgr(options.earlyTypeChecking); diff --git a/src/main/usage.h b/src/main/usage.h index ed35e76e8..7affc254c 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -38,7 +38,8 @@ CVC4 options:\n\ --show-config show CVC4 static configuration\n\ --segv-nospin don't spin on segfault waiting for gdb\n\ --no-checking disable semantic checks in the parser\n\ - --strict-parsing fail on inputs that are not strictly conformant (SMT2 only)\n\ + --no-type-checking disable type checking [default in non-debug builds]\n\ + --strict-parsing fail on non-conformant inputs (SMT2 only)\n\ --verbose | -v increase verbosity (repeatable)\n\ --quiet | -q decrease verbosity (repeatable)\n\ --trace | -t tracing for something (e.g. --trace pushpop)\n\ @@ -51,8 +52,7 @@ 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\ - --no-early-type-checking don't typecheck at Expr creation [non-DEBUG builds never do]\n"; + --lazy-definition-expansion expand define-fun lazily\n"; }/* CVC4::main namespace */ }/* CVC4 namespace */