diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-30 11:57:58 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-30 11:57:58 -0500 |
commit | bc0c0b8b9ea77e8e4e328dbe66a4582fa7883eda (patch) | |
tree | 4f43e20e294ade551676847668ceb424d44bab4f /src/theory/strings/regexp_elim.h | |
parent | 3eac9d04c5d4bfba81142d4a5fe91b86590b32ae (diff) |
Add regular expression elimination module (#2400)
Diffstat (limited to 'src/theory/strings/regexp_elim.h')
-rw-r--r-- | src/theory/strings/regexp_elim.h | 66 |
1 files changed, 66 insertions, 0 deletions
diff --git a/src/theory/strings/regexp_elim.h b/src/theory/strings/regexp_elim.h new file mode 100644 index 000000000..eddf33e71 --- /dev/null +++ b/src/theory/strings/regexp_elim.h @@ -0,0 +1,66 @@ +/********************* */ +/*! \file regexp_elim.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Techniques for eliminating regular expressions + ** + **/ + +#include "cvc4_private.h" +#ifndef __CVC4__THEORY__STRINGS__REGEXP_ELIM_H +#define __CVC4__THEORY__STRINGS__REGEXP_ELIM_H + +#include "expr/node.h" + +namespace CVC4 { +namespace theory { +namespace strings { + +/** Regular expression membership elimination + * + * This class implements techniques for reducing regular expression memberships + * to bounded integer quantifiers + extended function constraints. + * + * It is used by TheoryStrings during ppRewrite. + */ +class RegExpElimination +{ + public: + RegExpElimination(); + /** eliminate membership + * + * This method takes as input a regular expression membership atom of the + * form (str.in.re x R). If this method returns a non-null node ret, then ret + * is equivalent to atom. + */ + Node eliminate(Node atom); + + private: + /** common terms */ + Node d_zero; + Node d_one; + Node d_neg_one; + /** return elimination + * + * This method is called when atom is rewritten to atomElim, and returns + * atomElim. id is an identifier indicating the reason for the elimination. + */ + Node returnElim(Node atom, Node atomElim, const char* id); + /** elimination for regular expression concatenation */ + Node eliminateConcat(Node atom); + /** elimination for regular expression star */ + Node eliminateStar(Node atom); +}; /* class RegExpElimination */ + +} // namespace strings +} // namespace theory +} // namespace CVC4 + +#endif /* __CVC4__THEORY__STRINGS__REGEXP_ELIM_H */ |