diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-18 22:02:11 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-18 22:02:11 +0000 |
commit | 394791604a62e19763a8a45328bc5177d91fabf9 (patch) | |
tree | 29027c84c0285da33bac6c5d1366635b9e4db1bc /src/main/usage.h | |
parent | 477e97cd81afe4b86eea47e9abe6311fc22299fc (diff) |
work on exprs, driver, util
Diffstat (limited to 'src/main/usage.h')
-rw-r--r-- | src/main/usage.h | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/src/main/usage.h b/src/main/usage.h new file mode 100644 index 000000000..971ba7640 --- /dev/null +++ b/src/main/usage.h @@ -0,0 +1,29 @@ +#ifndef __CVC4_USAGE_H +#define __CVC4_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 set input language (--lang help gives a list;\n\ + `auto' is default)\n\ + --version | -V identify this CVC4 binary\n\ + --help | -h this command line reference\n\ + --verbose | -v increase verbosity (repeatable)\n\ + --quiet | -q decrease verbosity (repeatable)\n\ + --debug | -d debugging for something (e.g. --debug arith)\n\ + --smtcomp competition mode (very quiet)\n\ + --stats give statistics on exit\n\ +"; + +}/* CVC4::Main namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4_USAGE_H */ |