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
+