diff options
Diffstat (limited to 'src/theory/strings/regexp_operation.h')
-rw-r--r-- | src/theory/strings/regexp_operation.h | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index 04ac11549..d33a2b70c 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -75,7 +75,6 @@ private: Node mkAllExceptOne( unsigned char c ); bool isPairNodesInSet(std::set< PairNodes > &s, Node n1, Node n2); - void getCharSet( Node r, std::set<unsigned char> &pcset, SetNodes &pvset ); bool containC2(unsigned cnt, Node n); Node convert1(unsigned cnt, Node n); void convert2(unsigned cnt, Node n, Node &r1, Node &r2); @@ -83,20 +82,6 @@ private: Node intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > cache, unsigned cnt ); Node removeIntersection(Node r); void firstChars( Node r, std::set<unsigned char> &pcset, SetNodes &pvset ); - - //TODO: for intersection - bool follow( Node r, CVC4::String c, std::vector< unsigned char > &vec_chars ); - - /*class CState { - public: - Node r1; - Node r2; - unsigned cnt; - Node head; - CState(Node rr1, Node rr2, Node rcnt, Node rhead) - : r1(rr1), r2(rr2), cnt(rcnt), head(rhead) {} - };*/ - public: RegExpOpr(); ~RegExpOpr(); @@ -106,12 +91,7 @@ public: int delta( Node r, Node &exp ); int derivativeS( Node r, CVC4::String c, Node &retNode ); Node derivativeSingle( Node r, CVC4::String c ); - bool guessLength( Node r, int &co ); Node intersect(Node r1, Node r2, bool &spflag); - Node complement(Node r, int &ret); - void splitRegExp(Node r, std::vector< PairNodes > &pset); - void flattenRegExp(Node r, std::vector< std::pair< CVC4::String, unsigned > > &fvec); - void disjunctRegExp(Node r, std::vector<Node> &vec_or); std::string mkString( Node r ); }; |