diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-20 14:07:37 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-20 14:07:37 -0500 |
commit | 964760cf81eb7414a11bbd89ef3a16e8927d6947 (patch) | |
tree | 0c574e99433c722e69af6efeeefbe0901010f7b7 /src/theory/strings/strings_rewriter.h | |
parent | aa44c35f035f1cab03de0c5fe7c0f16b20f44696 (diff) |
Split string-specific operators from TheoryStringsRewriter (#3920)
Organization towards theory of sequences.
The motivation of this PR is to ensure that string-specific operators in the rewriter are in their own file; thus the use of mkConst<String> / getConst<String> is allowable in rewriter_str.cpp.
Diffstat (limited to 'src/theory/strings/strings_rewriter.h')
-rw-r--r-- | src/theory/strings/strings_rewriter.h | 88 |
1 files changed, 88 insertions, 0 deletions
diff --git a/src/theory/strings/strings_rewriter.h b/src/theory/strings/strings_rewriter.h new file mode 100644 index 000000000..e6a6b0693 --- /dev/null +++ b/src/theory/strings/strings_rewriter.h @@ -0,0 +1,88 @@ +/********************* */ +/*! \file strings_rewriter.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Andres Noetzli, Tianyi Liang + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 Rewrite rules for string-specific operators in theory of strings + ** + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__STRINGS__STRINGS_REWRITER_H +#define CVC4__THEORY__STRINGS__STRINGS_REWRITER_H + +#include "expr/node.h" +#include "theory/strings/sequences_rewriter.h" + +namespace CVC4 { +namespace theory { +namespace strings { + +/** + * An extension of SequencesRewriter that handles operators that + * are specific to strings (and cannot be applied to sequences). + */ +class StringsRewriter : public SequencesRewriter +{ + public: + /** rewrite string to integer + * + * This is the entry point for post-rewriting terms n of the form + * str.to_int( s ) + * Returns the rewritten form of n. + */ + static Node rewriteStrToInt(Node n); + + /** rewrite integer to string + * + * This is the entry point for post-rewriting terms n of the form + * str.from_int( i ) + * Returns the rewritten form of n. + */ + static Node rewriteIntToStr(Node n); + + /** rewrite string convert + * + * This is the entry point for post-rewriting terms n of the form + * str.tolower( s ) and str.toupper( s ) + * Returns the rewritten form of n. + */ + static Node rewriteStrConvert(Node n); + + /** rewrite string less than or equal + * + * This is the entry point for post-rewriting terms n of the form + * str.<=( t, s ) + * Returns the rewritten form of n. + */ + static Node rewriteStringLeq(Node n); + + /** rewrite str.from_code + * + * This is the entry point for post-rewriting terms n of the form + * str.from_code( t ) + * Returns the rewritten form of n. + */ + static Node rewriteStringFromCode(Node n); + + /** rewrite str.to_code + * + * This is the entry point for post-rewriting terms n of the form + * str.to_code( t ) + * Returns the rewritten form of n. + */ + static Node rewriteStringToCode(Node n); +}; + +} // namespace strings +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__STRINGS__STRINGS_REWRITER_H */ |