1 files changed, 74 insertions, 0 deletions
diff --git a/src/options/expr_options.toml b/src/options/expr_options.toml
new file mode 100644
index 000000000..3791da714
--- /dev/null
+++ b/src/options/expr_options.toml
@@ -0,0 +1,74 @@
+id     = "EXPR"
+name   = "Expression package"
+header = "options/expr_options.h"
+
+[[option]]
+  name       = "defaultExprDepth"
+  category   = "regular"
+  long       = "default-expr-depth=N"
+  type       = "int"
+  default    = "0"
+  predicates = ["setDefaultExprDepthPredicate"]
+  notifies   = ["notifySetDefaultExprDepth"]
+  read_only  = true
+  help       = "print exprs to depth N (0 == default, -1 == no limit)"
+
+[[alias]]
+  category   = "undocumented"
+  long       = "expr-depth=N"
+  links      = ["--default-expr-depth=N"]
+
+[[option]]
+  name       = "defaultDagThresh"
+  smt_name   = "default-dag-thresh"
+  category   = "regular"
+  long       = "default-dag-thresh=N"
+  type       = "int"
+  default    = "1"
+  predicates = ["setDefaultDagThreshPredicate"]
+  notifies   = ["notifySetDefaultDagThresh"]
+  read_only  = true
+  help       = "dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)"
+
+[[alias]]
+  category   = "undocumented"
+  long       = "dag-thresh=N"
+  links      = ["--default-dag-thresh=N"]
+
+[[alias]]
+  category   = "undocumented"
+  long       = "dag-threshold=N"
+  links      = ["--default-dag-thresh=N"]
+
+[[option]]
+  name       = "printExprTypes"
+  category   = "regular"
+  long       = "print-expr-types"
+  type       = "bool"
+  default    = "false"
+  notifies   = ["notifySetPrintExprTypes"]
+  read_only  = true
+  help       = "print types with variables when printing exprs"
+
+[[option]]
+  name       = "earlyTypeChecking"
+  category   = "regular"
+  long       = "eager-type-checking"
+  type       = "bool"
+  default    = "USE_EARLY_TYPE_CHECKING_BY_DEFAULT"
+  read_only  = true
+  help       = "type check expressions immediately on creation (debug builds only)"
+
+[[option]]
+  name       = "typeChecking"
+  category   = "regular"
+  long       = "type-checking"
+  type       = "bool"
+  default    = "DO_SEMANTIC_CHECKS_BY_DEFAULT"
+  read_only  = true
+  help       = "never type check expressions"
+
+[[alias]]
+  category   = "undocumented"
+  long       = "no-type-checking"
+  links      = ["--no-eager-type-checking"]