diff options
Diffstat (limited to 'src/options/expr_options')
-rw-r--r-- | src/options/expr_options | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/src/options/expr_options b/src/options/expr_options new file mode 100644 index 000000000..fc92c75a6 --- /dev/null +++ b/src/options/expr_options @@ -0,0 +1,33 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module EXPR "options/expr_options.h" Expression package + +option defaultExprDepth --default-expr-depth=N int :default 0 :predicate CVC4::options::setDefaultExprDepth :predicate-include "options/options_handler_interface.h" + print exprs to depth N (0 == default, -1 == no limit) +undocumented-alias --expr-depth=N = --default-expr-depth=N + +option defaultDagThresh default-dag-thresh --default-dag-thresh=N int :default 1 :predicate CVC4::options::setDefaultDagThresh :predicate-include "options/options_handler_interface.h" + dagify common subexprs appearing > N times (1 == default, 0 == don't dagify) +undocumented-alias --dag-thresh=N = --default-dag-thresh=N +undocumented-alias --dag-threshold=N = --default-dag-thresh=N + +option - --print-expr-types void :handler CVC4::options::setPrintExprTypes :handler-include "options/options_handler_interface.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 + |