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