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