diff options
| author | Tim King <taking@cs.nyu.edu> | 2017-11-13 23:25:59 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-11-13 23:25:59 -0800 |
| commit | afc3de987e3416e1987bc6be9aa0b0adb7fd63ab (patch) | |
| tree | 340c2eec525ffb825ed548dadf760ff3159c6343 | |
| parent | 312a7ec0ee5bf7fcf03f7af4a924e4eb03774f67 (diff) | |
Initializes RegExpOpr::d_char_start and d_char_end. (#1359)
| -rw-r--r-- | src/theory/strings/regexp_operation.cpp | 35 |
1 files changed, 18 insertions, 17 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index a98a2a0ef..a8fd08792 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -24,24 +24,25 @@ namespace theory { namespace strings { RegExpOpr::RegExpOpr() - : d_lastchar( options::stdASCII()? '\x7f' : '\xff' ), - RMAXINT( LONG_MAX ) -{ - d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); - d_true = NodeManager::currentNM()->mkConst( true ); - d_false = NodeManager::currentNM()->mkConst( false ); - d_emptySingleton = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString ); - d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); - d_one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); - std::vector< Node > nvec; - d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec ); - d_sigma = NodeManager::currentNM()->mkNode( kind::REGEXP_SIGMA, nvec ); - d_sigma_star = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma ); -} - -RegExpOpr::~RegExpOpr(){ + : d_lastchar(options::stdASCII() ? '\x7f' : '\xff'), + d_emptyString(NodeManager::currentNM()->mkConst(::CVC4::String(""))), + d_true(NodeManager::currentNM()->mkConst(true)), + d_false(NodeManager::currentNM()->mkConst(false)), + d_emptySingleton(NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, + d_emptyString)), + d_emptyRegexp(NodeManager::currentNM()->mkNode(kind::REGEXP_EMPTY, + std::vector<Node>{})), + d_zero(NodeManager::currentNM()->mkConst(::CVC4::Rational(0))), + d_one(NodeManager::currentNM()->mkConst(::CVC4::Rational(1))), + RMAXINT(LONG_MAX), + d_char_start(), + d_char_end(), + d_sigma(NodeManager::currentNM()->mkNode(kind::REGEXP_SIGMA, + std::vector<Node>{})), + d_sigma_star( + NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, d_sigma)) {} -} +RegExpOpr::~RegExpOpr() {} int RegExpOpr::gcd ( int a, int b ) { int c; |