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