GCC Code Coverage Report
 Directory: . Exec Total Coverage File: src/theory/strings/strings_rewriter.h Lines: 1 1 100.0 % Date: 2021-03-22 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 105935 class StringsRewriter : public SequencesRewriter 33 { 34 public: 35 StringsRewriter(IntegralHistogramStat* 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 */

 Generated by: GCOVR (Version 3.2)