GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/theory/theory_strings_word_white.cpp Lines: 73 73 100.0 %
Date: 2021-03-22 Branches: 351 1142 30.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_strings_word_white.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Andrew Reynolds
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 Unit tests for the strings word utilities
13
 **/
14
15
#include <iostream>
16
#include <memory>
17
#include <vector>
18
19
#include "expr/node.h"
20
#include "test_node.h"
21
#include "theory/strings/word.h"
22
23
namespace CVC4 {
24
25
using namespace theory;
26
using namespace theory::strings;
27
28
namespace test {
29
30
4
class TestTheoryWhiteStringsWord : public TestNode
31
{
32
};
33
34
10
TEST_F(TestTheoryWhiteStringsWord, strings)
35
{
36
4
  Node empty = d_nodeManager->mkConst(String(""));
37
4
  Node a = d_nodeManager->mkConst(String("a"));
38
4
  Node b = d_nodeManager->mkConst(String("b"));
39
4
  Node aa = d_nodeManager->mkConst(String("aa"));
40
4
  Node aaaaa = d_nodeManager->mkConst(String("aaaaa"));
41
4
  Node abc = d_nodeManager->mkConst(String("abc"));
42
4
  Node bbc = d_nodeManager->mkConst(String("bbc"));
43
4
  Node cac = d_nodeManager->mkConst(String("cac"));
44
4
  Node abca = d_nodeManager->mkConst(String("abca"));
45
46
4
  TypeNode stringType = d_nodeManager->stringType();
47
2
  ASSERT_TRUE(Word::mkEmptyWord(stringType) == empty);
48
49
4
  std::vector<Node> vec;
50
2
  vec.push_back(abc);
51
4
  Node abcMk = Word::mkWordFlatten(vec);
52
2
  ASSERT_EQ(abc, abcMk);
53
2
  vec.push_back(a);
54
4
  Node abcaMk = Word::mkWordFlatten(vec);
55
2
  ASSERT_EQ(abca, abcaMk);
56
57
2
  ASSERT_TRUE(Word::getLength(empty) == 0);
58
2
  ASSERT_TRUE(Word::getLength(aaaaa) == 5);
59
60
2
  ASSERT_TRUE(Word::isEmpty(empty));
61
2
  ASSERT_FALSE(Word::isEmpty(a));
62
63
2
  ASSERT_TRUE(Word::find(empty, empty) == 0);
64
2
  ASSERT_TRUE(Word::find(a, empty) == 0);
65
2
  ASSERT_TRUE(Word::find(empty, empty, 1) == std::string::npos);
66
2
  ASSERT_TRUE(Word::find(cac, a, 0) == 1);
67
2
  ASSERT_TRUE(Word::find(cac, abc) == std::string::npos);
68
69
2
  ASSERT_TRUE(Word::rfind(aaaaa, empty) == 0);
70
2
  ASSERT_TRUE(Word::rfind(aaaaa, a) == 0);
71
2
  ASSERT_TRUE(Word::rfind(abca, abc, 1) == 1);
72
73
2
  ASSERT_TRUE(Word::hasPrefix(empty, empty));
74
2
  ASSERT_TRUE(Word::hasPrefix(a, empty));
75
2
  ASSERT_TRUE(Word::hasPrefix(aaaaa, a));
76
2
  ASSERT_FALSE(Word::hasPrefix(abca, b));
77
2
  ASSERT_FALSE(Word::hasPrefix(empty, a));
78
79
2
  ASSERT_TRUE(Word::hasSuffix(empty, empty));
80
2
  ASSERT_TRUE(Word::hasSuffix(a, empty));
81
2
  ASSERT_TRUE(Word::hasSuffix(a, a));
82
2
  ASSERT_FALSE(Word::hasSuffix(abca, b));
83
2
  ASSERT_FALSE(Word::hasSuffix(empty, abc));
84
85
2
  ASSERT_EQ(bbc, Word::replace(abc, a, b));
86
2
  ASSERT_EQ(aaaaa, Word::replace(aaaaa, b, a));
87
2
  ASSERT_EQ(aa, Word::replace(a, empty, a));
88
89
2
  ASSERT_EQ(empty, Word::substr(a, 1));
90
2
  ASSERT_EQ(empty, Word::substr(empty, 0));
91
2
  ASSERT_EQ(a, Word::substr(abca, 3));
92
93
2
  ASSERT_EQ(a, Word::substr(abc, 0, 1));
94
2
  ASSERT_EQ(aa, Word::substr(aaaaa, 3, 2));
95
96
2
  ASSERT_EQ(a, Word::prefix(a, 1));
97
2
  ASSERT_EQ(empty, Word::prefix(empty, 0));
98
2
  ASSERT_EQ(a, Word::prefix(aaaaa, 1));
99
100
2
  ASSERT_EQ(a, Word::suffix(a, 1));
101
2
  ASSERT_EQ(empty, Word::suffix(empty, 0));
102
2
  ASSERT_EQ(aa, Word::suffix(aaaaa, 2));
103
104
2
  ASSERT_FALSE(Word::noOverlapWith(abc, empty));
105
2
  ASSERT_TRUE(Word::noOverlapWith(cac, aa));
106
2
  ASSERT_FALSE(Word::noOverlapWith(cac, abc));
107
2
  ASSERT_TRUE(Word::noOverlapWith(cac, b));
108
2
  ASSERT_FALSE(Word::noOverlapWith(cac, a));
109
2
  ASSERT_FALSE(Word::noOverlapWith(abca, a));
110
111
2
  ASSERT_TRUE(Word::overlap(abc, empty) == 0);
112
2
  ASSERT_TRUE(Word::overlap(aaaaa, abc) == 1);
113
2
  ASSERT_TRUE(Word::overlap(cac, abc) == 0);
114
2
  ASSERT_TRUE(Word::overlap(empty, abc) == 0);
115
2
  ASSERT_TRUE(Word::overlap(aaaaa, aa) == 2);
116
117
2
  ASSERT_TRUE(Word::roverlap(abc, empty) == 0);
118
2
  ASSERT_TRUE(Word::roverlap(aaaaa, abc) == 0);
119
2
  ASSERT_TRUE(Word::roverlap(cac, abc) == 1);
120
2
  ASSERT_TRUE(Word::roverlap(empty, abc) == 0);
121
2
  ASSERT_TRUE(Word::roverlap(aaaaa, aa) == 2);
122
}
123
}  // namespace test
124
8814
}  // namespace CVC4