diff options
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/options | 56 | ||||
-rw-r--r-- | src/theory/strings/regexp_operation.cpp | 3 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 17 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 9 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 7 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_type_rules.h | 2 |
6 files changed, 23 insertions, 71 deletions
diff --git a/src/theory/strings/options b/src/theory/strings/options deleted file mode 100644 index 59a95e5ec..000000000 --- a/src/theory/strings/options +++ /dev/null @@ -1,56 +0,0 @@ -# -# Option specification file for CVC4 -# See src/options/base_options for a description of this file format -# - -module STRINGS "theory/strings/options.h" Strings theory - -option stringExp strings-exp --strings-exp bool :default false :read-write - experimental features in the theory of strings - -option stringLB strings-lb --strings-lb=N unsigned :default 0 :predicate options::less_equal(2) :predicate-include "smt/smt_engine.h" - the strategy of LB rule application: 0-lazy, 1-eager, 2-no - -option stdASCII strings-std-ascii --strings-std-ascii bool :default true :predicate options::less_equal(2) :predicate-include "smt/smt_engine.h" - 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 upon assertion -option stringLazyPreproc2 strings-lazy-pp2 --strings-lazy-pp2 bool :default true - perform string preprocessing lazily upon failure to reduce - -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 - - -endmodule diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index ac4bddd73..98f03327a 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -15,8 +15,9 @@ **/ #include "theory/strings/regexp_operation.h" + #include "expr/kind.h" -#include "theory/strings/options.h" +#include "options/strings_options.h" namespace CVC4 { namespace theory { diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index d4a3cf9c5..dfd3c4803 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -14,18 +14,19 @@ ** Implementation of the theory of strings. **/ - #include "theory/strings/theory_strings.h" -#include "theory/valuation.h" + +#include <cmath> + #include "expr/kind.h" -#include "theory/rewriter.h" -#include "expr/command.h" -#include "theory/theory_model.h" +#include "options/strings_options.h" #include "smt/logic_exception.h" -#include "theory/strings/options.h" -#include "theory/strings/type_enumerator.h" +#include "smt_util/command.h" +#include "theory/rewriter.h" #include "theory/strings/theory_strings_rewriter.h" -#include <cmath> +#include "theory/strings/type_enumerator.h" +#include "theory/theory_model.h" +#include "theory/valuation.h" using namespace std; using namespace CVC4::context; diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 80eb89cc3..a1c93a369 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -15,11 +15,14 @@ **/ #include "theory/strings/theory_strings_preprocess.h" -#include "expr/kind.h" -#include "theory/strings/options.h" -#include "smt/logic_exception.h" + #include <stdint.h> + +#include "expr/kind.h" +#include "options/strings_options.h" #include "proof/proof_manager.h" +#include "smt/logic_exception.h" + namespace CVC4 { namespace theory { diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index e0e295d40..733471288 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -13,11 +13,14 @@ ** ** Implementation of the theory of strings. **/ + #include "theory/strings/theory_strings_rewriter.h" -#include "theory/strings/options.h" -#include "smt/logic_exception.h" + #include <stdint.h> +#include "options/strings_options.h" +#include "smt/logic_exception.h" + using namespace std; using namespace CVC4; using namespace CVC4::kind; diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index 13f3b3b73..aff033338 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -15,7 +15,7 @@ **/ #include "cvc4_private.h" -#include "theory/strings/options.h" +#include "options/strings_options.h" #ifndef __CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H #define __CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H |