change options

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index e325708c2cc34d7a522fdf2bf420ade5b2027321..20db916c98cdcc5f574cb407817b47e61c64aa79 100644 (file)
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -3,7 +3,7 @@
 
 theory THEORY_STRINGS ::CVC4::theory::strings::TheoryStrings "theory/strings/theory_strings.h"
 
-properties check parametric propagate getNextDecisionRequest
+properties check parametric propagate getNextDecisionRequest presolve
 
 rewriter ::CVC4::theory::strings::TheoryStringsRewriter "theory/strings/theory_strings_rewriter.h"
 

diff --git a/src/theory/strings/options b/src/theory/strings/options
index 2832c7833df32cb3da7666a930662b2a700482be..68d1f7bde93729ca405be9de7f237690d98e69dd 100644 (file)
--- a/src/theory/strings/options
+++ b/src/theory/strings/options
@@ -5,13 +5,13 @@
 
 module STRINGS "theory/strings/options.h" Strings theory
 
-option stringCharCardinality str-alphabet-card --str-alphabet-card=N int16_t :default 256 :read-write
+option stringCharCardinality str-alphabet-card --str-alphabet-card=N int16_t :default 256 :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
  the cardinality of the characters used by the theory of strings, default 256
 
 option stringRegExpUnrollDepth str-regexp-depth --str-regexp-depth=N int16_t :default 10 :read-write
  the depth of unrolloing regular expression used by the theory of strings, default 10
 
-option stringFMF fmf-strings --fmf-strings bool :default false
+option stringFMF fmf-strings --fmf-strings bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
  the finite model finding used by the theory of strings
 
 endmodule

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index ab6ff9d686b0f384dec61fa9ddd9fa729b20c7b1..e5ce2d6d3fb29e0756f70ced637c8c612758ebef 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -191,6 +191,17 @@ Node TheoryStrings::explain( TNode literal ){
   }
 }
 
+/////////////////////////////////////////////////////////////////////////////
+// NOTIFICATIONS
+/////////////////////////////////////////////////////////////////////////////
+
+
+void TheoryStrings::presolve()
+{
+  Trace("strings-presolve") << "TheoryStrings : Presolving " << std::endl;
+}
+
+
 /////////////////////////////////////////////////////////////////////////////
 // MODEL GENERATION
 /////////////////////////////////////////////////////////////////////////////
@@ -2044,8 +2055,8 @@ CVC4::String TheoryStrings::getHeadConst( Node x ) {
 bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) {
        x =  Rewriter::rewrite( x );
        if(x == d_emptyString) {
-               //if(d_regexp_opr.delta() == 1) {
-               //}
+               if(d_regexp_opr.delta( r ) == 1) {
+               }
                return false;
        } else {
                CVC4::String s = getHeadConst( x );

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 1291fc94ed25a55848f5a40d7c704f3c63d89198..df31dcff7b91240aaa46681fd0534ba2232d3627 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -169,7 +169,7 @@ class TheoryStrings : public Theory {
   /////////////////////////////////////////////////////////////////////////////
 
   public:
-
+  void presolve();
   void shutdown() { }
 
   /////////////////////////////////////////////////////////////////////////////