Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Aina Niemetz, Mudathir Mohamed, Gereon Kremer
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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).getStringValue();
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 : ss << cvc5::RoundingMode::ROUND_TOWARD_NEGATIVE;
164 : 1 : ss << cvc5::UnknownExplanation::UNKNOWN_REASON;
165 : 1 : ss << cvc5::modes::BlockModelsMode::LITERALS;
166 : 1 : ss << cvc5::modes::LearnedLitType::PREPROCESS;
167 : 1 : ss << cvc5::modes::ProofComponent::FULL;
168 : 1 : ss << cvc5::modes::FindSynthTarget::ENUM;
169 : 1 : ss << cvc5::modes::OptionCategory::EXPERT;
170 : 1 : ss << cvc5::modes::InputLanguage::SMT_LIB_2_6;
171 : 1 : ss << cvc5::modes::ProofFormat::LFSC;
172 : 1 : ss << cvc5::ProofRule::ASSUME << std::to_string(cvc5::ProofRule::ASSUME);
173 : 1 : ss << cvc5::ProofRewriteRule::NONE;
174 : 1 : ss << cvc5::SkolemId::PURIFY;
175 : 1 : ss << d_tm.mkOp(Kind::BITVECTOR_EXTRACT, {4, 0});
176 : 1 : ss << d_tm.mkDatatypeConstructorDecl("cons");
177 : :
178 : 2 : Sort intsort = d_tm.getIntegerSort();
179 : 2 : Term x = d_tm.mkConst(intsort, "x");
180 : :
181 [ + + ][ - - ]: 3 : ss << std::vector<Term>{x, x};
182 [ + + ][ - - ]: 3 : ss << std::set<Term>{x, x};
183 [ + + ][ - - ]: 3 : ss << std::unordered_set<Term>{x, x};
184 : :
185 : 1 : d_solver->setOption("sygus", "true");
186 : 1 : (void)d_solver->synthFun("f", {}, d_bool);
187 : 1 : ss << d_solver->checkSynth();
188 : 2 : ss << d_solver->mkGrammar({}, {d_tm.mkVar(d_bool)});
189 : 1 : ss << d_solver->checkSat();
190 : :
191 : 3 : DatatypeDecl decl = d_tm.mkDatatypeDecl("list");
192 : 3 : DatatypeConstructorDecl cons = d_tm.mkDatatypeConstructorDecl("cons");
193 : 1 : cons.addSelector("head", d_int);
194 : 1 : decl.addConstructor(cons);
195 : 2 : Datatype dt = d_tm.mkDatatypeSort(decl).getDatatype();
196 : 1 : ss << dt;
197 : 2 : DatatypeConstructor ctor = dt[0];
198 : 1 : ss << ctor;
199 : 3 : DatatypeSelector head = ctor.getSelector("head");
200 : 1 : ss << head;
201 : :
202 : 3 : OptionInfo info = d_solver->getOptionInfo("verbose");
203 : 1 : ss << info;
204 : 1 : }
205 : :
206 : 2 : TEST_F(TestCApiBlackUncovered, default_constructors)
207 : : {
208 : 1 : (void)cvc5::Op();
209 : 1 : (void)cvc5::Datatype();
210 : 1 : (void)cvc5::DatatypeDecl();
211 : 1 : (void)cvc5::DatatypeConstructorDecl();
212 : 1 : (void)cvc5::DatatypeConstructor();
213 : 1 : (void)cvc5::DatatypeSelector();
214 : 1 : (void)cvc5::SynthResult();
215 : 1 : (void)cvc5::Grammar();
216 : 1 : (void)cvc5::Result();
217 : 1 : (void)cvc5::Proof();
218 : 1 : (void)cvc5::parser::Command();
219 : 1 : }
220 : :
221 : 2 : TEST_F(TestCApiBlackUncovered, comparison_operators)
222 : : {
223 : 1 : cvc5::Sort sort;
224 [ - + ]: 1 : ASSERT_TRUE(sort <= sort);
225 [ - + ]: 1 : ASSERT_TRUE(sort >= sort);
226 : 1 : cvc5::Term term;
227 [ - + ]: 1 : ASSERT_TRUE(term <= term);
228 [ - + ]: 1 : ASSERT_TRUE(term >= term);
229 : : }
230 : :
231 : 2 : TEST_F(TestCApiBlackUncovered, term_creation)
232 : : {
233 : 1 : d_tm.mkTrue().notTerm();
234 : 1 : d_tm.mkTrue().andTerm(d_tm.mkTrue());
235 : 1 : d_tm.mkTrue().orTerm(d_tm.mkTrue());
236 : 1 : d_tm.mkTrue().xorTerm(d_tm.mkTrue());
237 : 1 : d_tm.mkTrue().eqTerm(d_tm.mkTrue());
238 : 1 : d_tm.mkTrue().impTerm(d_tm.mkTrue());
239 : 1 : d_tm.mkTrue().iteTerm(d_tm.mkTrue(), d_tm.mkFalse());
240 : 1 : }
241 : :
242 : 2 : TEST_F(TestCApiBlackUncovered, term_iterators)
243 : : {
244 : 1 : Term t = d_tm.mkInteger(0);
245 [ + + ][ - - ]: 3 : t = d_tm.mkTerm(Kind::GT, {t, t});
246 : 1 : Term::const_iterator it;
247 : 1 : it = t.begin();
248 : 1 : auto it2(it);
249 [ - + ]: 1 : ASSERT_FALSE(it == t.end());
250 [ - + ]: 1 : ASSERT_FALSE(it != it2);
251 : 1 : *it2;
252 : 1 : ++it;
253 : 1 : it++;
254 : : }
255 : :
256 : 2 : TEST_F(TestCApiBlackUncovered, dt_iterators)
257 : : {
258 : : // default constructors
259 : :
260 : 2 : DatatypeDecl decl = d_tm.mkDatatypeDecl("list");
261 : 2 : DatatypeConstructorDecl cons = d_tm.mkDatatypeConstructorDecl("cons");
262 : 1 : cons.addSelector("head", d_int);
263 : 1 : decl.addConstructor(cons);
264 : 1 : Sort list = d_tm.mkDatatypeSort(decl);
265 : 1 : Datatype dt = list.getDatatype();
266 : 2 : DatatypeConstructor dt_cons = dt["cons"];
267 : 2 : DatatypeSelector dt_sel = dt_cons["head"];
268 : :
269 : : {
270 : 1 : Datatype::const_iterator it;
271 : 1 : it = dt.begin();
272 [ - + ]: 1 : ASSERT_TRUE(it != dt.end());
273 : 1 : *it;
274 : 1 : it->getName();
275 : 1 : ++it;
276 [ - + ]: 1 : ASSERT_TRUE(it == dt.end());
277 : 1 : it++;
278 : : }
279 : : {
280 : 1 : DatatypeConstructor::const_iterator it;
281 : 1 : it = dt_cons.begin();
282 [ - + ]: 1 : ASSERT_TRUE(it != dt_cons.end());
283 : 1 : *it;
284 : 1 : it->getName();
285 : 1 : ++it;
286 : 1 : it = dt_cons.begin();
287 : 1 : it++;
288 [ - + ]: 1 : ASSERT_TRUE(it == dt_cons.end());
289 : : }
290 : : }
291 : :
292 : 2 : TEST_F(TestCApiBlackUncovered, stats_iterators)
293 : : {
294 : 1 : Stat stat;
295 : 1 : stat = Stat();
296 : 1 : Statistics stats = d_solver->getStatistics();
297 : 1 : auto it = stats.begin();
298 : 1 : it++;
299 : 1 : it--;
300 : 1 : ++it;
301 : 1 : --it;
302 [ - + ]: 1 : ASSERT_EQ(it, stats.begin());
303 [ - + ]: 1 : ASSERT_FALSE(stats.begin() == stats.end());
304 [ - + ]: 1 : ASSERT_TRUE(stats.begin() != stats.end());
305 : 2 : std::stringstream ss;
306 : 1 : ss << stats;
307 : 1 : ss << it->first;
308 : : }
309 : :
310 : 2 : TEST_F(TestCApiBlackUncovered, check_sat_assuming)
311 : : {
312 : 1 : d_solver->checkSatAssuming(d_tm.mkTrue());
313 : 1 : }
314 : :
315 : 2 : TEST_F(TestCApiBlackUncovered, option_info)
316 : : {
317 : 2 : cvc5::OptionInfo info = d_solver->getOptionInfo("print-success");
318 : 1 : (void)info.boolValue();
319 : 1 : info = d_solver->getOptionInfo("verbosity");
320 : 1 : (void)info.intValue();
321 : 1 : info = d_solver->getOptionInfo("rlimit");
322 : 1 : (void)info.uintValue();
323 : 1 : info = d_solver->getOptionInfo("random-freq");
324 : 1 : (void)info.doubleValue();
325 : 1 : info = d_solver->getOptionInfo("force-logic");
326 : 1 : (void)info.stringValue();
327 : 1 : }
328 : :
329 : : class PluginListen : public Plugin
330 : : {
331 : : public:
332 : 1 : PluginListen(TermManager& tm)
333 : 1 : : Plugin(tm), d_hasSeenTheoryLemma(false), d_hasSeenSatClause(false)
334 : : {
335 : 1 : }
336 : 1 : virtual ~PluginListen() {}
337 : 3 : void notifySatClause(const Term& cl) override
338 : : {
339 : 3 : Plugin::notifySatClause(cl); // Cover default implementation
340 : 3 : d_hasSeenSatClause = true;
341 : 3 : }
342 : 1 : bool hasSeenSatClause() const { return d_hasSeenSatClause; }
343 : 4 : void notifyTheoryLemma(const Term& lem) override
344 : : {
345 : 4 : Plugin::notifyTheoryLemma(lem); // Cover default implementation
346 : 4 : d_hasSeenTheoryLemma = true;
347 : 4 : }
348 : 1 : bool hasSeenTheoryLemma() const { return d_hasSeenTheoryLemma; }
349 : 1 : std::string getName() override { return "PluginListen"; }
350 : :
351 : : private:
352 : : /** have we seen a theory lemma? */
353 : : bool d_hasSeenTheoryLemma;
354 : : /** have we seen a SAT clause? */
355 : : bool d_hasSeenSatClause;
356 : : };
357 : :
358 : 2 : TEST_F(TestCApiBlackUncovered, plugin_uncovered_default)
359 : : {
360 : : // NOTE: this shouldn't be necessary but ensures notifySatClause is called
361 : : // here.
362 : 1 : d_solver->setOption("plugin-notify-sat-clause-in-solve", "false");
363 : 1 : PluginListen pl(d_tm);
364 : 1 : d_solver->addPlugin(pl);
365 : 1 : Sort stringSort = d_tm.getStringSort();
366 : 1 : Term x = d_tm.mkConst(stringSort, "x");
367 : 1 : Term y = d_tm.mkConst(stringSort, "y");
368 : 4 : Term ctn1 = d_tm.mkTerm(Kind::STRING_CONTAINS, {x, y});
369 : 4 : Term ctn2 = d_tm.mkTerm(Kind::STRING_CONTAINS, {y, x});
370 [ + + ][ - - ]: 3 : d_solver->assertFormula(d_tm.mkTerm(Kind::OR, {ctn1, ctn2}));
371 : 3 : Term lx = d_tm.mkTerm(Kind::STRING_LENGTH, {x});
372 : 3 : Term ly = d_tm.mkTerm(Kind::STRING_LENGTH, {y});
373 : 4 : Term lc = d_tm.mkTerm(Kind::GT, {lx, ly});
374 : 1 : d_solver->assertFormula(lc);
375 [ - + ]: 1 : ASSERT_TRUE(d_solver->checkSat().isSat());
376 : : // above input formulas should induce a theory lemma and SAT clause learning
377 [ - + ]: 1 : ASSERT_TRUE(pl.hasSeenTheoryLemma());
378 [ - + ]: 1 : ASSERT_TRUE(pl.hasSeenSatClause());
379 : : }
380 : :
381 : 2 : TEST_F(TestCApiBlackUncovered, parser)
382 : : {
383 : 1 : parser::Command command;
384 : 1 : Solver solver(d_tm);
385 : 1 : parser::InputParser parser(&solver);
386 : 1 : (void)parser.getSolver();
387 : 1 : std::stringstream ss;
388 : 1 : ss << command << std::endl;
389 : 1 : parser.setStreamInput(modes::InputLanguage::SMT_LIB_2_6, ss, "Parser");
390 : 1 : parser::ParserException defaultConstructor;
391 : 1 : std::string message = "error";
392 : 1 : const char* cMessage = "error";
393 : 1 : std::string filename = "file.smt2";
394 : 1 : parser::ParserException stringConstructor(message);
395 : 1 : parser::ParserException cStringConstructor(cMessage);
396 : 1 : parser::ParserException exception(message, filename, 10, 11);
397 : 1 : exception.toStream(ss);
398 [ - + ]: 1 : ASSERT_EQ(message, exception.getMessage());
399 [ - + ]: 1 : ASSERT_EQ(message, exception.getMessage());
400 [ - + ]: 2 : ASSERT_EQ(filename, exception.getFilename());
401 [ - + ]: 1 : ASSERT_EQ(10, exception.getLine());
402 [ - + ]: 1 : ASSERT_EQ(11, exception.getColumn());
403 : :
404 : 2 : parser::ParserEndOfFileException eofDefault;
405 : 2 : parser::ParserEndOfFileException eofString(message);
406 : 2 : parser::ParserEndOfFileException eofCMessage(cMessage);
407 : 1 : parser::ParserEndOfFileException eof(message, filename, 10, 11);
408 : : }
409 : :
410 : 2 : TEST_F(TestCApiBlackUncovered, driver_options)
411 : : {
412 : 1 : auto dopts = d_solver->getDriverOptions();
413 : 1 : dopts.err();
414 : 1 : dopts.in();
415 : 1 : dopts.out();
416 : 1 : }
417 : :
418 : : } // namespace cvc5::internal::test
|
