diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-11-06 12:11:11 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-11-06 17:20:04 -0600 |
| commit | 657a5e91cb0310f5791c9e9e887da71f395e1f07 (patch) | |
| tree | 3fd9a4ac61d827ca3906ef1507ed7937fbd66443 | |
| parent | ecf2e4ec0f623a46f89b697d1afba81834455d95 (diff) | |
change options
| -rw-r--r-- | src/theory/strings/kinds | 2 | ||||
| -rw-r--r-- | src/theory/strings/options | 4 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 15 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.h | 2 |
4 files changed, 17 insertions, 6 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index e325708c2..20db916c9 100644 --- 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 2832c7833..68d1f7bde 100644 --- 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 ab6ff9d68..e5ce2d6d3 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -192,6 +192,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 1291fc94e..df31dcff7 100644 --- 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() { } ///////////////////////////////////////////////////////////////////////////// |