summaryrefslogtreecommitdiff
path: root/src/main/usage.h
blob: edc9ad1d18b4477b697b3468a39fdaf8cf908600 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
#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     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__MAIN__USAGE_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback