path: root/src/options/strings_options.toml

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       = "stringLB"
  smt_name   = "strings-lb"
  category   = "regular"
  long       = "strings-lb=N"
  type       = "unsigned"
  default    = "0"
  predicates = ["unsignedLessEqual2"]
  read_only  = true
  help       = "the strategy of LB rule application: 0-lazy, 1-eager, 2-no"

[[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       = "stringEIT"
  category   = "regular"
  long       = "strings-eit"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "the eager intersection used by the theory of strings"

[[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       = "stringLenGeqZ"
  category   = "regular"
  long       = "strings-len-geqz"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "strings length greater than zero lemmas"

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

[[option]]
  name       = "stringSplitEmp"
  category   = "regular"
  long       = "strings-sp-emp"
  type       = "bool"
  default    = "true"
  read_only  = true
  help       = "strings split on empty string"

[[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       = "CVC4::theory::strings::ProcessLoopMode"
  default    = "CVC4::theory::strings::ProcessLoopMode::FULL"
  handler    = "stringToStringsProcessLoopMode"
  includes   = ["options/strings_process_loop_mode.h"]
  help       = "choose how to process looping string equations, see --strings-process-loop-mode=help for details"

[[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       = "stringBinaryCsp"
  category   = "regular"
  long       = "strings-binary-csp"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "use binary search when splitting strings"

[[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    = "true"
  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       = "stringsCacheSkolems"
  category   = "expert"
  long       = "strings-cache-skolems"
  type       = "bool"
  default    = "true"
  read_only  = true
  help       = "Cache skolems in string reductions"

[[option]]
  name       = "stringsNormalizeSkolems"
  category   = "expert"
  long       = "strings-normalize-skolems"
  type       = "bool"
  default    = "true"
  read_only  = true
  help       = "Normalize string skolems before looking them up in the cache"

[[option]]
  name       = "stringsRewriterEntailChecks"
  category   = "expert"
  long       = "strings-rewriter-entail-checks"
  type       = "bool"
  default    = "true"
  read_only  = true
  help       = "Enable the entailment checks in the strings rewriter"

[[option]]
  name       = "stringsRewriterApprox"
  category   = "expert"
  long       = "strings-rewriter-entail-approx"
  type       = "bool"
  default    = "true"
  read_only  = true
  help       = "Enable the entailment checks in the strings rewriter"

[[option]]
  name       = "stringsRewriterEntailContainsChecks"
  category   = "expert"
  long       = "strings-rewriter-entail-contains-checks"
  type       = "bool"
  default    = "true"
  read_only  = true
  help       = "Enable the contains entailment checks in the strings rewriter"

[[option]]
  name       = "stringsRewriterMultisetReasoning"
  category   = "expert"
  long       = "strings-rewriter-multiset-reasoning"
  type       = "bool"
  default    = "true"
  read_only  = true
  help       = "Enable multiset reasoning in the strings rewriter"

[[option]]
  name       = "stringsRewriterStripConstantEndpoints"
  category   = "expert"
  long       = "strings-rewriter-strip-constant-endpoints"
  type       = "bool"
  default    = "true"
  read_only  = true
  help       = "Enable stripping of constant endpoints"