Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 : : * Testing functions that are not exposed by the C API for code coverage.
14 : : */
15 : :
16 : : #include <cvc5/cvc5.h>
17 : : #include <cvc5/cvc5_parser.h>
18 : :
19 : : #include "gtest/gtest.h"
20 : :
21 : : namespace cvc5::internal::test {
22 : :
23 : : class TestCApiBlackUncovered : public ::testing::Test
24 : : {
25 : : protected:
26 : 13 : void SetUp() override
27 : : {
28 : 13 : d_solver.reset(new cvc5::Solver(d_tm));
29 : 13 : d_bool = d_tm.getBooleanSort();
30 : 13 : d_int = d_tm.getIntegerSort();
31 : 13 : }
32 : : cvc5::TermManager d_tm;
33 : : std::unique_ptr<cvc5::Solver> d_solver;
34 : : cvc5::Sort d_bool;
35 : : cvc5::Sort d_int;
36 : : };
37 : :
38 : 2 : TEST_F(TestCApiBlackUncovered, deprecated)
39 : : {
40 : 1 : std::stringstream ss;
41 : 1 : ss << cvc5::Kind::EQUAL << cvc5::kindToString(cvc5::Kind::EQUAL);
42 : 1 : ss << cvc5::SortKind::ARRAY_SORT
43 : 1 : << cvc5::sortKindToString(cvc5::SortKind::ARRAY_SORT);
44 : :
45 : 1 : Solver slv;
46 : 1 : (void)slv.getBooleanSort();
47 : 1 : (void)slv.getIntegerSort();
48 : 1 : (void)slv.getRealSort();
49 : 1 : (void)slv.getRegExpSort();
50 : 1 : (void)slv.getRoundingModeSort();
51 : 1 : (void)slv.getStringSort();
52 : 1 : (void)slv.mkArraySort(slv.getBooleanSort(), slv.getIntegerSort());
53 : 1 : (void)slv.mkBitVectorSort(32);
54 : 1 : (void)slv.mkFloatingPointSort(5, 11);
55 : 1 : (void)slv.mkFiniteFieldSort("37");
56 : :
57 : : {
58 : 3 : DatatypeDecl decl = slv.mkDatatypeDecl("list");
59 : 2 : DatatypeConstructorDecl cons = slv.mkDatatypeConstructorDecl("cons");
60 : 1 : cons.addSelector("head", slv.getIntegerSort());
61 : 1 : decl.addConstructor(cons);
62 : 1 : decl.addConstructor(slv.mkDatatypeConstructorDecl("nil"));
63 : 1 : (void)slv.mkDatatypeSort(decl);
64 : : }
65 : : {
66 : 2 : DatatypeDecl decl1 = slv.mkDatatypeDecl("list1");
67 : 2 : DatatypeConstructorDecl cons1 = slv.mkDatatypeConstructorDecl("cons1");
68 : 1 : cons1.addSelector("head1", slv.getIntegerSort());
69 : 1 : decl1.addConstructor(cons1);
70 : 2 : DatatypeConstructorDecl nil1 = slv.mkDatatypeConstructorDecl("nil1");
71 : 1 : decl1.addConstructor(nil1);
72 : 2 : DatatypeDecl decl2 = slv.mkDatatypeDecl("list2");
73 : 2 : DatatypeConstructorDecl cons2 = slv.mkDatatypeConstructorDecl("cons2");
74 : 1 : cons2.addSelector("head2", slv.getIntegerSort());
75 : 1 : decl2.addConstructor(cons2);
76 : 2 : DatatypeConstructorDecl nil2 = slv.mkDatatypeConstructorDecl("nil2");
77 : 1 : decl2.addConstructor(nil2);
78 : 4 : std::vector<DatatypeDecl> decls = {decl1, decl2};
79 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(slv.mkDatatypeSorts(decls));
80 : : }
81 : :
82 : 2 : (void)slv.mkFunctionSort({slv.mkUninterpretedSort("u")},
83 : 3 : slv.getIntegerSort());
84 : 1 : (void)slv.mkParamSort("T");
85 : 2 : (void)slv.mkPredicateSort({slv.getIntegerSort()});
86 : :
87 [ + + ][ - - ]: 7 : (void)slv.mkRecordSort({std::make_pair("b", slv.getBooleanSort()),
88 : 2 : std::make_pair("bv", slv.mkBitVectorSort(8)),
89 : 5 : std::make_pair("i", slv.getIntegerSort())});
90 : 1 : (void)slv.mkSetSort(slv.getBooleanSort());
91 : 1 : (void)slv.mkBagSort(slv.getBooleanSort());
92 : 1 : (void)slv.mkSequenceSort(slv.getBooleanSort());
93 : 1 : (void)slv.mkAbstractSort(SortKind::ARRAY_SORT);
94 : 1 : (void)slv.mkUninterpretedSort("u");
95 : 1 : (void)slv.mkUnresolvedDatatypeSort("u");
96 : 1 : (void)slv.mkUninterpretedSortConstructorSort(2, "s");
97 : 2 : (void)slv.mkTupleSort({slv.getIntegerSort()});
98 : 1 : (void)slv.mkNullableSort({slv.getIntegerSort()});
99 [ + + ][ - - ]: 4 : (void)slv.mkTerm(Kind::STRING_IN_REGEXP,
100 : 4 : {slv.mkConst(slv.getStringSort(), "s"), slv.mkRegexpAll()});
101 : 1 : (void)slv.mkTerm(slv.mkOp(Kind::REGEXP_ALLCHAR));
102 : 2 : (void)slv.mkTuple({slv.mkBitVector(3, "101", 2)});
103 : 1 : (void)slv.mkNullableSome(slv.mkBitVector(3, "101", 2));
104 : 1 : (void)slv.mkNullableVal(slv.mkNullableSome(slv.mkInteger(5)));
105 : 1 : (void)slv.mkNullableNull(slv.mkNullableSort(slv.getBooleanSort()));
106 : 1 : (void)slv.mkNullableIsNull(slv.mkNullableSome(slv.mkInteger(5)));
107 : 1 : (void)slv.mkNullableIsSome(slv.mkNullableSome(slv.mkInteger(5)));
108 : 1 : (void)slv.mkNullableSort(slv.getBooleanSort());
109 [ + + ][ - - ]: 4 : (void)slv.mkNullableLift(Kind::ADD,
110 : 1 : {slv.mkNullableSome(slv.mkInteger(1)),
111 : 4 : slv.mkNullableSome(slv.mkInteger(2))});
112 : 1 : (void)slv.mkOp(Kind::DIVISIBLE, "2147483648");
113 : 1 : (void)slv.mkOp(Kind::TUPLE_PROJECT, {1, 2, 2});
114 : :
115 : 1 : (void)slv.mkTrue();
116 : 1 : (void)slv.mkFalse();
117 : 1 : (void)slv.mkBoolean(true);
118 : 1 : (void)slv.mkPi();
119 : 1 : (void)slv.mkInteger("2");
120 : 1 : (void)slv.mkInteger(2);
121 : 1 : (void)slv.mkReal("2.1");
122 : 1 : (void)slv.mkReal(2);
123 : 1 : (void)slv.mkReal(2, 3);
124 : 1 : (void)slv.mkRegexpAll();
125 : 1 : (void)slv.mkRegexpAllchar();
126 : 1 : (void)slv.mkRegexpNone();
127 : 1 : (void)slv.mkEmptySet(slv.mkSetSort(slv.getIntegerSort()));
128 : 1 : (void)slv.mkEmptyBag(slv.mkBagSort(slv.getIntegerSort()));
129 : 1 : (void)slv.mkSepEmp();
130 : 1 : (void)slv.mkSepNil(slv.getIntegerSort());
131 : 1 : (void)slv.mkString("asdfasdf");
132 : 1 : std::wstring s;
133 : 1 : (void)slv.mkString(s);
134 : 1 : (void)slv.mkEmptySequence(slv.getIntegerSort());
135 : 1 : (void)slv.mkUniverseSet(slv.getIntegerSort());
136 : 1 : (void)slv.mkBitVector(32, 2);
137 : 1 : (void)slv.mkBitVector(32, "2", 10);
138 : 1 : (void)slv.mkFiniteFieldElem("0", slv.mkFiniteFieldSort("7"));
139 : 1 : (void)slv.mkConstArray(
140 : 2 : slv.mkArraySort(slv.getIntegerSort(), slv.getIntegerSort()),
141 : 2 : slv.mkInteger(2));
142 : 1 : (void)slv.mkFloatingPointPosInf(5, 11);
143 : 1 : (void)slv.mkFloatingPointNegInf(5, 11);
144 : 1 : (void)slv.mkFloatingPointNaN(5, 11);
145 : 1 : (void)slv.mkFloatingPointPosZero(5, 11);
146 : 1 : (void)slv.mkFloatingPointNegZero(5, 11);
147 : 1 : (void)slv.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN);
148 : 1 : (void)slv.mkFloatingPoint(5, 11, slv.mkBitVector(16));
149 : 1 : (void)slv.mkFloatingPoint(
150 : 2 : slv.mkBitVector(1), slv.mkBitVector(5), slv.mkBitVector(10));
151 : 1 : (void)slv.mkCardinalityConstraint(slv.mkUninterpretedSort("u"), 3);
152 : :
153 : 1 : (void)slv.mkVar(slv.getIntegerSort());
154 : 2 : (void)slv.mkDatatypeDecl("paramlist", {slv.mkParamSort("T")});
155 : 1 : (void)cvc5::parser::SymbolManager(&slv);
156 : : }
157 : :
158 : 2 : TEST_F(TestCApiBlackUncovered, stream_operators)
159 : : {
160 : 2 : std::stringstream ss;
161 : 1 : ss << cvc5::Kind::EQUAL << std::to_string(cvc5::Kind::EQUAL);
162 : 1 : ss << cvc5::SortKind::ARRAY_SORT
163 : 1 : << std::to_string(cvc5::SortKind::ARRAY_SORT);
164 : 1 : ss << cvc5::RoundingMode::ROUND_TOWARD_NEGATIVE
165 : 1 : << std::to_string(cvc5::RoundingMode::ROUND_TOWARD_NEGATIVE);
166 : 1 : ss << cvc5::UnknownExplanation::UNKNOWN_REASON
167 : 1 : << std::to_string(cvc5::UnknownExplanation::UNKNOWN_REASON);
168 : 1 : ss << cvc5::modes::BlockModelsMode::LITERALS
169 : 1 : << std::to_string(cvc5::modes::BlockModelsMode::LITERALS);
170 : 1 : ss << cvc5::modes::LearnedLitType::PREPROCESS
171 : 1 : << std::to_string(cvc5::modes::LearnedLitType::PREPROCESS);
172 : 1 : ss << cvc5::modes::ProofComponent::FULL
173 : 1 : << std::to_string(cvc5::modes::ProofComponent::FULL);
174 : 1 : ss << cvc5::modes::FindSynthTarget::ENUM
175 : 1 : << std::to_string(cvc5::modes::FindSynthTarget::ENUM);
176 : 1 : ss << cvc5::modes::InputLanguage::SMT_LIB_2_6
177 : 1 : << std::to_string(cvc5::modes::InputLanguage::SMT_LIB_2_6);
178 : 1 : ss << cvc5::modes::ProofFormat::LFSC
179 : 1 : << std::to_string(cvc5::modes::ProofFormat::LFSC);
180 : 1 : ss << cvc5::ProofRule::ASSUME << std::to_string(cvc5::ProofRule::ASSUME);
181 : 1 : ss << cvc5::ProofRewriteRule::NONE
182 : 1 : << std::to_string(cvc5::ProofRewriteRule::NONE);
183 : 1 : ss << cvc5::SkolemId::PURIFY << std::to_string(cvc5::SkolemId::PURIFY);
184 : 1 : ss << d_tm.mkOp(Kind::BITVECTOR_EXTRACT, {4, 0});
185 : 1 : ss << d_tm.mkDatatypeConstructorDecl("cons");
186 : :
187 : 2 : Sort intsort = d_tm.getIntegerSort();
188 : 2 : Term x = d_tm.mkConst(intsort, "x");
189 : :
190 [ + + ][ - - ]: 3 : ss << std::vector<Term>{x, x};
191 [ + + ][ - - ]: 3 : ss << std::set<Term>{x, x};
192 [ + + ][ - - ]: 3 : ss << std::unordered_set<Term>{x, x};
193 : :
194 : 1 : d_solver->setOption("sygus", "true");
195 : 1 : (void)d_solver->synthFun("f", {}, d_bool);
196 : 1 : ss << d_solver->checkSynth();
197 : 2 : ss << d_solver->mkGrammar({}, {d_tm.mkVar(d_bool)});
198 : 1 : ss << d_solver->checkSat();
199 : :
200 : 3 : DatatypeDecl decl = d_tm.mkDatatypeDecl("list");
201 : 3 : DatatypeConstructorDecl cons = d_tm.mkDatatypeConstructorDecl("cons");
202 : 1 : cons.addSelector("head", d_int);
203 : 1 : decl.addConstructor(cons);
204 : 2 : Datatype dt = d_tm.mkDatatypeSort(decl).getDatatype();
205 : 1 : ss << dt;
206 : 2 : DatatypeConstructor ctor = dt[0];
207 : 1 : ss << ctor;
208 : 3 : DatatypeSelector head = ctor.getSelector("head");
209 : 1 : ss << head;
210 : :
211 : 3 : OptionInfo info = d_solver->getOptionInfo("verbose");
212 : 1 : ss << info;
213 : 1 : }
214 : :
215 : 2 : TEST_F(TestCApiBlackUncovered, default_constructors)
216 : : {
217 : 1 : (void)cvc5::Op();
218 : 1 : (void)cvc5::Datatype();
219 : 1 : (void)cvc5::DatatypeDecl();
220 : 1 : (void)cvc5::DatatypeConstructorDecl();
221 : 1 : (void)cvc5::DatatypeConstructor();
222 : 1 : (void)cvc5::DatatypeSelector();
223 : 1 : (void)cvc5::SynthResult();
224 : 1 : (void)cvc5::Grammar();
225 : 1 : (void)cvc5::Result();
226 : 1 : (void)cvc5::Proof();
227 : 1 : (void)cvc5::parser::Command();
228 : 1 : }
229 : :
230 : 2 : TEST_F(TestCApiBlackUncovered, comparison_operators)
231 : : {
232 : 1 : cvc5::Sort sort;
233 [ - + ]: 1 : ASSERT_TRUE(sort <= sort);
234 [ - + ]: 1 : ASSERT_TRUE(sort >= sort);
235 : 1 : cvc5::Term term;
236 [ - + ]: 1 : ASSERT_TRUE(term <= term);
237 [ - + ]: 1 : ASSERT_TRUE(term >= term);
238 : : }
239 : :
240 : 2 : TEST_F(TestCApiBlackUncovered, term_creation)
241 : : {
242 : 1 : d_tm.mkTrue().notTerm();
243 : 1 : d_tm.mkTrue().andTerm(d_tm.mkTrue());
244 : 1 : d_tm.mkTrue().orTerm(d_tm.mkTrue());
245 : 1 : d_tm.mkTrue().xorTerm(d_tm.mkTrue());
246 : 1 : d_tm.mkTrue().eqTerm(d_tm.mkTrue());
247 : 1 : d_tm.mkTrue().impTerm(d_tm.mkTrue());
248 : 1 : d_tm.mkTrue().iteTerm(d_tm.mkTrue(), d_tm.mkFalse());
249 : 1 : }
250 : :
251 : 2 : TEST_F(TestCApiBlackUncovered, term_iterators)
252 : : {
253 : 1 : Term t = d_tm.mkInteger(0);
254 [ + + ][ - - ]: 3 : t = d_tm.mkTerm(Kind::GT, {t, t});
255 : 1 : Term::const_iterator it;
256 : 1 : it = t.begin();
257 : 1 : auto it2(it);
258 [ - + ]: 1 : ASSERT_FALSE(it == t.end());
259 [ - + ]: 1 : ASSERT_FALSE(it != it2);
260 : 1 : *it2;
261 : 1 : ++it;
262 : 1 : it++;
263 : : }
264 : :
265 : 2 : TEST_F(TestCApiBlackUncovered, dt_iterators)
266 : : {
267 : : // default constructors
268 : :
269 : 2 : DatatypeDecl decl = d_tm.mkDatatypeDecl("list");
270 : 2 : DatatypeConstructorDecl cons = d_tm.mkDatatypeConstructorDecl("cons");
271 : 1 : cons.addSelector("head", d_int);
272 : 1 : decl.addConstructor(cons);
273 : 1 : Sort list = d_tm.mkDatatypeSort(decl);
274 : 1 : Datatype dt = list.getDatatype();
275 : 2 : DatatypeConstructor dt_cons = dt["cons"];
276 : 2 : DatatypeSelector dt_sel = dt_cons["head"];
277 : :
278 : : {
279 : 1 : Datatype::const_iterator it;
280 : 1 : it = dt.begin();
281 [ - + ]: 1 : ASSERT_TRUE(it != dt.end());
282 : 1 : *it;
283 : 1 : it->getName();
284 : 1 : ++it;
285 [ - + ]: 1 : ASSERT_TRUE(it == dt.end());
286 : 1 : it++;
287 : : }
288 : : {
289 : 1 : DatatypeConstructor::const_iterator it;
290 : 1 : it = dt_cons.begin();
291 [ - + ]: 1 : ASSERT_TRUE(it != dt_cons.end());
292 : 1 : *it;
293 : 1 : it->getName();
294 : 1 : ++it;
295 : 1 : it = dt_cons.begin();
296 : 1 : it++;
297 [ - + ]: 1 : ASSERT_TRUE(it == dt_cons.end());
298 : : }
299 : : }
300 : :
301 : 2 : TEST_F(TestCApiBlackUncovered, stats_iterators)
302 : : {
303 : 1 : Stat stat;
304 : 1 : stat = Stat();
305 : 1 : Statistics stats = d_solver->getStatistics();
306 : 1 : auto it = stats.begin();
307 : 1 : it++;
308 : 1 : it--;
309 : 1 : ++it;
310 : 1 : --it;
311 [ - + ]: 1 : ASSERT_EQ(it, stats.begin());
312 [ - + ]: 1 : ASSERT_FALSE(stats.begin() == stats.end());
313 [ - + ]: 1 : ASSERT_TRUE(stats.begin() != stats.end());
314 : 2 : std::stringstream ss;
315 : 1 : ss << stats;
316 : 1 : ss << it->first;
317 : : }
318 : :
319 : 2 : TEST_F(TestCApiBlackUncovered, check_sat_assuming)
320 : : {
321 : 1 : d_solver->checkSatAssuming(d_tm.mkTrue());
322 : 1 : }
323 : :
324 : 2 : TEST_F(TestCApiBlackUncovered, option_info)
325 : : {
326 : 2 : cvc5::OptionInfo info = d_solver->getOptionInfo("print-success");
327 : 1 : (void)info.boolValue();
328 : 1 : info = d_solver->getOptionInfo("verbosity");
329 : 1 : (void)info.intValue();
330 : 1 : info = d_solver->getOptionInfo("rlimit");
331 : 1 : (void)info.uintValue();
332 : 1 : info = d_solver->getOptionInfo("random-freq");
333 : 1 : (void)info.doubleValue();
334 : 1 : info = d_solver->getOptionInfo("force-logic");
335 : 1 : (void)info.stringValue();
336 : 1 : }
337 : :
338 : : class PluginListen : public Plugin
339 : : {
340 : : public:
341 : 1 : PluginListen(TermManager& tm)
342 : 1 : : Plugin(tm), d_hasSeenTheoryLemma(false), d_hasSeenSatClause(false)
343 : : {
344 : 1 : }
345 : 1 : virtual ~PluginListen() {}
346 : 3 : void notifySatClause(const Term& cl) override
347 : : {
348 : 3 : Plugin::notifySatClause(cl); // Cover default implementation
349 : 3 : d_hasSeenSatClause = true;
350 : 3 : }
351 : 1 : bool hasSeenSatClause() const { return d_hasSeenSatClause; }
352 : 4 : void notifyTheoryLemma(const Term& lem) override
353 : : {
354 : 4 : Plugin::notifyTheoryLemma(lem); // Cover default implementation
355 : 4 : d_hasSeenTheoryLemma = true;
356 : 4 : }
357 : 1 : bool hasSeenTheoryLemma() const { return d_hasSeenTheoryLemma; }
358 : 1 : std::string getName() override { return "PluginListen"; }
359 : :
360 : : private:
361 : : /** have we seen a theory lemma? */
362 : : bool d_hasSeenTheoryLemma;
363 : : /** have we seen a SAT clause? */
364 : : bool d_hasSeenSatClause;
365 : : };
366 : :
367 : 2 : TEST_F(TestCApiBlackUncovered, plugin_uncovered_default)
368 : : {
369 : : // NOTE: this shouldn't be necessary but ensures notifySatClause is called
370 : : // here.
371 : 1 : d_solver->setOption("plugin-notify-sat-clause-in-solve", "false");
372 : 1 : PluginListen pl(d_tm);
373 : 1 : d_solver->addPlugin(pl);
374 : 1 : Sort stringSort = d_tm.getStringSort();
375 : 1 : Term x = d_tm.mkConst(stringSort, "x");
376 : 1 : Term y = d_tm.mkConst(stringSort, "y");
377 : 4 : Term ctn1 = d_tm.mkTerm(Kind::STRING_CONTAINS, {x, y});
378 : 4 : Term ctn2 = d_tm.mkTerm(Kind::STRING_CONTAINS, {y, x});
379 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::OR, {ctn1, ctn2}));
380 : 3 : Term lx = d_tm.mkTerm(Kind::STRING_LENGTH, {x});
381 : 3 : Term ly = d_tm.mkTerm(Kind::STRING_LENGTH, {y});
382 : 4 : Term lc = d_tm.mkTerm(Kind::GT, {lx, ly});
383 : 1 : d_solver->assertFormula(lc);
384 [ - + ]: 1 : ASSERT_TRUE(d_solver->checkSat().isSat());
385 : : // above input formulas should induce a theory lemma and SAT clause learning
386 [ - + ]: 1 : ASSERT_TRUE(pl.hasSeenTheoryLemma());
387 [ - + ]: 1 : ASSERT_TRUE(pl.hasSeenSatClause());
388 : : }
389 : :
390 : 2 : TEST_F(TestCApiBlackUncovered, parser)
391 : : {
392 : 1 : parser::Command command;
393 : 1 : Solver solver(d_tm);
394 : 1 : parser::InputParser parser(&solver);
395 : 1 : (void)parser.getSolver();
396 : 1 : std::stringstream ss;
397 : 1 : ss << command << std::endl;
398 : 1 : parser.setStreamInput(modes::InputLanguage::SMT_LIB_2_6, ss, "Parser");
399 : 1 : parser::ParserException defaultConstructor;
400 : 1 : std::string message = "error";
401 : 1 : const char* cMessage = "error";
402 : 1 : std::string filename = "file.smt2";
403 : 1 : parser::ParserException stringConstructor(message);
404 : 1 : parser::ParserException cStringConstructor(cMessage);
405 : 1 : parser::ParserException exception(message, filename, 10, 11);
406 : 1 : exception.toStream(ss);
407 [ - + ]: 1 : ASSERT_EQ(message, exception.getMessage());
408 [ - + ]: 1 : ASSERT_EQ(message, exception.getMessage());
409 [ - + ]: 2 : ASSERT_EQ(filename, exception.getFilename());
410 [ - + ]: 1 : ASSERT_EQ(10, exception.getLine());
411 [ - + ]: 1 : ASSERT_EQ(11, exception.getColumn());
412 : :
413 : 2 : parser::ParserEndOfFileException eofDefault;
414 : 2 : parser::ParserEndOfFileException eofString(message);
415 : 2 : parser::ParserEndOfFileException eofCMessage(cMessage);
416 : 1 : parser::ParserEndOfFileException eof(message, filename, 10, 11);
417 : : }
418 : :
419 : 2 : TEST_F(TestCApiBlackUncovered, driver_options)
420 : : {
421 : 1 : auto dopts = d_solver->getDriverOptions();
422 : 1 : dopts.err();
423 : 1 : dopts.in();
424 : 1 : dopts.out();
425 : 1 : }
426 : :
427 : : } // namespace cvc5::internal::test
|
