diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-10-28 20:30:24 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-10-28 20:30:24 +0000 |
commit | 890bacd7cb11c6e991722e8a7b7cd0ef9147ea3b (patch) | |
tree | 0c2f05f224fe79310130dc054c7606144e248de0 /src/main | |
parent | b084a7efa9d65ec2f7475caa8486f8fd4cbafbd5 (diff) |
* ability to output NodeBuilders without first converting them to Nodes---useful for debugging.
* language-dependent Node::toString()
* some minor proof-related cleanup
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/Makefile.am | 1 | ||||
-rw-r--r-- | src/main/usage.h | 63 |
2 files changed, 0 insertions, 64 deletions
diff --git a/src/main/Makefile.am b/src/main/Makefile.am index da3b5896a..78d468000 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -11,7 +11,6 @@ libmain_a_SOURCES = \ interactive_shell.cpp \ main.h \ main.cpp \ - usage.h \ util.cpp cvc4_SOURCES = diff --git a/src/main/usage.h b/src/main/usage.h deleted file mode 100644 index f0c7c7f08..000000000 --- a/src/main/usage.h +++ /dev/null @@ -1,63 +0,0 @@ -/********************* */ -/*! \file usage.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): cconway - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief The "usage" string for the CVC4 driver binary. - ** - ** The "usage" string for the CVC4 driver binary. - **/ - -#ifndef __CVC4__MAIN__USAGE_H -#define __CVC4__MAIN__USAGE_H - -namespace CVC4 { -namespace main { - -// no more % chars in here without being escaped; it's used as a -// printf() format string -const char usage[] = "\ -usage: %s [options] [input-file]\n\ -\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\ - --segv-nospin don't spin on segfault waiting for gdb\n\ - --lazy-type-checking type check expressions only when necessary (default)\n\ - --eager-type-checking type check expressions immediately on creation\n\ - --no-type-checking never type check expressions\n\ - --no-checking disable ALL semantic checks, including type checks \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\ - --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\ - --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 - --proof\n"; - -}/* CVC4::main namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__MAIN__USAGE_H */ |