7b41c176419ff5df8f3bb4c8ee47360db75dd028
1 /********************* */
2 /*! \file regexp_operation.h
4 ** Original author: Tianyi Liang
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Regular Expression Operations
14 ** Regular Expression Operations
17 #include "cvc4_private.h"
19 #ifndef __CVC4__THEORY__STRINGS__REGEXP__OPERATION_H
20 #define __CVC4__THEORY__STRINGS__REGEXP__OPERATION_H
23 #include "util/hash.h"
24 #include "theory/theory.h"
25 #include "theory/rewriter.h"
26 //#include "context/cdhashmap.h"
33 typedef std::pair
< Node
, CVC4::String
> PairDvStr
;
48 std::map
< std::pair
< Node
, Node
>, Node
> d_simpl_cache
;
49 std::map
< std::pair
< Node
, Node
>, Node
> d_simpl_neg_cache
;
50 std::map
< Node
, Node
> d_compl_cache
;
51 std::map
< Node
, int > d_delta_cache
;
52 std::map
< PairDvStr
, Node
> d_dv_cache
;
53 std::map
< Node
, bool > d_cstre_cache
;
54 //bool checkStarPlus( Node t );
55 void simplifyPRegExp( Node s
, Node r
, std::vector
< Node
> &new_nodes
);
56 void simplifyNRegExp( Node s
, Node r
, std::vector
< Node
> &new_nodes
);
57 std::string
niceChar( Node r
);
58 int gcd ( int a
, int b
);
59 Node
mkAllExceptOne( char c
);
64 bool checkConstRegExp( Node r
);
65 void simplify(Node t
, std::vector
< Node
> &new_nodes
, bool polarity
);
67 Node
derivativeSingle( Node r
, CVC4::String c
);
68 bool guessLength( Node r
, int &co
);
69 void firstChar( Node r
);
70 bool follow( Node r
, CVC4::String c
, std::vector
< char > &vec_chars
);
71 std::string
mkString( Node r
);
74 }/* CVC4::theory::strings namespace */
75 }/* CVC4::theory namespace */
78 #endif /* __CVC4__THEORY__STRINGS__REGEXP__OPERATION_H */