diff options
Diffstat (limited to 'src/theory/strings/regexp_operation.h')
-rw-r--r-- | src/theory/strings/regexp_operation.h | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index 8c0cd6c14..27324d971 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -28,7 +28,7 @@ #include "theory/strings/skolem_cache.h" #include "util/string.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -55,7 +55,7 @@ enum RegExpConstType }; class RegExpOpr { - typedef std::pair< Node, CVC4::String > PairNodeStr; + typedef std::pair<Node, CVC5::String> PairNodeStr; typedef std::set< Node > SetNodes; typedef std::pair< Node, Node > PairNodes; @@ -171,8 +171,8 @@ class RegExpOpr { * - delta( (re.union (re.* "A") R) ) returns 1. */ int delta( Node r, Node &exp ); - int derivativeS( Node r, CVC4::String c, Node &retNode ); - Node derivativeSingle( Node r, CVC4::String c ); + int derivativeS(Node r, CVC5::String c, Node& retNode); + Node derivativeSingle(Node r, CVC5::String c); /** * Returns the regular expression intersection of r1 and r2. If r1 or r2 is * not constant, then this method returns null. @@ -207,8 +207,8 @@ class RegExpOpr { SkolemCache* d_sc; }; -}/* CVC4::theory::strings namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace strings +} // namespace theory +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__REGEXP__OPERATION_H */ |