diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-15 02:34:33 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-15 02:34:33 -0500 |
commit | 3f3a0445fe772360d8a2da3069a5f082c031d7f8 (patch) | |
tree | bf78f4bbe23ca8f88cf23aca0f31e0594765799f /src/theory/strings/regexp_operation.cpp | |
parent | c808605ef15eb79f9ddc2d1a2b4f6dd052530877 (diff) |
Convert more cases of strings to words (#4206)
Diffstat (limited to 'src/theory/strings/regexp_operation.cpp')
-rw-r--r-- | src/theory/strings/regexp_operation.cpp | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 0520ec88a..0d6b6c7fe 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -288,7 +288,9 @@ int RegExpOpr::derivativeS( Node r, CVC4::String c, Node &retNode ) { if( d_deriv_cache.find( dv ) != d_deriv_cache.end() ) { retNode = d_deriv_cache[dv].first; ret = d_deriv_cache[dv].second; - } else if( c.isEmptyString() ) { + } + else if (c.empty()) + { Node expNode; ret = delta( r, expNode ); if(ret == 0) { @@ -536,7 +538,9 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) { NodeManager* nm = NodeManager::currentNM(); if( d_dv_cache.find( dv ) != d_dv_cache.end() ) { retNode = d_dv_cache[dv]; - } else if( c.isEmptyString() ){ + } + else if (c.empty()) + { Node exp; int tmp = delta( r, exp ); if(tmp == 0) { |