From be7e2fcf9c0b1b45bcd253211b9ebdd1c2257198 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Wed, 6 Nov 2013 12:11:11 -0600 Subject: [PATCH] change options --- src/theory/strings/kinds | 2 +- src/theory/strings/options | 4 ++-- src/theory/strings/theory_strings.cpp | 15 +++++++++++++-- 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 @@ -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 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() { } ///////////////////////////////////////////////////////////////////////////// -- 2.30.2