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 : : * The cvc5 C Parser API.
11 : : */
12 : :
13 : : extern "C" {
14 : : #include <cvc5/c/cvc5_parser.h>
15 : : }
16 : :
17 : : #include <cvc5/cvc5.h>
18 : : #include <cvc5/cvc5_parser.h>
19 : :
20 : : #include <fstream>
21 : : #include <memory>
22 : :
23 : : #include "api/c/cvc5_c_structs.h"
24 : : #include "api/c/cvc5_checks.h"
25 : :
26 : : /* -------------------------------------------------------------------------- */
27 : :
28 : : /** Wrapper for cvc5 C++ command. */
29 : : struct cvc5_cmd_t
30 : : {
31 : : /**
32 : : * Constructor.
33 : : * @param parser The associated parser instance.
34 : : * @param cmd The wrapped C++ command.
35 : : */
36 : 135 : cvc5_cmd_t(Cvc5InputParser* parser, const cvc5::parser::Command& cmd)
37 : 135 : : d_cmd(cmd), d_parser(parser)
38 : : {
39 : 135 : }
40 : : /** The associated command instance. */
41 : : cvc5::parser::Command d_cmd;
42 : : /** External refs count. */
43 : : uint32_t d_refs = 1;
44 : : /** The associated parser instance. */
45 : : Cvc5InputParser* d_parser = nullptr;
46 : : };
47 : :
48 : : /** Wrapper for cvc5 C++ symbol manager. */
49 : : struct Cvc5SymbolManager
50 : : {
51 : : /**
52 : : * Constructor.
53 : : * @param tm The associated term manager.
54 : : */
55 : 48 : Cvc5SymbolManager(Cvc5TermManager* tm)
56 : 48 : : d_sm_wrapped(new cvc5::parser::SymbolManager(tm->d_tm)),
57 : 48 : d_sm(*d_sm_wrapped),
58 : 48 : d_tm(tm)
59 : : {
60 : : // The symbol manager keeps the term manager alive (e.g., to export
61 : : // declared terms and sorts).
62 : 48 : d_tm->inc_ref();
63 : 48 : }
64 : : /**
65 : : * Constructor.
66 : : * @param sm The wrapped symbol manager instance.
67 : : * @param tm The associated term manager.
68 : : */
69 : 12 : Cvc5SymbolManager(cvc5::parser::SymbolManager& sm, Cvc5TermManager* tm)
70 : 12 : : d_sm(sm), d_tm(tm)
71 : : {
72 : 12 : d_tm->inc_ref();
73 : 12 : }
74 : : /** Destructor. */
75 : 60 : ~Cvc5SymbolManager() { d_tm->dec_ref(); }
76 : : /**
77 : : * The created symbol manager instance.
78 : : *
79 : : * This will be a newly created symbol manager when created via
80 : : * cvc5_symbol_manager_new(). However, if we create a parsere via
81 : : * cvc5_parser_new() while passing NULL as a symbol manager, this will be
82 : : * NULL and `d_sm` will point to the symbol manager created by the parser.
83 : : */
84 : : std::unique_ptr<cvc5::parser::SymbolManager> d_sm_wrapped;
85 : : /** The associated symbol manager instance. */
86 : : cvc5::parser::SymbolManager& d_sm;
87 : : /** The associated term manager. */
88 : : Cvc5TermManager* d_tm = nullptr;
89 : : };
90 : :
91 : : /** Wrapper for cvc5 C++ parser. */
92 : : struct Cvc5InputParser
93 : : {
94 : : /**
95 : : * Constructor.
96 : : * @param cvc5 The associated solver instance.
97 : : */
98 : 12 : Cvc5InputParser(Cvc5* cvc5) : d_parser(&cvc5->d_solver), d_cvc5(cvc5)
99 : : {
100 : 24 : d_sm_wrapped.reset(new Cvc5SymbolManager(*d_parser.getSymbolManager(),
101 : 12 : cvc5_get_tm(d_cvc5)));
102 : 12 : d_sm = d_sm_wrapped.get();
103 : 12 : }
104 : : /**
105 : : * Constructor.
106 : : * @param cvc5 The associated solver instance.
107 : : * @param sm The associated symbol manager.
108 : : */
109 : 41 : Cvc5InputParser(Cvc5* cvc5, Cvc5SymbolManager* sm)
110 : 41 : : d_parser(&cvc5->d_solver, &sm->d_sm), d_cvc5(cvc5), d_sm(sm)
111 : : {
112 : 41 : }
113 : :
114 : : /**
115 : : * Export C++ command to C API.
116 : : * @param cmd The command to export.
117 : : */
118 : : Cvc5Command export_cmd(const cvc5::parser::Command& cmd);
119 : :
120 : : /**
121 : : * Decrement the external ref count of a command. If the ref count reaches
122 : : * zero, the command is released (freed).
123 : : * @param cmd The command to release.
124 : : */
125 : : void release(cvc5_cmd_t* cmd);
126 : : /**
127 : : * Increment the external ref count of a command.
128 : : * @param cmd The command to copy.
129 : : * @return The copied command.
130 : : */
131 : : cvc5_cmd_t* copy(cvc5_cmd_t* cmd);
132 : : /** Release all managed command objects. */
133 : : void release();
134 : :
135 : : /**
136 : : * Increment the number of external handles to this parser.
137 : : *
138 : : * A handle is held by the user (returned by `cvc5_parser_new()` and dropped
139 : : * via `cvc5_parser_delete()`) and by each command allocated by this parser.
140 : : */
141 : : void inc_ref();
142 : : /**
143 : : * Decrement the number of external handles to this parser.
144 : : *
145 : : * The parser is freed once it has no external handles and no managed
146 : : * command objects left. Commands thus keep their parser alive until they
147 : : * are released, and remain valid after `cvc5_parser_delete()`.
148 : : */
149 : : void dec_ref();
150 : :
151 : : /** The associated input parser instance. */
152 : : cvc5::parser::InputParser d_parser;
153 : : /** The associated solver instance. */
154 : : Cvc5* d_cvc5 = nullptr;
155 : : /** The associated symbol manager instance. */
156 : : Cvc5SymbolManager* d_sm = nullptr;
157 : : /**
158 : : * Maintain Cvc5SymbolManager wrapper instance if symbol manager was not
159 : : * given via constructor but created by the parser.
160 : : */
161 : : std::unique_ptr<Cvc5SymbolManager> d_sm_wrapped;
162 : :
163 : : private:
164 : : /** Free this parser if it has no external handles and no commands. */
165 : : void free_if_unused();
166 : :
167 : : /** The number of external handles to this parser. */
168 : : uint32_t d_refs = 1;
169 : : /**
170 : : * The allocated command objects.
171 : : * @note Commands are never exported more than once, we thus key this cache
172 : : * on the allocated wrapper object.
173 : : */
174 : : std::unordered_map<cvc5_cmd_t*, std::unique_ptr<cvc5_cmd_t>> d_alloc_cmds;
175 : : };
176 : :
177 : : /* -------------------------------------------------------------------------- */
178 : :
179 : 135 : Cvc5Command Cvc5InputParser::export_cmd(const cvc5::parser::Command& cmd)
180 : : {
181 [ - + ][ - + ]: 135 : Assert(!cmd.isNull());
[ - - ]
182 : 135 : auto c = std::make_unique<cvc5_cmd_t>(this, cmd);
183 : 135 : cvc5_cmd_t* res = c.get();
184 : 135 : d_alloc_cmds.emplace(res, std::move(c));
185 : : // the command keeps this parser alive
186 : 135 : inc_ref();
187 : 135 : return res;
188 : 135 : }
189 : :
190 : 4 : void Cvc5InputParser::release(cvc5_cmd_t* cmd)
191 : : {
192 [ + - ]: 4 : if (cmd)
193 : : {
194 : 4 : cmd->d_refs -= 1;
195 [ + + ]: 4 : if (cmd->d_refs == 0)
196 : : {
197 [ - + ][ - + ]: 3 : Assert(d_alloc_cmds.find(cmd) != d_alloc_cmds.end());
[ - - ]
198 : 3 : d_alloc_cmds.erase(cmd);
199 : 3 : dec_ref();
200 : : }
201 : : }
202 : 4 : }
203 : :
204 : 1 : cvc5_cmd_t* Cvc5InputParser::copy(cvc5_cmd_t* cmd)
205 : : {
206 [ + - ]: 1 : if (cmd)
207 : : {
208 : 1 : cmd->d_refs += 1;
209 : : }
210 : 1 : return cmd;
211 : : }
212 : :
213 : 51 : void Cvc5InputParser::release()
214 : : {
215 : 51 : size_t ncmds = d_alloc_cmds.size();
216 : 51 : d_alloc_cmds.clear();
217 : : // drop the handles held by the released commands
218 [ - + ][ - + ]: 51 : Assert(d_refs >= ncmds);
[ - - ]
219 : 51 : d_refs -= ncmds;
220 : 51 : free_if_unused();
221 : 51 : }
222 : :
223 : 135 : void Cvc5InputParser::inc_ref() { d_refs += 1; }
224 : :
225 : 56 : void Cvc5InputParser::dec_ref()
226 : : {
227 [ - + ][ - + ]: 56 : Assert(d_refs > 0);
[ - - ]
228 : 56 : d_refs -= 1;
229 : 56 : free_if_unused();
230 : 56 : }
231 : :
232 : 107 : void Cvc5InputParser::free_if_unused()
233 : : {
234 [ + + ]: 107 : if (d_refs == 0)
235 : : {
236 [ - + ][ - + ]: 53 : Assert(d_alloc_cmds.empty());
[ - - ]
237 [ + - ]: 53 : delete this;
238 : : }
239 : 107 : }
240 : :
241 : : /* -------------------------------------------------------------------------- */
242 : :
243 : 48 : Cvc5SymbolManager* cvc5_symbol_manager_new(Cvc5TermManager* tm)
244 : : {
245 : 48 : Cvc5SymbolManager* res = nullptr;
246 : 48 : CVC5_CAPI_TRY_CATCH_BEGIN;
247 [ - + ][ - + ]: 48 : CVC5_CAPI_CHECK_NOT_NULL(tm);
[ - - ]
248 : 48 : res = new Cvc5SymbolManager(tm);
249 [ - - ][ - - ]: 0 : CVC5_CAPI_TRY_CATCH_END;
[ - - ][ - - ]
[ - - ][ - - ]
[ - ]
250 : 48 : return res;
251 : : }
252 : :
253 : 48 : void cvc5_symbol_manager_delete(Cvc5SymbolManager* sm)
254 : : {
255 : 48 : CVC5_CAPI_TRY_CATCH_BEGIN;
256 [ - + ][ - + ]: 48 : CVC5_CAPI_CHECK_NOT_NULL(sm);
[ - - ]
257 [ + - ]: 48 : delete sm;
258 [ - - ][ - - ]: 0 : CVC5_CAPI_TRY_CATCH_END;
[ - - ][ - - ]
[ - - ][ - - ]
[ - ]
259 : 48 : }
260 : :
261 : 5 : bool cvc5_sm_is_logic_set(Cvc5SymbolManager* sm)
262 : : {
263 : 5 : bool res = false;
264 : 5 : CVC5_CAPI_TRY_CATCH_BEGIN;
265 [ + + ][ + + ]: 5 : CVC5_CAPI_CHECK_NOT_NULL(sm);
[ - - ]
266 : 4 : res = sm->d_sm.isLogicSet();
267 [ + - ][ - + ]: 1 : CVC5_CAPI_TRY_CATCH_END;
[ - - ][ - - ]
[ - - ][ - - ]
[ - ]
268 : 5 : return res;
269 : : }
270 : :
271 : 4 : const char* cvc5_sm_get_logic(Cvc5SymbolManager* sm)
272 : : {
273 [ + + ]: 4 : static thread_local std::string str;
274 : 4 : CVC5_CAPI_TRY_CATCH_BEGIN;
275 [ + + ][ + + ]: 4 : CVC5_CAPI_CHECK_NOT_NULL(sm);
[ - - ]
276 : 3 : str = sm->d_sm.getLogic();
277 [ + - ][ - + ]: 2 : CVC5_CAPI_TRY_CATCH_END;
[ - - ][ - - ]
[ - - ][ - - ]
[ - ]
278 : 4 : return str.c_str();
279 : : }
280 : :
281 : 6 : const Cvc5Sort* cvc5_sm_get_declared_sorts(Cvc5SymbolManager* sm, size_t* size)
282 : : {
283 [ + + ]: 6 : static thread_local std::vector<Cvc5Sort> res;
284 : 6 : CVC5_CAPI_TRY_CATCH_BEGIN;
285 [ + + ][ + + ]: 6 : CVC5_CAPI_CHECK_NOT_NULL(sm);
[ - - ]
286 [ + + ][ + + ]: 5 : CVC5_CAPI_CHECK_NOT_NULL(size);
[ - - ]
287 : 4 : res.clear();
288 : 4 : auto sorts = sm->d_sm.getDeclaredSorts();
289 : 4 : auto tm = sm->d_tm;
290 [ + + ]: 6 : for (auto& s : sorts)
291 : : {
292 : 2 : res.push_back(tm->export_sort(s));
293 : : }
294 : 4 : *size = res.size();
295 [ + - ][ - + ]: 6 : CVC5_CAPI_TRY_CATCH_END;
[ - - ][ - - ]
[ - - ][ - - ]
[ - ]
296 : : // On error, `size` may be invalid (e.g. NULL) and `res` may hold stale data,
297 : : // so we must not dereference `size` here; gate on the error state instead.
298 [ + + ][ + + ]: 6 : return cvc5::cvc5_capi_has_error() || res.empty() ? nullptr : res.data();
299 : : }
300 : :
301 : 6 : const Cvc5Term* cvc5_sm_get_declared_terms(Cvc5SymbolManager* sm, size_t* size)
302 : : {
303 [ + + ]: 6 : static thread_local std::vector<Cvc5Term> res;
304 : 6 : CVC5_CAPI_TRY_CATCH_BEGIN;
305 [ + + ][ + + ]: 6 : CVC5_CAPI_CHECK_NOT_NULL(sm);
[ - - ]
306 [ + + ][ + + ]: 5 : CVC5_CAPI_CHECK_NOT_NULL(size);
[ - - ]
307 : 4 : res.clear();
308 : 4 : auto terms = sm->d_sm.getDeclaredTerms();
309 : 4 : auto tm = sm->d_tm;
310 [ + + ]: 7 : for (auto& t : terms)
311 : : {
312 : 3 : res.push_back(tm->export_term(t));
313 : : }
314 : 4 : *size = res.size();
315 [ + - ][ - + ]: 6 : CVC5_CAPI_TRY_CATCH_END;
[ - - ][ - - ]
[ - - ][ - - ]
[ - ]
316 : : // On error, `size` may be invalid (e.g. NULL) and `res` may hold stale data,
317 : : // so we must not dereference `size` here; gate on the error state instead.
318 [ + + ][ + + ]: 6 : return cvc5::cvc5_capi_has_error() || res.empty() ? nullptr : res.data();
319 : : }
320 : :
321 : 2 : void cvc5_sm_get_named_terms(Cvc5SymbolManager* sm,
322 : : size_t* size,
323 : : Cvc5Term* terms[],
324 : : const char** names[])
325 : : {
326 [ + + ]: 2 : static thread_local std::vector<Cvc5Term> rterms;
327 [ + + ]: 2 : static thread_local std::vector<const char*> rnames;
328 : 2 : CVC5_CAPI_TRY_CATCH_BEGIN;
329 [ - + ][ - + ]: 2 : CVC5_CAPI_CHECK_NOT_NULL(sm);
[ - - ]
330 [ - + ][ - + ]: 2 : CVC5_CAPI_CHECK_NOT_NULL(size);
[ - - ]
331 [ - + ][ - + ]: 2 : CVC5_CAPI_CHECK_NOT_NULL(terms);
[ - - ]
332 [ - + ][ - + ]: 2 : CVC5_CAPI_CHECK_NOT_NULL(names);
[ - - ]
333 : 2 : rterms.clear();
334 : 2 : rnames.clear();
335 : 2 : auto res = sm->d_sm.getNamedTerms();
336 : 2 : auto tm = sm->d_tm;
337 [ + + ]: 3 : for (auto& t : res)
338 : : {
339 : 1 : rterms.push_back(tm->export_term(t.first));
340 : 1 : rnames.push_back(t.second.c_str());
341 : : }
342 : 2 : *size = rterms.size();
343 : 2 : *terms = rterms.data();
344 : 2 : *names = rnames.data();
345 [ - - ][ - - ]: 2 : CVC5_CAPI_TRY_CATCH_END;
[ - - ][ - - ]
[ - - ][ - - ]
[ - ]
346 : 2 : }
347 : :
348 : : /* -------------------------------------------------------------------------- */
349 : :
350 : 134 : const char* cvc5_cmd_invoke(Cvc5Command cmd, Cvc5* cvc5, Cvc5SymbolManager* sm)
351 : : {
352 [ + + ]: 134 : static thread_local std::string str;
353 : 134 : CVC5_CAPI_TRY_CATCH_BEGIN;
354 [ + + ][ + + ]: 134 : CVC5_CAPI_CHECK_CMD(cmd);
[ - - ]
355 [ + + ][ + + ]: 133 : CVC5_CAPI_CHECK_NOT_NULL(cvc5);
[ - - ]
356 [ + + ][ + + ]: 132 : CVC5_CAPI_CHECK_NOT_NULL(sm);
[ - - ]
357 : 131 : std::stringstream ss;
358 : 131 : cmd->d_cmd.invoke(&cvc5->d_solver, &sm->d_sm, ss);
359 : 131 : str = ss.str();
360 [ + - ][ - + ]: 134 : CVC5_CAPI_TRY_CATCH_END;
[ - - ][ - - ]
[ - - ][ - - ]
[ - ]
361 : 134 : return str.c_str();
362 : : }
363 : :
364 : 1 : Cvc5Command cvc5_cmd_copy(Cvc5Command cmd)
365 : : {
366 : 1 : Cvc5Command res = nullptr;
367 : 1 : CVC5_CAPI_TRY_CATCH_BEGIN;
368 [ - + ][ - + ]: 1 : CVC5_CAPI_CHECK_CMD(cmd);
[ - - ]
369 : 1 : res = cmd->d_parser->copy(cmd);
370 [ - - ][ - - ]: 0 : CVC5_CAPI_TRY_CATCH_END;
[ - - ][ - - ]
[ - - ][ - - ]
[ - ]
371 : 1 : return res;
372 : : }
373 : :
374 : 4 : void cvc5_cmd_release(Cvc5Command cmd)
375 : : {
376 : 4 : CVC5_CAPI_TRY_CATCH_BEGIN;
377 [ - + ][ - + ]: 4 : CVC5_CAPI_CHECK_CMD(cmd);
[ - - ]
378 : 4 : cmd->d_parser->release(cmd);
379 [ - - ][ - - ]: 0 : CVC5_CAPI_TRY_CATCH_END;
[ - - ][ - - ]
[ - - ][ - - ]
[ - ]
380 : 4 : }
381 : :
382 : 3 : const char* cvc5_cmd_to_string(const Cvc5Command cmd)
383 : : {
384 [ + + ]: 3 : static thread_local std::string str;
385 : 3 : CVC5_CAPI_TRY_CATCH_BEGIN;
386 [ + + ][ + + ]: 3 : CVC5_CAPI_CHECK_CMD(cmd);
[ - - ]
387 : 2 : str = cmd->d_cmd.toString();
388 [ + - ][ - + ]: 1 : CVC5_CAPI_TRY_CATCH_END;
[ - - ][ - - ]
[ - - ][ - - ]
[ - ]
389 : 3 : return str.c_str();
390 : : }
391 : :
392 : 5 : const char* cvc5_cmd_get_name(const Cvc5Command cmd)
393 : : {
394 [ + + ]: 5 : static thread_local std::string str;
395 : 5 : CVC5_CAPI_TRY_CATCH_BEGIN;
396 [ + + ][ + + ]: 5 : CVC5_CAPI_CHECK_CMD(cmd);
[ - - ]
397 : 4 : str = cmd->d_cmd.getCommandName();
398 [ + - ][ - + ]: 1 : CVC5_CAPI_TRY_CATCH_END;
[ - - ][ - - ]
[ - - ][ - - ]
[ - ]
399 : 5 : return str.c_str();
400 : : }
401 : :
402 : : /* -------------------------------------------------------------------------- */
403 : :
404 : 54 : Cvc5InputParser* cvc5_parser_new(Cvc5* cvc5, Cvc5SymbolManager* sm)
405 : : {
406 : 54 : Cvc5InputParser* res = nullptr;
407 : 54 : CVC5_CAPI_TRY_CATCH_BEGIN;
408 [ + + ][ + + ]: 54 : CVC5_CAPI_CHECK_NOT_NULL(cvc5);
[ - - ]
409 [ + + ]: 53 : if (sm)
410 : : {
411 : 41 : res = new Cvc5InputParser(cvc5, sm);
412 : : }
413 : : else
414 : : {
415 : 12 : res = new Cvc5InputParser(cvc5);
416 : : }
417 [ + - ][ - + ]: 1 : CVC5_CAPI_TRY_CATCH_END;
[ - - ][ - - ]
[ - - ][ - - ]
[ - ]
418 : 54 : return res;
419 : : }
420 : :
421 : 53 : void cvc5_parser_delete(Cvc5InputParser* parser)
422 : : {
423 : 53 : CVC5_CAPI_TRY_CATCH_BEGIN;
424 [ - + ][ - + ]: 53 : CVC5_CAPI_CHECK_NOT_NULL(parser);
[ - - ]
425 : : // Commands allocated by this parser keep it alive, it is only freed once
426 : : // all of them have been released.
427 : 53 : parser->dec_ref();
428 [ - - ][ - - ]: 0 : CVC5_CAPI_TRY_CATCH_END;
[ - - ][ - - ]
[ - - ][ - - ]
[ - ]
429 : 53 : }
430 : :
431 : 51 : void cvc5_parser_release(Cvc5InputParser* parser)
432 : : {
433 : 51 : CVC5_CAPI_TRY_CATCH_BEGIN;
434 [ - + ][ - + ]: 51 : CVC5_CAPI_CHECK_NOT_NULL(parser);
[ - - ]
435 : 51 : parser->release();
436 [ - - ][ - - ]: 0 : CVC5_CAPI_TRY_CATCH_END;
[ - - ][ - - ]
[ - - ][ - - ]
[ - ]
437 : 51 : }
438 : :
439 : 1 : Cvc5* cvc5_parser_get_solver(Cvc5InputParser* parser)
440 : : {
441 : 1 : Cvc5* res = nullptr;
442 : 1 : CVC5_CAPI_TRY_CATCH_BEGIN;
443 : 1 : res = parser->d_cvc5;
444 : : CVC5_CAPI_TRY_CATCH_END;
445 : 1 : return res;
446 : : }
447 : :
448 : 1 : Cvc5SymbolManager* cvc5_parser_get_sm(Cvc5InputParser* parser)
449 : : {
450 : 1 : Cvc5SymbolManager* res = nullptr;
451 : 1 : CVC5_CAPI_TRY_CATCH_BEGIN;
452 : 1 : res = parser->d_sm;
453 : : CVC5_CAPI_TRY_CATCH_END;
454 : 1 : return res;
455 : : }
456 : :
457 : 4 : void cvc5_parser_set_file_input(Cvc5InputParser* parser,
458 : : Cvc5InputLanguage lang,
459 : : const char* filename)
460 : : {
461 : 4 : CVC5_CAPI_TRY_CATCH_BEGIN;
462 [ + + ][ + + ]: 4 : CVC5_CAPI_CHECK_NOT_NULL(parser);
[ - - ]
463 [ + - ][ + - ]: 3 : CVC5_CAPI_CHECK_INPUT_LANGUAGE(lang);
[ - + ][ - + ]
[ - - ]
464 [ + + ][ + + ]: 3 : CVC5_CAPI_CHECK_NOT_NULL(filename);
[ - - ]
465 : 4 : parser->d_parser.setFileInput(static_cast<cvc5::modes::InputLanguage>(lang),
466 : : filename);
467 [ + - ][ - + ]: 3 : CVC5_CAPI_TRY_CATCH_END;
[ - - ][ - - ]
[ - - ][ - - ]
[ - ]
468 : 4 : }
469 : :
470 : 49 : void cvc5_parser_set_str_input(Cvc5InputParser* parser,
471 : : Cvc5InputLanguage lang,
472 : : const char* input,
473 : : const char* name)
474 : : {
475 : 49 : CVC5_CAPI_TRY_CATCH_BEGIN;
476 [ + + ][ + + ]: 49 : CVC5_CAPI_CHECK_NOT_NULL(parser);
[ - - ]
477 [ + - ][ + - ]: 48 : CVC5_CAPI_CHECK_INPUT_LANGUAGE(lang);
[ - + ][ - + ]
[ - - ]
478 [ + + ][ + + ]: 48 : CVC5_CAPI_CHECK_NOT_NULL(input);
[ - - ]
479 [ + + ][ + + ]: 47 : CVC5_CAPI_CHECK_NOT_NULL(name);
[ - - ]
480 : 46 : parser->d_parser.setStringInput(
481 : : static_cast<cvc5::modes::InputLanguage>(lang), input, name);
482 [ + - ][ - + ]: 3 : CVC5_CAPI_TRY_CATCH_END;
[ - - ][ - - ]
[ - - ][ - - ]
[ - ]
483 : 49 : }
484 : :
485 : 21 : void cvc5_parser_set_inc_str_input(Cvc5InputParser* parser,
486 : : Cvc5InputLanguage lang,
487 : : const char* name)
488 : : {
489 : 21 : CVC5_CAPI_TRY_CATCH_BEGIN;
490 [ + + ][ + + ]: 21 : CVC5_CAPI_CHECK_NOT_NULL(parser);
[ - - ]
491 [ + - ][ + - ]: 20 : CVC5_CAPI_CHECK_INPUT_LANGUAGE(lang);
[ - + ][ - + ]
[ - - ]
492 [ + + ][ + + ]: 20 : CVC5_CAPI_CHECK_NOT_NULL(name);
[ - - ]
493 : 21 : parser->d_parser.setIncrementalStringInput(
494 : : static_cast<cvc5::modes::InputLanguage>(lang), name);
495 [ + - ][ - + ]: 3 : CVC5_CAPI_TRY_CATCH_END;
[ - - ][ - - ]
[ - - ][ - - ]
[ - ]
496 : 21 : }
497 : :
498 : 40 : void cvc5_parser_append_inc_str_input(Cvc5InputParser* parser,
499 : : const char* input)
500 : : {
501 [ + + ]: 40 : static thread_local std::string error;
502 : 40 : CVC5_CAPI_TRY_CATCH_BEGIN;
503 [ + + ][ + + ]: 40 : CVC5_CAPI_CHECK_NOT_NULL(parser);
[ - - ]
504 [ + + ][ + + ]: 39 : CVC5_CAPI_CHECK_NOT_NULL(input);
[ - - ]
505 : 40 : parser->d_parser.appendIncrementalStringInput(input);
506 [ + - ][ - + ]: 3 : CVC5_CAPI_TRY_CATCH_END;
[ - - ][ - - ]
[ - - ][ - - ]
[ - ]
507 : 40 : }
508 : :
509 : 169 : Cvc5Command cvc5_parser_next_command(Cvc5InputParser* parser,
510 : : const char** error_msg)
511 : : {
512 : 169 : Cvc5Command res = nullptr;
513 [ + + ]: 169 : static thread_local std::string error;
514 : 169 : CVC5_CAPI_TRY_CATCH_BEGIN;
515 [ + + ][ + + ]: 169 : CVC5_CAPI_CHECK_NOT_NULL(parser);
[ - - ]
516 [ + + ][ + + ]: 168 : CVC5_CAPI_CHECK_NOT_NULL(error_msg);
[ - - ]
517 : : try
518 : : {
519 : 167 : cvc5::parser::Command cres = parser->d_parser.nextCommand();
520 [ + + ]: 165 : res = cres.isNull() ? nullptr : parser->export_cmd(cres);
521 : 165 : error = "";
522 : 165 : *error_msg = nullptr;
523 : 165 : }
524 [ + + ]: 2 : catch (cvc5::parser::ParserException& e)
525 : : {
526 : 1 : error = e.getMessage();
527 : 1 : *error_msg = error.c_str();
528 : 1 : }
529 [ + - ][ - + ]: 3 : CVC5_CAPI_TRY_CATCH_END;
[ - - ][ - - ]
[ - - ][ - - ]
[ - ]
530 : 169 : return res;
531 : : }
532 : :
533 : 34 : Cvc5Term cvc5_parser_next_term(Cvc5InputParser* parser, const char** error_msg)
534 : : {
535 : 34 : Cvc5Term res = nullptr;
536 [ + + ]: 34 : static thread_local std::string error;
537 : 34 : CVC5_CAPI_TRY_CATCH_BEGIN;
538 [ + + ][ + + ]: 34 : CVC5_CAPI_CHECK_NOT_NULL(parser);
[ - - ]
539 [ + + ][ + + ]: 33 : CVC5_CAPI_CHECK_NOT_NULL(error_msg);
[ - - ]
540 : : try
541 : : {
542 : 32 : cvc5::Term cres = parser->d_parser.nextTerm();
543 [ + + ]: 30 : res = cres.isNull() ? nullptr : parser->d_cvc5->d_tm->export_term(cres);
544 : 30 : error = "";
545 : 30 : *error_msg = nullptr;
546 : 30 : }
547 [ + + ]: 2 : catch (cvc5::parser::ParserException& e)
548 : : {
549 : 1 : error = e.getMessage();
550 : 1 : *error_msg = error.c_str();
551 : 1 : }
552 [ + - ][ - + ]: 3 : CVC5_CAPI_TRY_CATCH_END;
[ - - ][ - - ]
[ - - ][ - - ]
[ - ]
553 : 34 : return res;
554 : : }
555 : :
556 : 28 : bool cvc5_parser_done(Cvc5InputParser* parser)
557 : : {
558 : 28 : bool res = false;
559 : 28 : CVC5_CAPI_TRY_CATCH_BEGIN;
560 [ - + ][ - + ]: 28 : CVC5_CAPI_CHECK_NOT_NULL(parser);
[ - - ]
561 : 28 : res = parser->d_parser.done();
562 [ - - ][ - - ]: 0 : CVC5_CAPI_TRY_CATCH_END;
[ - - ][ - - ]
[ - - ][ - - ]
[ - ]
563 : 28 : return res;
564 : : }
|
