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