diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-28 13:04:33 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-28 22:59:00 -0600 |
| commit | fb4104e7c5a88741f9ffd55384198af31435df9e (patch) | |
| tree | 4b9cd33cbe4ebccd914e63ddb1ae412f2c101d8b /src/theory/strings/theory_strings.cpp | |
| parent | acb79cbe43ddcd855db042b7c937fc2eacaa0ac3 (diff) | |
minor clean-up, bring back derivatives
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 28ef43cf9..072d28f9d 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -62,7 +62,8 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); - d_emptyRegexp = NodeManager::currentNM()->mkConst( kind::REGEXP_EMPTY ); + std::vector< Node > nvec; + d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec ); d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); @@ -2312,13 +2313,13 @@ bool TheoryStrings::checkMemberships() { flag = false; d_regexp_deriv_processed[atom] = true; } - } /*else if(splitRegExp( x, r, atom )) { + } else if(splitRegExp( x, r, atom )) { addedLemma = true; flag = false; d_regexp_deriv_processed[ atom ] = true; - }*/ + } } } else { - //TODO + //TODO: will be removed soon. keep it for consistence if(! options::stringExp()) { is_unk = true; break; |