diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-07-02 00:09:52 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-07-02 00:09:52 +0000 |
commit | 83a143b1dd78e5d7f07666fbec1362dd60348116 (patch) | |
tree | 08400222d94f4760c7155fea787ac7e78b7b0dfc /src/main | |
parent | a8566c313e9b5eb8248eaeea642a9c72c803dcfa (diff) |
* Added white-box TheoryEngine test that tests the rewriter
* Added regression documentation to test/regress/README
* Added ability to print types of vars in expr printouts
with iomanipulator Node::printtypes(true)... for example,
Warning() << Node::printtypes(true) << n << std::endl;
* Types-printing can be specified on the command line with
--print-expr-types
* Improved type handling facilities and theoryOf().
For now, SORT_TYPE moved from builtin theory to UF theory
to match old behavior.
* Additional gdb debug functionality. Now we have:
debugPrintNode(Node) debugPrintRawNode(Node)
debugPrintTNode(TNode) debugPrintRawTNode(TNode)
debugPrintTypeNode(TypeNode) debugPrintRawTypeNode(TypeNode)
debugPrintNodeValue(NodeValue*) debugPrintRawNodeValue(NodeValue*)
they all print a {Node,TNode,NodeValue*} from the debugger.
The "Raw" versions print a very low-level AST-like form.
The regular versions do the same as operator<<, but force
full printing on (no depth-limiting).
* Other trivial fixes
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/getopt.cpp | 15 | ||||
-rw-r--r-- | src/main/usage.h | 37 |
2 files changed, 30 insertions, 22 deletions
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 88840a8e8..e050a0dfb 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -68,7 +68,8 @@ enum OptionValue { USE_MMAP, SHOW_CONFIG, STRICT_PARSING, - DEFAULT_EXPR_DEPTH + DEFAULT_EXPR_DEPTH, + PRINT_EXPR_TYPES };/* enum OptionValue */ /** @@ -113,6 +114,7 @@ static struct option cmdlineOptions[] = { { "mmap", no_argument , NULL, USE_MMAP }, { "strict-parsing", no_argument , NULL, STRICT_PARSING }, { "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH }, + { "print-expr-types", no_argument , NULL, PRINT_EXPR_TYPES }, };/* if you add things to the above, please remember to update usage.h! */ /** Full argv[0] */ @@ -234,6 +236,17 @@ throw(OptionException) { } break; + case PRINT_EXPR_TYPES: + { + Debug.getStream() << Expr::printtypes(true); + Trace.getStream() << Expr::printtypes(true); + Notice.getStream() << Expr::printtypes(true); + Chat.getStream() << Expr::printtypes(true); + Message.getStream() << Expr::printtypes(true); + Warning.getStream() << Expr::printtypes(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 ef37b7650..b56f083a5 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -30,27 +30,22 @@ usage: %s [options] [input-file]\n\ Without an input file, or with `-', CVC4 reads from standard input.\n\ \n\ CVC4 options:\n\ - --lang | -L force input language (default is `auto'; see --lang help)\n\ - --version | -V identify this CVC4 binary\n\ - --help | -h this command line reference\n\ - --parse-only exit after parsing input\n\ - --mmap memory map file input\n\ - --show-config show CVC4 static configuration\n" -#ifdef CVC4_DEBUG -"\ - --segv-nospin don't spin on segfault waiting for gdb\n" -#endif -#ifndef CVC4_MUZZLE -"\ - --no-checking disable semantic checks in the parser\n\ - --strict-parsing fail on inputs that are not strictly conformant (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\ - --debug | -d debugging for something (e.g. --debug arith), implies -t\n\ - --stats give statistics on exit\n\ - --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n" -#endif + --lang | -L force input language (default is `auto'; see --lang help)\n\ + --version | -V identify this CVC4 binary\n\ + --help | -h this command line reference\n\ + --parse-only exit after parsing input\n\ + --mmap memory map file input\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\ + --verbose | -v increase verbosity (repeatable)\n\ + --quiet | -q decrease verbosity (repeatable)\n\ + --trace | -t tracing for something (e.g. --trace pushpop)\n\ + --debug | -d debugging for something (e.g. --debug arith), implies -t\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" ; }/* CVC4::main namespace */ |