blob: ee4d40b2cf3befb12e0fc5c0f50cd8c1814f9615 (
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
|
#
# Option specification file for CVC4
# See src/options/base_options for a description of this file format
#
module EXPR "expr/options.h" Expression package
option defaultExprDepth --default-expr-depth=N int :default 0 :predicate CVC4::expr::setDefaultExprDepth :predicate-include "expr/options_handlers.h"
print exprs to depth N (0 == default, -1 == no limit)
undocumented-alias --expr-depth = --default-expr-depth
option defaultDagThresh default-dag-thresh --default-dag-thresh=N int :default 1 :predicate CVC4::expr::setDefaultDagThresh :predicate-include "expr/options_handlers.h"
dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)
undocumented-alias --dag-thresh = --default-dag-thresh
undocumented-alias --dag-threshold = --default-dag-thresh
option - --print-expr-types void :handler CVC4::expr::setPrintExprTypes :handler-include "expr/options_handlers.h"
print types with variables when printing exprs
option earlyTypeChecking --eager-type-checking/--lazy-type-checking bool :default USE_EARLY_TYPE_CHECKING_BY_DEFAULT
type check expressions immediately on creation (debug builds only)
/type check expressions only when necessary (default)
# --no-type-checking will override any --early-type-checking or --lazy-type-checking option
# --lazy-type-checking is linked because earlyTypeChecking should be set false too
option typeChecking /--no-type-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--lazy-type-checking
never type check expressions
option biasedITERemoval --biased-ites bool :default false
try the new remove ite pass that is biased against term ites appearing
endmodule
|
