GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/strings_rewriter.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 2 8 25.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file strings_rewriter.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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 Rewrite rules for string-specific operators in theory of strings
13
 **
14
 **/
15
16
#include "cvc4_private.h"
17
18
#ifndef CVC4__THEORY__STRINGS__STRINGS_REWRITER_H
19
#define CVC4__THEORY__STRINGS__STRINGS_REWRITER_H
20
21
#include "expr/node.h"
22
#include "theory/strings/sequences_rewriter.h"
23
24
namespace CVC4 {
25
namespace theory {
26
namespace strings {
27
28
/**
29
 * An extension of SequencesRewriter that handles operators that
30
 * are specific to strings (and cannot be applied to sequences).
31
 */
32
106013
class StringsRewriter : public SequencesRewriter
33
{
34
 public:
35
  StringsRewriter(IntegralHistogramStat<Rewrite>* statistics);
36
37
  RewriteResponse postRewrite(TNode node) override;
38
39
  /** rewrite string to integer
40
   *
41
   * This is the entry point for post-rewriting terms n of the form
42
   *   str.to_int( s )
43
   * Returns the rewritten form of n.
44
   */
45
  Node rewriteStrToInt(Node n);
46
47
  /** rewrite integer to string
48
   *
49
   * This is the entry point for post-rewriting terms n of the form
50
   *   str.from_int( i )
51
   * Returns the rewritten form of n.
52
   */
53
  Node rewriteIntToStr(Node n);
54
55
  /** rewrite string convert
56
   *
57
   * This is the entry point for post-rewriting terms n of the form
58
   *   str.tolower( s ) and str.toupper( s )
59
   * Returns the rewritten form of n.
60
   */
61
  Node rewriteStrConvert(Node n);
62
63
  /** rewrite string less than
64
   *
65
   * This is the entry point for post-rewriting terms n of the form
66
   *   str.<( t, s )
67
   * Returns the rewritten form of n.
68
   */
69
  Node rewriteStringLt(Node n);
70
71
  /** rewrite string less than or equal
72
   *
73
   * This is the entry point for post-rewriting terms n of the form
74
   *   str.<=( t, s )
75
   * Returns the rewritten form of n.
76
   */
77
  Node rewriteStringLeq(Node n);
78
79
  /** rewrite str.from_code
80
   *
81
   * This is the entry point for post-rewriting terms n of the form
82
   *   str.from_code( t )
83
   * Returns the rewritten form of n.
84
   */
85
  Node rewriteStringFromCode(Node n);
86
87
  /** rewrite str.to_code
88
   *
89
   * This is the entry point for post-rewriting terms n of the form
90
   *   str.to_code( t )
91
   * Returns the rewritten form of n.
92
   */
93
  Node rewriteStringToCode(Node n);
94
95
  /** rewrite is digit
96
   *
97
   * This is the entry point for post-rewriting terms n of the form
98
   *   str.is_digit( t )
99
   * Returns the rewritten form of n.
100
   */
101
  Node rewriteStringIsDigit(Node n);
102
};
103
104
}  // namespace strings
105
}  // namespace theory
106
}  // namespace CVC4
107
108
#endif /* CVC4__THEORY__STRINGS__STRINGS_REWRITER_H */