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/smt_engine_scope.h" |
24 |
|
#include "test_smt.h" |
25 |
|
#include "theory/rewriter.h" |
26 |
|
#include "theory/strings/regexp_operation.h" |
27 |
|
#include "theory/strings/skolem_cache.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 |
d_skolemCache.reset(new SkolemCache()); |
44 |
4 |
d_regExpOpr.reset(new RegExpOpr(d_skolemCache.get())); |
45 |
4 |
} |
46 |
|
|
47 |
30 |
void includes(Node r1, Node r2) |
48 |
|
{ |
49 |
30 |
r1 = Rewriter::rewrite(r1); |
50 |
30 |
r2 = Rewriter::rewrite(r2); |
51 |
30 |
std::cout << r1 << " includes " << r2 << std::endl; |
52 |
30 |
ASSERT_TRUE(d_regExpOpr->regExpIncludes(r1, r2)); |
53 |
|
} |
54 |
|
|
55 |
24 |
void doesNotInclude(Node r1, Node r2) |
56 |
|
{ |
57 |
24 |
r1 = Rewriter::rewrite(r1); |
58 |
24 |
r2 = Rewriter::rewrite(r2); |
59 |
24 |
std::cout << r1 << " does not include " << r2 << std::endl; |
60 |
24 |
ASSERT_FALSE(d_regExpOpr->regExpIncludes(r1, r2)); |
61 |
|
} |
62 |
|
|
63 |
|
std::unique_ptr<SkolemCache> d_skolemCache; |
64 |
|
std::unique_ptr<RegExpOpr> d_regExpOpr; |
65 |
|
}; |
66 |
|
|
67 |
11 |
TEST_F(TestTheoryBlackRegexpOperation, basic) |
68 |
|
{ |
69 |
4 |
Node sigma = d_nodeManager->mkNode(REGEXP_SIGMA); |
70 |
4 |
Node sigmaStar = d_nodeManager->mkNode(REGEXP_STAR, sigma); |
71 |
|
Node a = d_nodeManager->mkNode(STRING_TO_REGEXP, |
72 |
4 |
d_nodeManager->mkConst(String("a"))); |
73 |
|
Node c = d_nodeManager->mkNode(STRING_TO_REGEXP, |
74 |
4 |
d_nodeManager->mkConst(String("c"))); |
75 |
|
Node abc = d_nodeManager->mkNode(STRING_TO_REGEXP, |
76 |
4 |
d_nodeManager->mkConst(String("abc"))); |
77 |
4 |
Node sigma3 = d_nodeManager->mkNode(REGEXP_CONCAT, sigma, sigma, sigma); |
78 |
4 |
Node asc = d_nodeManager->mkNode(REGEXP_CONCAT, a, sigma, c); |
79 |
4 |
Node asw = d_nodeManager->mkNode(REGEXP_CONCAT, a, sigma, sigmaStar); |
80 |
|
|
81 |
2 |
includes(sigma3, abc); |
82 |
2 |
doesNotInclude(abc, sigma3); |
83 |
|
|
84 |
2 |
includes(sigma3, asc); |
85 |
2 |
doesNotInclude(asc, sigma3); |
86 |
|
|
87 |
2 |
includes(asc, abc); |
88 |
2 |
doesNotInclude(abc, asc); |
89 |
|
|
90 |
2 |
includes(asw, asc); |
91 |
2 |
doesNotInclude(asc, asw); |
92 |
2 |
} |
93 |
|
|
94 |
11 |
TEST_F(TestTheoryBlackRegexpOperation, star_wildcards) |
95 |
|
{ |
96 |
4 |
Node sigma = d_nodeManager->mkNode(REGEXP_SIGMA); |
97 |
4 |
Node sigmaStar = d_nodeManager->mkNode(REGEXP_STAR, sigma); |
98 |
|
Node a = d_nodeManager->mkNode(STRING_TO_REGEXP, |
99 |
4 |
d_nodeManager->mkConst(String("a"))); |
100 |
|
Node c = d_nodeManager->mkNode(STRING_TO_REGEXP, |
101 |
4 |
d_nodeManager->mkConst(String("c"))); |
102 |
|
Node abc = d_nodeManager->mkNode(STRING_TO_REGEXP, |
103 |
4 |
d_nodeManager->mkConst(String("abc"))); |
104 |
|
|
105 |
4 |
Node _abc_ = d_nodeManager->mkNode(REGEXP_CONCAT, sigmaStar, abc, sigmaStar); |
106 |
|
Node _asc_ = |
107 |
4 |
d_nodeManager->mkNode(REGEXP_CONCAT, {sigmaStar, a, sigma, c, sigmaStar}); |
108 |
|
Node _sc_ = Rewriter::rewrite( |
109 |
4 |
d_nodeManager->mkNode(REGEXP_CONCAT, {sigmaStar, sigma, c, sigmaStar})); |
110 |
|
Node _as_ = Rewriter::rewrite( |
111 |
4 |
d_nodeManager->mkNode(REGEXP_CONCAT, {sigmaStar, a, sigma, sigmaStar})); |
112 |
|
Node _assc_ = d_nodeManager->mkNode( |
113 |
|
REGEXP_CONCAT, |
114 |
4 |
std::vector<Node>{sigmaStar, a, sigma, sigma, c, sigmaStar}); |
115 |
|
Node _csa_ = |
116 |
4 |
d_nodeManager->mkNode(REGEXP_CONCAT, {sigmaStar, c, sigma, a, sigmaStar}); |
117 |
|
Node _c_a_ = d_nodeManager->mkNode(REGEXP_CONCAT, |
118 |
4 |
{sigmaStar, c, sigmaStar, a, sigmaStar}); |
119 |
6 |
Node _s_s_ = Rewriter::rewrite(d_nodeManager->mkNode( |
120 |
14 |
REGEXP_CONCAT, {sigmaStar, sigma, sigmaStar, sigma, sigmaStar})); |
121 |
6 |
Node _a_abc_ = Rewriter::rewrite(d_nodeManager->mkNode( |
122 |
14 |
REGEXP_CONCAT, {sigmaStar, a, sigmaStar, abc, sigmaStar})); |
123 |
|
|
124 |
2 |
includes(_asc_, _abc_); |
125 |
2 |
doesNotInclude(_abc_, _asc_); |
126 |
2 |
doesNotInclude(_csa_, _abc_); |
127 |
2 |
doesNotInclude(_assc_, _asc_); |
128 |
2 |
doesNotInclude(_asc_, _assc_); |
129 |
2 |
includes(_sc_, abc); |
130 |
2 |
includes(_sc_, _abc_); |
131 |
2 |
includes(_sc_, _asc_); |
132 |
2 |
includes(_sc_, _assc_); |
133 |
2 |
doesNotInclude(_sc_, _csa_); |
134 |
2 |
includes(_as_, abc); |
135 |
2 |
includes(_as_, _abc_); |
136 |
2 |
includes(_as_, _asc_); |
137 |
2 |
includes(_as_, _assc_); |
138 |
2 |
doesNotInclude(_sc_, _csa_); |
139 |
2 |
includes(_s_s_, _c_a_); |
140 |
2 |
doesNotInclude(_c_a_, _s_s_); |
141 |
2 |
includes(_abc_, _a_abc_); |
142 |
2 |
doesNotInclude(_a_abc_, _abc_); |
143 |
2 |
} |
144 |
|
|
145 |
|
} // namespace test |
146 |
102255 |
} // namespace cvc5 |