GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/theory/regexp_operation_black.cpp Lines: 72 72 100.0 %
Date: 2021-03-23 Branches: 220 456 48.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file regexp_operation_black.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, 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 Unit tests for symbolic regular expression operations
13
 **
14
 ** Unit tests for symbolic regular expression operations.
15
 **/
16
17
#include <iostream>
18
#include <memory>
19
#include <vector>
20
21
#include "api/cvc4cpp.h"
22
#include "expr/node.h"
23
#include "expr/node_manager.h"
24
#include "smt/smt_engine_scope.h"
25
#include "test_smt.h"
26
#include "theory/rewriter.h"
27
#include "theory/strings/regexp_operation.h"
28
#include "theory/strings/skolem_cache.h"
29
30
namespace CVC4 {
31
32
using namespace kind;
33
using namespace theory;
34
using namespace theory::strings;
35
36
namespace test {
37
38
8
class TestTheoryBlackRegexpOperation : public TestSmt
39
{
40
 protected:
41
4
  void SetUp() override
42
  {
43
4
    TestSmt::SetUp();
44
4
    d_skolemCache.reset(new SkolemCache());
45
4
    d_regExpOpr.reset(new RegExpOpr(d_skolemCache.get()));
46
4
  }
47
48
30
  void includes(Node r1, Node r2)
49
  {
50
30
    r1 = Rewriter::rewrite(r1);
51
30
    r2 = Rewriter::rewrite(r2);
52
30
    std::cout << r1 << " includes " << r2 << std::endl;
53
30
    ASSERT_TRUE(d_regExpOpr->regExpIncludes(r1, r2));
54
  }
55
56
24
  void doesNotInclude(Node r1, Node r2)
57
  {
58
24
    r1 = Rewriter::rewrite(r1);
59
24
    r2 = Rewriter::rewrite(r2);
60
24
    std::cout << r1 << " does not include " << r2 << std::endl;
61
24
    ASSERT_FALSE(d_regExpOpr->regExpIncludes(r1, r2));
62
  }
63
64
  std::unique_ptr<SkolemCache> d_skolemCache;
65
  std::unique_ptr<RegExpOpr> d_regExpOpr;
66
};
67
68
11
TEST_F(TestTheoryBlackRegexpOperation, basic)
69
{
70
4
  Node sigma = d_nodeManager->mkNode(REGEXP_SIGMA, std::vector<Node>{});
71
4
  Node sigmaStar = d_nodeManager->mkNode(REGEXP_STAR, sigma);
72
  Node a = d_nodeManager->mkNode(STRING_TO_REGEXP,
73
4
                                 d_nodeManager->mkConst(String("a")));
74
  Node c = d_nodeManager->mkNode(STRING_TO_REGEXP,
75
4
                                 d_nodeManager->mkConst(String("c")));
76
  Node abc = d_nodeManager->mkNode(STRING_TO_REGEXP,
77
4
                                   d_nodeManager->mkConst(String("abc")));
78
4
  Node sigma3 = d_nodeManager->mkNode(REGEXP_CONCAT, sigma, sigma, sigma);
79
4
  Node asc = d_nodeManager->mkNode(REGEXP_CONCAT, a, sigma, c);
80
4
  Node asw = d_nodeManager->mkNode(REGEXP_CONCAT, a, sigma, sigmaStar);
81
82
2
  includes(sigma3, abc);
83
2
  doesNotInclude(abc, sigma3);
84
85
2
  includes(sigma3, asc);
86
2
  doesNotInclude(asc, sigma3);
87
88
2
  includes(asc, abc);
89
2
  doesNotInclude(abc, asc);
90
91
2
  includes(asw, asc);
92
2
  doesNotInclude(asc, asw);
93
2
}
94
95
11
TEST_F(TestTheoryBlackRegexpOperation, star_wildcards)
96
{
97
4
  Node sigma = d_nodeManager->mkNode(REGEXP_SIGMA, std::vector<Node>{});
98
4
  Node sigmaStar = d_nodeManager->mkNode(REGEXP_STAR, sigma);
99
  Node a = d_nodeManager->mkNode(STRING_TO_REGEXP,
100
4
                                 d_nodeManager->mkConst(String("a")));
101
  Node c = d_nodeManager->mkNode(STRING_TO_REGEXP,
102
4
                                 d_nodeManager->mkConst(String("c")));
103
  Node abc = d_nodeManager->mkNode(STRING_TO_REGEXP,
104
4
                                   d_nodeManager->mkConst(String("abc")));
105
106
4
  Node _abc_ = d_nodeManager->mkNode(REGEXP_CONCAT, sigmaStar, abc, sigmaStar);
107
  Node _asc_ =
108
4
      d_nodeManager->mkNode(REGEXP_CONCAT, sigmaStar, a, sigma, c, sigmaStar);
109
  Node _sc_ = Rewriter::rewrite(
110
4
      d_nodeManager->mkNode(REGEXP_CONCAT, sigmaStar, sigma, c, sigmaStar));
111
  Node _as_ = Rewriter::rewrite(
112
4
      d_nodeManager->mkNode(REGEXP_CONCAT, sigmaStar, a, sigma, sigmaStar));
113
  Node _assc_ = d_nodeManager->mkNode(
114
      REGEXP_CONCAT,
115
4
      std::vector<Node>{sigmaStar, a, sigma, sigma, c, sigmaStar});
116
  Node _csa_ =
117
4
      d_nodeManager->mkNode(REGEXP_CONCAT, sigmaStar, c, sigma, a, sigmaStar);
118
  Node _c_a_ = d_nodeManager->mkNode(
119
4
      REGEXP_CONCAT, sigmaStar, c, sigmaStar, a, sigmaStar);
120
4
  Node _s_s_ = Rewriter::rewrite(d_nodeManager->mkNode(
121
4
      REGEXP_CONCAT, sigmaStar, sigma, sigmaStar, sigma, sigmaStar));
122
4
  Node _a_abc_ = Rewriter::rewrite(d_nodeManager->mkNode(
123
4
      REGEXP_CONCAT, sigmaStar, a, sigmaStar, abc, sigmaStar));
124
125
2
  includes(_asc_, _abc_);
126
2
  doesNotInclude(_abc_, _asc_);
127
2
  doesNotInclude(_csa_, _abc_);
128
2
  doesNotInclude(_assc_, _asc_);
129
2
  doesNotInclude(_asc_, _assc_);
130
2
  includes(_sc_, abc);
131
2
  includes(_sc_, _abc_);
132
2
  includes(_sc_, _asc_);
133
2
  includes(_sc_, _assc_);
134
2
  doesNotInclude(_sc_, _csa_);
135
2
  includes(_as_, abc);
136
2
  includes(_as_, _abc_);
137
2
  includes(_as_, _asc_);
138
2
  includes(_as_, _assc_);
139
2
  doesNotInclude(_sc_, _csa_);
140
2
  includes(_s_s_, _c_a_);
141
2
  doesNotInclude(_c_a_, _s_s_);
142
2
  includes(_abc_, _a_abc_);
143
2
  doesNotInclude(_a_abc_, _abc_);
144
2
}
145
146
}  // namespace test
147
114147
}  // namespace CVC4