Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Unit tests for symbolic regular expression operations.
11 : : */
12 : :
13 : : #include <cvc5/cvc5.h>
14 : :
15 : : #include <iostream>
16 : : #include <memory>
17 : : #include <vector>
18 : :
19 : : #include "expr/node.h"
20 : : #include "expr/node_manager.h"
21 : : #include "test_smt.h"
22 : : #include "theory/rewriter.h"
23 : : #include "theory/strings/regexp_entail.h"
24 : : #include "util/string.h"
25 : :
26 : : namespace cvc5::internal {
27 : :
28 : : using namespace theory;
29 : : using namespace theory::strings;
30 : :
31 : : namespace test {
32 : :
33 : : class TestTheoryBlackRegexpOperation : public TestSmt
34 : : {
35 : : protected:
36 : 3 : void SetUp() override { TestSmt::SetUp(); }
37 : :
38 : 15 : void includes(Node r1, Node r2)
39 : : {
40 : 15 : Rewriter* rr = d_slvEngine->getEnv().getRewriter();
41 : 15 : r1 = rr->rewrite(r1);
42 : 15 : r2 = rr->rewrite(r2);
43 : 15 : std::cout << r1 << " includes " << r2 << std::endl;
44 [ - + ][ + - ]: 15 : ASSERT_TRUE(RegExpEntail::regExpIncludes(r1, r2));
45 : : }
46 : :
47 : 12 : void doesNotInclude(Node r1, Node r2)
48 : : {
49 : 12 : Rewriter* rr = d_slvEngine->getEnv().getRewriter();
50 : 12 : r1 = rr->rewrite(r1);
51 : 12 : r2 = rr->rewrite(r2);
52 : 12 : std::cout << r1 << " does not include " << r2 << std::endl;
53 [ - + ][ + - ]: 12 : ASSERT_FALSE(RegExpEntail::regExpIncludes(r1, r2));
54 : : }
55 : : };
56 : :
57 : 4 : TEST_F(TestTheoryBlackRegexpOperation, basic)
58 : : {
59 : 1 : Node sigma = d_nodeManager->mkNode(Kind::REGEXP_ALLCHAR);
60 : 1 : Node sigmaStar = d_nodeManager->mkNode(Kind::REGEXP_STAR, sigma);
61 : 1 : Node a = d_nodeManager->mkNode(Kind::STRING_TO_REGEXP,
62 : 2 : d_nodeManager->mkConst(String("a")));
63 : 1 : Node c = d_nodeManager->mkNode(Kind::STRING_TO_REGEXP,
64 : 2 : d_nodeManager->mkConst(String("c")));
65 : 1 : Node abc = d_nodeManager->mkNode(Kind::STRING_TO_REGEXP,
66 : 2 : d_nodeManager->mkConst(String("abc")));
67 : 2 : Node sigma3 = d_nodeManager->mkNode(Kind::REGEXP_CONCAT, sigma, sigma, sigma);
68 : 2 : Node asc = d_nodeManager->mkNode(Kind::REGEXP_CONCAT, a, sigma, c);
69 : 2 : Node asw = d_nodeManager->mkNode(Kind::REGEXP_CONCAT, a, sigma, sigmaStar);
70 : :
71 : 1 : includes(sigma3, abc);
72 : 1 : doesNotInclude(abc, sigma3);
73 : :
74 : 1 : includes(sigma3, asc);
75 : 1 : doesNotInclude(asc, sigma3);
76 : :
77 : 1 : includes(asc, abc);
78 : 1 : doesNotInclude(abc, asc);
79 : :
80 : 1 : includes(asw, asc);
81 : 1 : doesNotInclude(asc, asw);
82 : 1 : }
83 : :
84 : 4 : TEST_F(TestTheoryBlackRegexpOperation, star_wildcards)
85 : : {
86 : 1 : Rewriter* rr = d_slvEngine->getEnv().getRewriter();
87 : 1 : Node sigma = d_nodeManager->mkNode(Kind::REGEXP_ALLCHAR);
88 : 1 : Node sigmaStar = d_nodeManager->mkNode(Kind::REGEXP_STAR, sigma);
89 : 1 : Node a = d_nodeManager->mkNode(Kind::STRING_TO_REGEXP,
90 : 2 : d_nodeManager->mkConst(String("a")));
91 : 1 : Node c = d_nodeManager->mkNode(Kind::STRING_TO_REGEXP,
92 : 2 : d_nodeManager->mkConst(String("c")));
93 : 1 : Node abc = d_nodeManager->mkNode(Kind::STRING_TO_REGEXP,
94 : 2 : d_nodeManager->mkConst(String("abc")));
95 : :
96 : : Node _abc_ =
97 : 2 : d_nodeManager->mkNode(Kind::REGEXP_CONCAT, sigmaStar, abc, sigmaStar);
98 : 7 : Node _asc_ = d_nodeManager->mkNode(Kind::REGEXP_CONCAT,
99 : 1 : {sigmaStar, a, sigma, c, sigmaStar});
100 : 4 : Node _sc_ = rr->rewrite(d_nodeManager->mkNode(
101 : 2 : Kind::REGEXP_CONCAT, {sigmaStar, sigma, c, sigmaStar}));
102 : 4 : Node _as_ = rr->rewrite(d_nodeManager->mkNode(
103 : 2 : Kind::REGEXP_CONCAT, {sigmaStar, a, sigma, sigmaStar}));
104 : : Node _assc_ = d_nodeManager->mkNode(
105 : : Kind::REGEXP_CONCAT,
106 : 8 : std::vector<Node>{sigmaStar, a, sigma, sigma, c, sigmaStar});
107 : 7 : Node _csa_ = d_nodeManager->mkNode(Kind::REGEXP_CONCAT,
108 : 1 : {sigmaStar, c, sigma, a, sigmaStar});
109 : 7 : Node _c_a_ = d_nodeManager->mkNode(Kind::REGEXP_CONCAT,
110 : 1 : {sigmaStar, c, sigmaStar, a, sigmaStar});
111 : 5 : Node _s_s_ = rr->rewrite(d_nodeManager->mkNode(
112 : 2 : Kind::REGEXP_CONCAT, {sigmaStar, sigma, sigmaStar, sigma, sigmaStar}));
113 : 5 : Node _a_abc_ = rr->rewrite(d_nodeManager->mkNode(
114 : 2 : Kind::REGEXP_CONCAT, {sigmaStar, a, sigmaStar, abc, sigmaStar}));
115 : :
116 : 1 : includes(_asc_, _abc_);
117 : 1 : doesNotInclude(_abc_, _asc_);
118 : 1 : doesNotInclude(_csa_, _abc_);
119 : 1 : doesNotInclude(_assc_, _asc_);
120 : 1 : doesNotInclude(_asc_, _assc_);
121 : 1 : includes(_sc_, abc);
122 : 1 : includes(_sc_, _abc_);
123 : 1 : includes(_sc_, _asc_);
124 : 1 : includes(_sc_, _assc_);
125 : 1 : doesNotInclude(_sc_, _csa_);
126 : 1 : includes(_as_, abc);
127 : 1 : includes(_as_, _abc_);
128 : 1 : includes(_as_, _asc_);
129 : 1 : includes(_as_, _assc_);
130 : 1 : doesNotInclude(_sc_, _csa_);
131 : 1 : includes(_s_s_, _c_a_);
132 : 1 : doesNotInclude(_c_a_, _s_s_);
133 : 1 : includes(_abc_, _a_abc_);
134 : 1 : doesNotInclude(_a_abc_, _abc_);
135 : 1 : }
136 : :
137 : 4 : TEST_F(TestTheoryBlackRegexpOperation, generalizedRegExp)
138 : : {
139 : 1 : RegExpEntail re(d_nodeManager.get(), nullptr);
140 : :
141 : 1 : TypeNode strType = d_nodeManager->stringType();
142 : 1 : TypeNode intType = d_nodeManager->integerType();
143 : :
144 : 1 : Node abc = d_nodeManager->mkConst(String("abc"));
145 : 2 : Node a = d_nodeManager->mkDummySkolem("a", intType);
146 : 2 : Node s = d_nodeManager->mkDummySkolem("s", strType);
147 : 1 : Node fia = d_nodeManager->mkNode(Kind::STRING_ITOS, a);
148 : 1 : Node fils = d_nodeManager->mkNode(
149 : 2 : Kind::STRING_ITOS, d_nodeManager->mkNode(Kind::STRING_LENGTH, s));
150 : :
151 : 1 : Node sigma = d_nodeManager->mkNode(Kind::REGEXP_ALLCHAR);
152 : 1 : Node sigmaStar = d_nodeManager->mkNode(Kind::REGEXP_STAR, sigma);
153 : 1 : Node rabc = d_nodeManager->mkNode(Kind::STRING_TO_REGEXP,
154 : 2 : d_nodeManager->mkConst(String("abc")));
155 : 1 : Node digRange = d_nodeManager->mkNode(Kind::REGEXP_RANGE,
156 : 2 : d_nodeManager->mkConst(String("0")),
157 : 4 : d_nodeManager->mkConst(String("9")));
158 : 1 : Node digRangeStar = d_nodeManager->mkNode(Kind::REGEXP_STAR, digRange);
159 : : Node digRangePlus =
160 : 2 : d_nodeManager->mkNode(Kind::REGEXP_CONCAT, digRange, digRangeStar);
161 : :
162 [ - + ][ + - ]: 1 : ASSERT_TRUE(re.getGeneralizedConstRegExp(s).isNull());
163 [ - + ][ + - ]: 2 : ASSERT_EQ(re.getGeneralizedConstRegExp(fia), digRangeStar);
164 [ - + ][ + - ]: 2 : ASSERT_EQ(re.getGeneralizedConstRegExp(fils), digRangePlus);
165 [ - + ][ + - ]: 2 : ASSERT_EQ(re.getGeneralizedConstRegExp(abc), rabc);
166 : :
167 : 2 : Node ss = d_nodeManager->mkNode(Kind::STRING_CONCAT, s, s);
168 [ - + ][ + - ]: 1 : ASSERT_TRUE(re.getGeneralizedConstRegExp(ss).isNull());
169 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
170 : :
171 : : } // namespace test
172 : : } // namespace cvc5::internal
|
