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 : : * Black box testing of grammar-related functions of the C API.
11 : : */
12 : :
13 : : extern "C" {
14 : : #include <cvc5/c/cvc5.h>
15 : : }
16 : :
17 : : #include "base/output.h"
18 : : #include "gtest/gtest.h"
19 : :
20 : : namespace cvc5::internal::test {
21 : :
22 : : class TestCApiBlackGrammar : public ::testing::Test
23 : : {
24 : : protected:
25 : 100 : void SetUp() override
26 : : {
27 : 100 : d_tm = cvc5_term_manager_new();
28 : 100 : d_solver = cvc5_new(d_tm);
29 : 100 : d_bool = cvc5_get_boolean_sort(d_tm);
30 : 100 : d_int = cvc5_get_integer_sort(d_tm);
31 : 100 : d_real = cvc5_get_real_sort(d_tm);
32 : 100 : d_str = cvc5_get_string_sort(d_tm);
33 : 100 : d_uninterpreted = cvc5_mk_uninterpreted_sort(d_tm, "u");
34 : 100 : }
35 : 74 : void TearDown() override
36 : : {
37 : 74 : cvc5_delete(d_solver);
38 : 74 : cvc5_term_manager_delete(d_tm);
39 : 74 : }
40 : :
41 : : Cvc5TermManager* d_tm;
42 : : Cvc5* d_solver;
43 : : Cvc5Sort d_bool;
44 : : Cvc5Sort d_int;
45 : : Cvc5Sort d_real;
46 : : Cvc5Sort d_str;
47 : : Cvc5Sort d_uninterpreted;
48 : : };
49 : :
50 : 106 : TEST_F(TestCApiBlackGrammar, to_string)
51 : : {
52 : 27 : cvc5_set_option(d_solver, "sygus", "true");
53 : 27 : Cvc5Term start = cvc5_mk_var(d_tm, d_bool, "start");
54 : 27 : std::vector<Cvc5Term> bvars;
55 : 27 : std::vector<Cvc5Term> symbols = {start};
56 : 54 : Cvc5Grammar g = cvc5_mk_grammar(
57 : 54 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
58 [ - + ][ + - ]: 27 : ASSERT_EQ(cvc5_grammar_to_string(g), std::string(""));
59 : 27 : cvc5_grammar_add_rule(g, start, cvc5_mk_false(d_tm));
60 : 27 : ASSERT_DEATH(cvc5_grammar_to_string(nullptr), "invalid grammar");
61 [ - + ][ + - ]: 26 : ASSERT_NE(cvc5_grammar_to_string(g), std::string(""));
62 [ + - ][ + - ]: 26 : }
63 : :
64 : 92 : TEST_F(TestCApiBlackGrammar, add_rule)
65 : : {
66 : 26 : cvc5_set_option(d_solver, "sygus", "true");
67 : 26 : Cvc5Term start = cvc5_mk_var(d_tm, d_bool, "start");
68 : 26 : Cvc5Term nts = cvc5_mk_var(d_tm, d_bool, "nts");
69 : :
70 : 26 : std::vector<Cvc5Term> bvars;
71 : 26 : std::vector<Cvc5Term> symbols = {start};
72 : 52 : Cvc5Grammar g = cvc5_mk_grammar(
73 : 52 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
74 : :
75 : 26 : cvc5_grammar_add_rule(g, start, cvc5_mk_false(d_tm));
76 : :
77 : 26 : ASSERT_DEATH(cvc5_grammar_add_rule(nullptr, start, cvc5_mk_false(d_tm)),
78 : : "invalid grammar");
79 : 25 : ASSERT_DEATH(cvc5_grammar_add_rule(g, nullptr, cvc5_mk_false(d_tm)),
80 : : "invalid term");
81 : 24 : ASSERT_DEATH(cvc5_grammar_add_rule(g, start, nullptr), "invalid term");
82 : :
83 : 23 : ASSERT_DEATH(cvc5_grammar_add_rule(g, nts, cvc5_mk_false(d_tm)),
84 : : "invalid argument");
85 : 22 : ASSERT_DEATH(cvc5_grammar_add_rule(g, start, cvc5_mk_integer_int64(d_tm, 0)),
86 : : "same sort");
87 : :
88 : 21 : (void)cvc5_synth_fun_with_grammar(d_solver, "f", 0, nullptr, d_bool, g);
89 : 21 : ASSERT_DEATH(cvc5_grammar_add_rule(g, start, cvc5_mk_false(d_tm)),
90 : : "cannot be modified");
91 [ + - ][ + - ]: 20 : }
92 : :
93 : 64 : TEST_F(TestCApiBlackGrammar, add_rules)
94 : : {
95 : 20 : cvc5_set_option(d_solver, "sygus", "true");
96 : 20 : Cvc5Term start = cvc5_mk_var(d_tm, d_bool, "start");
97 : 20 : Cvc5Term nts = cvc5_mk_var(d_tm, d_bool, "nts");
98 : :
99 : 20 : std::vector<Cvc5Term> bvars;
100 : 20 : std::vector<Cvc5Term> symbols = {start};
101 : 40 : Cvc5Grammar g = cvc5_mk_grammar(
102 : 40 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
103 : :
104 : 20 : std::vector<Cvc5Term> rules = {cvc5_mk_false(d_tm)};
105 : 20 : cvc5_grammar_add_rules(g, start, rules.size(), rules.data());
106 : :
107 : 20 : ASSERT_DEATH(
108 : : cvc5_grammar_add_rules(nullptr, start, rules.size(), rules.data()),
109 : : "invalid grammar");
110 : 19 : ASSERT_DEATH(cvc5_grammar_add_rules(g, nullptr, rules.size(), rules.data()),
111 : : "invalid term");
112 : 18 : ASSERT_DEATH(cvc5_grammar_add_rules(g, start, 0, nullptr),
113 : : "unexpected NULL argument");
114 : :
115 : 17 : ASSERT_DEATH(cvc5_grammar_add_rules(g, nts, rules.size(), rules.data()),
116 : : "invalid argument");
117 : 16 : rules.push_back(nullptr);
118 : 16 : ASSERT_DEATH(cvc5_grammar_add_rules(g, start, rules.size(), rules.data()),
119 : : "invalid term at index 1");
120 : 15 : rules = {cvc5_mk_false(d_tm)};
121 : 15 : ASSERT_DEATH(cvc5_grammar_add_rules(g, nts, rules.size(), rules.data()),
122 : : "invalid argument");
123 : 14 : rules = {cvc5_mk_integer_int64(d_tm, 0)};
124 : 14 : ASSERT_DEATH(cvc5_grammar_add_rules(g, start, rules.size(), rules.data()),
125 : : "Expected term with sort Bool");
126 : :
127 : 13 : (void)cvc5_synth_fun_with_grammar(d_solver, "f", 0, nullptr, d_bool, g);
128 : :
129 : 13 : rules = {cvc5_mk_false(d_tm)};
130 : 13 : ASSERT_DEATH(cvc5_grammar_add_rules(g, start, rules.size(), rules.data()),
131 : : "cannot be modified");
132 [ + - ][ + - ]: 12 : }
[ + - ]
133 : :
134 : 40 : TEST_F(TestCApiBlackGrammar, add_any_constant)
135 : : {
136 : 12 : cvc5_set_option(d_solver, "sygus", "true");
137 : :
138 : 12 : Cvc5Term start = cvc5_mk_var(d_tm, d_bool, "start");
139 : 12 : Cvc5Term nts = cvc5_mk_var(d_tm, d_bool, "nts");
140 : :
141 : 12 : std::vector<Cvc5Term> bvars;
142 : 12 : std::vector<Cvc5Term> symbols = {start};
143 : 24 : Cvc5Grammar g = cvc5_mk_grammar(
144 : 24 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
145 : :
146 : 12 : cvc5_grammar_add_any_constant(g, start);
147 : 12 : cvc5_grammar_add_any_constant(g, start);
148 : :
149 : 12 : ASSERT_DEATH(cvc5_grammar_add_any_constant(nullptr, start),
150 : : "invalid grammar");
151 : 11 : ASSERT_DEATH(cvc5_grammar_add_any_constant(g, nullptr), "invalid term");
152 : 10 : ASSERT_DEATH(cvc5_grammar_add_any_constant(g, nts),
153 : : "expected ntSymbol to be one of the non-terminal symbols");
154 : :
155 : 9 : (void)cvc5_synth_fun_with_grammar(d_solver, "f", 0, nullptr, d_bool, g);
156 : :
157 : 9 : ASSERT_DEATH(cvc5_grammar_add_any_constant(g, start), "cannot be modified");
158 [ + - ][ + - ]: 8 : }
159 : :
160 : 24 : TEST_F(TestCApiBlackGrammar, add_any_variable)
161 : : {
162 : 8 : cvc5_set_option(d_solver, "sygus", "true");
163 : :
164 : 8 : Cvc5Term start = cvc5_mk_var(d_tm, d_bool, "start");
165 : 8 : Cvc5Term nts = cvc5_mk_var(d_tm, d_bool, "nts");
166 : :
167 : 8 : Cvc5Term x = cvc5_mk_var(d_tm, d_bool, "x");
168 : 8 : std::vector<Cvc5Term> bvars = {x};
169 : 8 : std::vector<Cvc5Term> symbols = {start};
170 : 16 : Cvc5Grammar g1 = cvc5_mk_grammar(
171 : 16 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
172 : : Cvc5Grammar g2 =
173 : 8 : cvc5_mk_grammar(d_solver, 0, nullptr, symbols.size(), symbols.data());
174 : :
175 : 8 : cvc5_grammar_add_any_variable(g1, start);
176 : 8 : cvc5_grammar_add_any_variable(g1, start);
177 : 8 : cvc5_grammar_add_any_variable(g2, start);
178 : :
179 : 8 : ASSERT_DEATH(cvc5_grammar_add_any_variable(nullptr, start),
180 : : "invalid grammar");
181 : 7 : ASSERT_DEATH(cvc5_grammar_add_any_variable(g1, nullptr), "invalid term");
182 : 6 : ASSERT_DEATH(cvc5_grammar_add_any_variable(g1, nts),
183 : : "expected ntSymbol to be one of the non-terminal symbols");
184 : :
185 : 5 : (void)cvc5_synth_fun_with_grammar(d_solver, "f", 0, nullptr, d_bool, g1);
186 : :
187 : 5 : ASSERT_DEATH(cvc5_grammar_add_any_variable(g1, start), "cannot be modified");
188 [ + - ][ + - ]: 4 : }
189 : :
190 : 14 : TEST_F(TestCApiBlackGrammar, equal_hash)
191 : : {
192 : 4 : cvc5_set_option(d_solver, "sygus", "true");
193 : :
194 : 4 : Cvc5Term x = cvc5_mk_var(d_tm, d_bool, "x");
195 : 4 : Cvc5Term start1 = cvc5_mk_var(d_tm, d_bool, "start");
196 : 4 : Cvc5Term start2 = cvc5_mk_var(d_tm, d_bool, "start");
197 : 4 : std::vector<Cvc5Term> bvars, symbols;
198 : : Cvc5Grammar g1, g2;
199 : :
200 : : {
201 : 4 : symbols = {start1};
202 : 4 : bvars = {};
203 : 8 : g1 = cvc5_mk_grammar(
204 : 8 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
205 : 8 : g2 = cvc5_mk_grammar(
206 : 8 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
207 [ - + ][ + - ]: 4 : ASSERT_EQ(cvc5_grammar_hash(g1), cvc5_grammar_hash(g1));
208 [ - + ][ + - ]: 4 : ASSERT_EQ(cvc5_grammar_hash(g1), cvc5_grammar_hash(g2));
209 [ - + ][ + - ]: 4 : ASSERT_TRUE(cvc5_grammar_is_equal(g1, g1));
210 [ - + ][ + - ]: 4 : ASSERT_FALSE(cvc5_grammar_is_equal(g1, g2));
211 [ - + ][ + - ]: 4 : ASSERT_TRUE(cvc5_grammar_is_disequal(g1, g2));
212 : : }
213 : :
214 : : {
215 : 4 : symbols = {start1};
216 : 4 : bvars = {};
217 : 8 : g1 = cvc5_mk_grammar(
218 : 8 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
219 : 4 : bvars = {x};
220 : 8 : g2 = cvc5_mk_grammar(
221 : 8 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
222 [ - + ][ + - ]: 4 : ASSERT_NE(cvc5_grammar_hash(g1), cvc5_grammar_hash(g2));
223 [ - + ][ + - ]: 4 : ASSERT_TRUE(cvc5_grammar_is_equal(g1, g1));
224 [ - + ][ + - ]: 4 : ASSERT_FALSE(cvc5_grammar_is_equal(g1, g2));
225 [ - + ][ + - ]: 4 : ASSERT_TRUE(cvc5_grammar_is_disequal(g1, g2));
226 : : }
227 : :
228 : : {
229 : 4 : bvars = {x};
230 : 4 : symbols = {start1};
231 : 8 : g1 = cvc5_mk_grammar(
232 : 8 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
233 : 4 : symbols = {start2};
234 : 8 : g2 = cvc5_mk_grammar(
235 : 8 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
236 [ - + ][ + - ]: 4 : ASSERT_NE(cvc5_grammar_hash(g1), cvc5_grammar_hash(g2));
237 [ - + ][ + - ]: 4 : ASSERT_TRUE(cvc5_grammar_is_equal(g1, g1));
238 [ - + ][ + - ]: 4 : ASSERT_FALSE(cvc5_grammar_is_equal(g1, g2));
239 [ - + ][ + - ]: 4 : ASSERT_TRUE(cvc5_grammar_is_disequal(g1, g2));
240 : : }
241 : :
242 : : {
243 : 4 : bvars = {x};
244 : 4 : symbols = {start1};
245 : 8 : g1 = cvc5_mk_grammar(
246 : 8 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
247 : 8 : g2 = cvc5_mk_grammar(
248 : 8 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
249 : 4 : cvc5_grammar_add_any_variable(g2, start1);
250 [ - + ][ + - ]: 4 : ASSERT_NE(cvc5_grammar_hash(g1), cvc5_grammar_hash(g2));
251 [ - + ][ + - ]: 4 : ASSERT_TRUE(cvc5_grammar_is_equal(g1, g1));
252 [ - + ][ + - ]: 4 : ASSERT_FALSE(cvc5_grammar_is_equal(g1, g2));
253 [ - + ][ + - ]: 4 : ASSERT_TRUE(cvc5_grammar_is_disequal(g1, g2));
254 : : }
255 : :
256 : : {
257 : 4 : bvars = {x};
258 : 4 : symbols = {start1};
259 : 8 : g1 = cvc5_mk_grammar(
260 : 8 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
261 : 8 : g2 = cvc5_mk_grammar(
262 : 8 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
263 : 4 : std::vector<Cvc5Term> rules = {cvc5_mk_false(d_tm)};
264 : 4 : cvc5_grammar_add_rules(g1, start1, rules.size(), rules.data());
265 : 4 : cvc5_grammar_add_rules(g2, start1, rules.size(), rules.data());
266 [ - + ][ + - ]: 4 : ASSERT_EQ(cvc5_grammar_hash(g1), cvc5_grammar_hash(g2));
267 [ - + ][ + - ]: 4 : ASSERT_TRUE(cvc5_grammar_is_equal(g1, g1));
268 [ - + ][ + - ]: 4 : ASSERT_FALSE(cvc5_grammar_is_equal(g1, g2));
269 [ - + ][ + - ]: 4 : ASSERT_TRUE(cvc5_grammar_is_disequal(g1, g2));
270 [ + - ]: 4 : }
271 : :
272 : : {
273 : 4 : bvars = {x};
274 : 4 : symbols = {start1};
275 : 8 : g1 = cvc5_mk_grammar(
276 : 8 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
277 : 8 : g2 = cvc5_mk_grammar(
278 : 8 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
279 : 4 : std::vector<Cvc5Term> rules2 = {cvc5_mk_false(d_tm)};
280 : 4 : cvc5_grammar_add_rules(g2, start1, rules2.size(), rules2.data());
281 [ - + ][ + - ]: 4 : ASSERT_NE(cvc5_grammar_hash(g1), cvc5_grammar_hash(g2));
282 [ - + ][ + - ]: 4 : ASSERT_TRUE(cvc5_grammar_is_equal(g1, g1));
283 [ - + ][ + - ]: 4 : ASSERT_FALSE(cvc5_grammar_is_equal(g1, g2));
284 [ - + ][ + - ]: 4 : ASSERT_TRUE(cvc5_grammar_is_disequal(g1, g2));
285 [ + - ]: 4 : }
286 : :
287 : : {
288 : 4 : bvars = {x};
289 : 4 : symbols = {start1};
290 : 8 : g1 = cvc5_mk_grammar(
291 : 8 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
292 : 8 : g2 = cvc5_mk_grammar(
293 : 8 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
294 : 4 : std::vector<Cvc5Term> rules1 = {cvc5_mk_true(d_tm)};
295 : 4 : std::vector<Cvc5Term> rules2 = {cvc5_mk_false(d_tm)};
296 : 4 : cvc5_grammar_add_rules(g1, start1, rules1.size(), rules1.data());
297 : 4 : cvc5_grammar_add_rules(g2, start1, rules2.size(), rules2.data());
298 [ - + ][ + - ]: 4 : ASSERT_NE(cvc5_grammar_hash(g1), cvc5_grammar_hash(g2));
299 [ - + ][ + - ]: 4 : ASSERT_TRUE(cvc5_grammar_is_equal(g1, g1));
300 [ - + ][ + - ]: 4 : ASSERT_FALSE(cvc5_grammar_is_equal(g1, g2));
301 [ - + ][ + - ]: 4 : ASSERT_TRUE(cvc5_grammar_is_disequal(g1, g2));
302 [ + - ][ + - ]: 4 : }
303 : 4 : ASSERT_DEATH(cvc5_grammar_hash(nullptr), "invalid grammar");
304 [ + - ][ + - ]: 3 : }
305 : :
306 : 8 : TEST_F(TestCApiBlackGrammar, copy_release)
307 : : {
308 : 3 : ASSERT_DEATH(cvc5_grammar_copy(nullptr), "invalid grammar");
309 : 2 : ASSERT_DEATH(cvc5_grammar_release(nullptr), "invalid grammar");
310 : 1 : cvc5_set_option(d_solver, "sygus", "true");
311 : 1 : Cvc5Term start = cvc5_mk_var(d_tm, d_bool, "start");
312 : 1 : Cvc5Term x = cvc5_mk_var(d_tm, d_bool, "x");
313 : 1 : std::vector<Cvc5Term> bvars = {x};
314 : 1 : std::vector<Cvc5Term> symbols = {start};
315 : 2 : Cvc5Grammar g1 = cvc5_mk_grammar(
316 : 2 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
317 : 1 : Cvc5Grammar g2 = cvc5_grammar_copy(g1);
318 [ - + ][ + - ]: 1 : ASSERT_EQ(cvc5_grammar_hash(g1), cvc5_grammar_hash(g2));
319 : 1 : cvc5_grammar_release(g1);
320 [ - + ][ + - ]: 1 : ASSERT_EQ(cvc5_grammar_hash(g1), cvc5_grammar_hash(g2));
321 : 1 : cvc5_grammar_release(g1);
322 : : // we cannot reliably check that querying on the (now freed) grammar fails
323 : : // unless ASAN is enabled
324 : : }
325 : : } // namespace cvc5::internal::test
|
