id     = "STRINGS"
name   = "Strings theory"
header = "options/strings_options.h"

[[option]]
  name       = "stringExp"
  category   = "regular"
  long       = "strings-exp"
  type       = "bool"
  default    = "false"
  help       = "experimental features in the theory of strings"

[[option]]
  name       = "stdPrintASCII"
  category   = "regular"
  long       = "strings-print-ascii"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "the alphabet contains only printable characters from the standard extended ASCII"

[[option]]
  name       = "stringFMF"
  category   = "regular"
  long       = "strings-fmf"
  type       = "bool"
  default    = "false"
  help       = "the finite model finding used by the theory of strings"

[[option]]
  name       = "stringEager"
  category   = "regular"
  long       = "strings-eager"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "strings eager check"

[[option]]
  name       = "stringIgnNegMembership"
  category   = "regular"
  long       = "strings-inm"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "internal for strings: ignore negative membership constraints (fragment checking is needed, left to users for now)"

[[option]]
  name       = "stringLazyPreproc"
  category   = "regular"
  long       = "strings-lazy-pp"
  type       = "bool"
  default    = "true"
  read_only  = true
  help       = "perform string preprocessing lazily"

[[option]]
  name       = "stringLenNorm"
  category   = "regular"
  long       = "strings-len-norm"
  type       = "bool"
  default    = "true"
  read_only  = true
  help       = "strings length normalization lemma"

[[option]]
  name       = "stringInferSym"
  category   = "regular"
  long       = "strings-infer-sym"
  type       = "bool"
  default    = "true"
  read_only  = true
  help       = "strings split on empty string"

[[option]]
  name       = "stringEagerLen"
  category   = "regular"
  long       = "strings-eager-len"
  type       = "bool"
  default    = "true"
  read_only  = true
  help       = "strings eager length lemmas"

[[option]]
  name       = "stringCheckEntailLen"
  category   = "regular"
  long       = "strings-check-entail-len"
  type       = "bool"
  default    = "true"
  read_only  = true
  help       = "check entailment between length terms to reduce splitting"

[[option]]
  name       = "stringProcessLoopMode"
  category   = "expert"
  long       = "strings-process-loop-mode=MODE"
  type       = "ProcessLoopMode"
  default    = "FULL"
  help       = "determines how to process looping string equations"
  help_mode = "Loop processing modes."
[[option.mode.FULL]]
  name = "full"
  help = "Perform full processing of looping word equations."
[[option.mode.SIMPLE]]
  name = "simple"
  help = "Omit normal loop breaking (default with --strings-fmf)."
[[option.mode.SIMPLE_ABORT]]
  name = "simple-abort"
  help = "Abort when normal loop breaking is required."
[[option.mode.NONE]]
  name = "none"
  help = "Omit loop processing."
[[option.mode.ABORT]]
  name = "abort"
  help = "Abort if looping word equations are encountered."


[[option]]
  name       = "stringInferAsLemmas"
  category   = "regular"
  long       = "strings-infer-as-lemmas"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "always send lemmas out instead of making internal inferences"

[[option]]
  name       = "stringRExplainLemmas"
  category   = "regular"
  long       = "strings-rexplain-lemmas"
  type       = "bool"
  default    = "true"
  read_only  = true
  help       = "regression explanations for string lemmas"

[[option]]
  name       = "stringMinPrefixExplain"
  category   = "regular"
  long       = "strings-min-prefix-explain"
  type       = "bool"
  default    = "true"
  read_only  = true
  help       = "minimize explanations for prefix of normal forms in strings"

[[option]]
  name       = "stringGuessModel"
  category   = "regular"
  long       = "strings-guess-model"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "use model guessing to avoid string extended function reductions"

[[option]]
  name       = "stringLenPropCsp"
  category   = "regular"
  long       = "strings-lprop-csp"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "do length propagation based on constant splits"

[[option]]
  name       = "regExpElim"
  category   = "regular"
  long       = "re-elim"
  type       = "bool"
  default    = "false"
  help       = "elimination techniques for regular expressions"

[[option]]
  name       = "regExpElimAgg"
  category   = "regular"
  long       = "re-elim-agg"
  type       = "bool"
  default    = "false"
  help       = "aggressive elimination techniques for regular expressions"

[[option]]
  name       = "stringFlatForms"
  category   = "regular"
  long       = "strings-ff"
  type       = "bool"
  default    = "true"
  read_only  = true
  help       = "do flat form inferences"

[[option]]
  name       = "stringRegExpInterMode"
  category   = "expert"
  long       = "re-inter-mode=MODE"
  type       = "RegExpInterMode"
  default    = "CONSTANT"
  help       = "determines which regular expressions intersections to compute"
  help_mode  = "Regular expression intersection modes."
[[option.mode.ALL]]
  name = "all"
  help = "Compute intersections for all regular expressions."
[[option.mode.CONSTANT]]
  name = "constant"
  help = "Compute intersections only between regular expressions that do not contain re.allchar or re.range."
[[option.mode.ONE_CONSTANT]]
  name = "one-constant"
  help = "Compute intersections only between regular expressions such that at least one side does not contain re.allchar or re.range."
[[option.mode.NONE]]
  name = "none"
  help = "Do not compute intersections for regular expressions."

[[option]]
  name       = "stringUnifiedVSpt"
  category   = "regular"
  long       = "strings-unified-vspt"
  type       = "bool"
  default    = "true"
  read_only  = true
  help       = "use a single skolem for the variable splitting rule"

[[option]]
  name       = "stringLenConc"
  category   = "regular"
  long       = "strings-len-conc"
  type       = "bool"
  default    = "false"
  help       = "add skolem length constraints in conclusions of inferences"

[[option]]
  name       = "stringEagerEval"
  category   = "regular"
  long       = "strings-eager-eval"
  type       = "bool"
  default    = "true"
  help       = "perform eager context-dependent evaluation for applications of string kinds"