diff options
Diffstat (limited to 'src/options/strings_options')
| -rw-r--r-- | src/options/strings_options | 76 |
1 files changed, 0 insertions, 76 deletions
diff --git a/src/options/strings_options b/src/options/strings_options deleted file mode 100644 index 6dd7030a1..000000000 --- a/src/options/strings_options +++ /dev/null @@ -1,76 +0,0 @@ -# -# Option specification file for CVC4 -# See src/options/base_options for a description of this file format -# - -module STRINGS "options/strings_options.h" Strings theory - -option stringExp strings-exp --strings-exp bool :default false :read-write - experimental features in the theory of strings - -# :predicate-include "smt/smt_engine.h" -option stringLB strings-lb --strings-lb=N unsigned :default 0 :predicate unsignedLessEqual2 - the strategy of LB rule application: 0-lazy, 1-eager, 2-no - -# :predicate-include "smt/smt_engine.h" -option stdASCII strings-std-ascii --strings-std-ascii bool :default true :predicate unsignedLessEqual2 - the alphabet contains only characters from the standard ASCII or the extended one - -option stringFMF strings-fmf --strings-fmf bool :default false :read-write - the finite model finding used by the theory of strings - -option stringEager strings-eager --strings-eager bool :default false - strings eager check - -option stringEIT strings-eit --strings-eit bool :default false - the eager intersection used by the theory of strings - -option stringOpt1 strings-opt1 --strings-opt1 bool :default true - internal option1 for strings: normal form - -option stringOpt2 strings-opt2 --strings-opt2 bool :default false - internal option2 for strings: constant regexp splitting - -option stringIgnNegMembership strings-inm --strings-inm bool :default false - internal for strings: ignore negative membership constraints (fragment checking is needed, left to users for now) - -#expert-option stringCharCardinality strings-alphabet-card --strings-alphabet-card=N int16_t :default 128 :read-write -# the cardinality of the characters used by the theory of strings, default 128 (for standard ASCII) or 256 (for extended ASCII) - -option stringLazyPreproc strings-lazy-pp --strings-lazy-pp bool :default true - perform string preprocessing lazily - -option stringLenGeqZ strings-len-geqz --strings-len-geqz bool :default false - strings length greater than zero lemmas - -option stringLenNorm strings-len-norm --strings-len-norm bool :default true - strings length normalization lemma -option stringSplitEmp strings-sp-emp --strings-sp-emp bool :default true - strings split on empty string -option stringInferSym strings-infer-sym --strings-infer-sym bool :default true - strings split on empty string -option stringEagerLen strings-eager-len --strings-eager-len bool :default true - strings eager length lemmas -option stringCheckEntailLen strings-check-entail-len --strings-check-entail-len bool :default true - check entailment between length terms to reduce splitting -option stringProcessLoop strings-process-loop --strings-process-loop bool :default true - reduce looping word equations to regular expressions -option stringAbortLoop strings-abort-loop --strings-abort-loop bool :default false - abort when a looping word equation is encountered -option stringInferAsLemmas strings-infer-as-lemmas --strings-infer-as-lemmas bool :default false - always send lemmas out instead of making internal inferences -option stringRExplainLemmas strings-rexplain-lemmas --strings-rexplain-lemmas bool :default true - regression explanations for string lemmas -option stringMinPrefixExplain strings-min-prefix-explain --strings-min-prefix-explain bool :default true - minimize explanations for prefix of normal forms in strings -option stringGuessModel strings-guess-model --strings-guess-model bool :default false - use model guessing to avoid string extended function reductions -option stringUfReduct strings-uf-reduct --strings-uf-reduct bool :default false - use uninterpreted functions when applying extended function reductions -option stringBinaryCsp strings-binary-csp --strings-binary-csp bool :default false - use binary search when splitting strings -option stringLenPropCsp strings-lprop-csp --strings-lprop-csp bool :default false - do length propagation based on constant splits - - -endmodule |