blob: 433e6f613b77ce39bfeeae4ee38f2cdf667d7117 (
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
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
|
id = "PRINTER"
name = "Printing"
[[option]]
name = "modelFormatMode"
category = "regular"
long = "model-format=MODE"
type = "ModelFormatMode"
default = "DEFAULT"
help = "print format mode for models, see --model-format=help"
help_mode = "Model format modes."
[[option.mode.DEFAULT]]
name = "default"
help = "Print model as expressions in the output language format."
[[option.mode.TABLE]]
name = "table"
help = "Print functional expressions over finite domains in a table format."
[[option]]
name = "instFormatMode"
category = "regular"
long = "inst-format=MODE"
type = "InstFormatMode"
default = "InstFormatMode::DEFAULT"
handler = "stringToInstFormatMode"
includes = ["options/printer_modes.h"]
help = "print format mode for instantiations, see --inst-format=help"
# InstFormatMode is currently exported as public so we can't auto genenerate
# the enum.
# help_mode = "Inst format modes."
#[[option.mode.DEFAULT]]
# name = "default"
# help = "Print instantiations as a list in the output language format."
#[[option.mode.SZS]]
# name = "szs"
# help = "Print instantiations as SZS compliant proof."
[[option]]
name = "flattenHOChains"
category = "regular"
long = "flatten-ho-chains"
type = "bool"
default = "false"
help = "print (binary) application chains in a flattened way, e.g. (a b c) rather than ((a b) c)"
[[option]]
name = "printInstMode"
category = "regular"
long = "print-inst=MODE"
type = "PrintInstMode"
default = "LIST"
help = "print format for printing instantiations"
help_mode = "Print format for printing instantiations."
[[option.mode.LIST]]
name = "list"
help = "Print the list of instantiations per quantified formula, when non-empty."
[[option.mode.NUM]]
name = "num"
help = "Print the total number of instantiations per quantified formula, when non-zero."
[[option]]
name = "printInstFull"
category = "regular"
long = "print-inst-full"
type = "bool"
default = "true"
help = "print instantiations for formulas that do not have given identifiers"
|