1 /*********************                                                        */
2 /*! \file regexp_elim.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Andrew Reynolds
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
8  ** in the top-level source directory) and their institutional affiliations.
9  ** All rights reserved.  See the file COPYING in the top-level source
10  ** directory for licensing information.\endverbatim
11  **
12  ** \brief Techniques for eliminating regular expressions
13  **
14  **/
15 
16 #include "cvc4_private.h"
17 #ifndef __CVC4__THEORY__STRINGS__REGEXP_ELIM_H
18 #define __CVC4__THEORY__STRINGS__REGEXP_ELIM_H
19 
20 #include "expr/node.h"
21 
22 namespace CVC4 {
23 namespace theory {
24 namespace strings {
25 
26 /** Regular expression membership elimination
27  *
28  * This class implements techniques for reducing regular expression memberships
29  * to bounded integer quantifiers + extended function constraints.
30  *
31  * It is used by TheoryStrings during ppRewrite.
32  */
33 class RegExpElimination
34 {
35  public:
36   RegExpElimination();
37   /** eliminate membership
38    *
39    * This method takes as input a regular expression membership atom of the
40    * form (str.in.re x R). If this method returns a non-null node ret, then ret
41    * is equivalent to atom.
42    */
43   Node eliminate(Node atom);
44 
45  private:
46   /** common terms */
47   Node d_zero;
48   Node d_one;
49   Node d_neg_one;
50   /** return elimination
51    *
52    * This method is called when atom is rewritten to atomElim, and returns
53    * atomElim. id is an identifier indicating the reason for the elimination.
54    */
55   Node returnElim(Node atom, Node atomElim, const char* id);
56   /** elimination for regular expression concatenation */
57   Node eliminateConcat(Node atom);
58   /** elimination for regular expression star */
59   Node eliminateStar(Node atom);
60 }; /* class RegExpElimination */
61 
62 }  // namespace strings
63 }  // namespace theory
64 }  // namespace CVC4
65 
66 #endif /* __CVC4__THEORY__STRINGS__REGEXP_ELIM_H */
67