diff options
Diffstat (limited to 'src/theory/strings/regexp_operation.h')
-rw-r--r-- | src/theory/strings/regexp_operation.h | 200 |
1 files changed, 100 insertions, 100 deletions
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index d5606627f..e4ae1208d 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -1,100 +1,100 @@ -/********************* */
-/*! \file regexp_operation.h
- ** \verbatim
- ** Original author: Tianyi Liang
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Symbolic Regular Expresion Operations
- **
- ** Symbolic Regular Expression Operations
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__STRINGS__REGEXP__OPERATION_H
-#define __CVC4__THEORY__STRINGS__REGEXP__OPERATION_H
-
-#include <vector>
-#include <set>
-#include <algorithm>
-#include "util/hash.h"
-#include "util/regexp.h"
-#include "theory/theory.h"
-#include "theory/rewriter.h"
-//#include "context/cdhashmap.h"
-
-namespace CVC4 {
-namespace theory {
-namespace strings {
-
-class RegExpOpr {
- typedef std::pair< Node, CVC4::String > PairNodeStr;
- typedef std::set< Node > SetNodes;
- typedef std::pair< Node, Node > PairNodes;
-
-private:
- unsigned d_card;
- Node d_emptyString;
- Node d_true;
- Node d_false;
- Node d_emptySingleton;
- Node d_emptyRegexp;
- Node d_zero;
- Node d_one;
-
- char d_char_start;
- char d_char_end;
- Node d_sigma;
- Node d_sigma_star;
-
- std::map< PairNodes, Node > d_simpl_cache;
- std::map< PairNodes, Node > d_simpl_neg_cache;
- std::map< Node, std::pair< int, Node > > d_delta_cache;
- std::map< PairNodeStr, Node > d_dv_cache;
- std::map< PairNodeStr, std::pair< Node, int > > d_deriv_cache;
- std::map< Node, std::pair< Node, int > > d_compl_cache;
- std::map< Node, bool > d_cstre_cache;
- std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_cset_cache;
- std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_fset_cache;
- std::map< PairNodes, Node > d_inter_cache;
- std::map< Node, std::vector< PairNodes > > d_split_cache;
- //bool checkStarPlus( Node t );
- void simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes );
- void simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes );
- std::string niceChar( Node r );
- int gcd ( int a, int b );
- Node mkAllExceptOne( char c );
-
- void getCharSet( Node r, std::set<unsigned> &pcset, SetNodes &pvset );
- Node intersectInternal( Node r1, Node r2, std::map< unsigned, std::set< PairNodes > > cache, bool &spflag );
- void firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset );
-
- //TODO: for intersection
- bool follow( Node r, CVC4::String c, std::vector< char > &vec_chars );
-
-public:
- RegExpOpr();
-
- bool checkConstRegExp( Node r );
- void simplify(Node t, std::vector< Node > &new_nodes, bool polarity);
- 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);
-
- std::string mkString( Node r );
-};
-
-}/* CVC4::theory::strings namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__STRINGS__REGEXP__OPERATION_H */
+/********************* */ +/*! \file regexp_operation.h + ** \verbatim + ** Original author: Tianyi Liang + ** Major contributors: Morgan Deters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Symbolic Regular Expresion Operations + ** + ** Symbolic Regular Expression Operations + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__STRINGS__REGEXP__OPERATION_H +#define __CVC4__THEORY__STRINGS__REGEXP__OPERATION_H + +#include <vector> +#include <set> +#include <algorithm> +#include "util/hash.h" +#include "util/regexp.h" +#include "theory/theory.h" +#include "theory/rewriter.h" +//#include "context/cdhashmap.h" + +namespace CVC4 { +namespace theory { +namespace strings { + +class RegExpOpr { + typedef std::pair< Node, CVC4::String > PairNodeStr; + typedef std::set< Node > SetNodes; + typedef std::pair< Node, Node > PairNodes; + +private: + unsigned d_card; + Node d_emptyString; + Node d_true; + Node d_false; + Node d_emptySingleton; + Node d_emptyRegexp; + Node d_zero; + Node d_one; + + char d_char_start; + char d_char_end; + Node d_sigma; + Node d_sigma_star; + + std::map< PairNodes, Node > d_simpl_cache; + std::map< PairNodes, Node > d_simpl_neg_cache; + std::map< Node, std::pair< int, Node > > d_delta_cache; + std::map< PairNodeStr, Node > d_dv_cache; + std::map< PairNodeStr, std::pair< Node, int > > d_deriv_cache; + std::map< Node, std::pair< Node, int > > d_compl_cache; + std::map< Node, bool > d_cstre_cache; + std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_cset_cache; + std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_fset_cache; + std::map< PairNodes, Node > d_inter_cache; + std::map< Node, std::vector< PairNodes > > d_split_cache; + //bool checkStarPlus( Node t ); + void simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes ); + void simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes ); + std::string niceChar( Node r ); + int gcd ( int a, int b ); + Node mkAllExceptOne( char c ); + + void getCharSet( Node r, std::set<unsigned> &pcset, SetNodes &pvset ); + Node intersectInternal( Node r1, Node r2, std::map< unsigned, std::set< PairNodes > > cache, bool &spflag ); + void firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset ); + + //TODO: for intersection + bool follow( Node r, CVC4::String c, std::vector< char > &vec_chars ); + +public: + RegExpOpr(); + + bool checkConstRegExp( Node r ); + void simplify(Node t, std::vector< Node > &new_nodes, bool polarity); + 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); + + std::string mkString( Node r ); +}; + +}/* CVC4::theory::strings namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__STRINGS__REGEXP__OPERATION_H */ |