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 : : * The cvc5 C Parser API.
14 : : */
15 : :
16 : : extern "C" {
17 : : #include <cvc5/c/cvc5_parser.h>
18 : : }
19 : :
20 : : #include <cvc5/cvc5.h>
21 : : #include <cvc5/cvc5_parser.h>
22 : :
23 : : #include <fstream>
24 : :
25 : : #include "api/c/cvc5_c_structs.h"
26 : : #include "api/c/cvc5_checks.h"
27 : :
28 : : /* -------------------------------------------------------------------------- */
29 : :
30 : : /** Wrapper for cvc5 C++ command. */
31 : : struct cvc5_cmd_t
32 : : {
33 : : /**
34 : : * Constructor.
35 : : * @param parser The associated parser instance.
36 : : * @param cmd The wrapped C++ command.
37 : : */
38 : 233 : cvc5_cmd_t(Cvc5InputParser* parser, const cvc5::parser::Command& cmd)
39 : 233 : : d_cmd(cmd), d_parser(parser)
40 : : {
41 : 233 : }
42 : : /** The associated command instance. */
43 : : cvc5::parser::Command d_cmd;
44 : : /** The associated parserinstance. */
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 : 184 : Cvc5SymbolManager(Cvc5TermManager* tm)
56 : 184 : : d_sm_wrapped(new cvc5::parser::SymbolManager(tm->d_tm)),
57 : 184 : d_sm(*d_sm_wrapped),
58 : 368 : d_tm(tm)
59 : : {
60 : 184 : }
61 : 117 : Cvc5SymbolManager(cvc5::parser::SymbolManager& sm, Cvc5TermManager* tm)
62 : 117 : : d_sm(sm), d_tm(tm)
63 : : {
64 : 117 : }
65 : : /**
66 : : * The created symbol manager instance.
67 : : *
68 : : * This will be a newly created symbol manager when created via
69 : : * cvc5_symbol_manager_new(). However, if we create a parsere via
70 : : * cvc5_parser_new() while passing NULL as a symbol manager, this will be
71 : : * NULL and `d_sm` will point to the symbol manager created by the parser.
72 : : */
73 : : std::unique_ptr<cvc5::parser::SymbolManager> d_sm_wrapped;
74 : : /** The associated symbol manager instance. */
75 : : cvc5::parser::SymbolManager& d_sm;
76 : : /** The associated term manager. */
77 : : Cvc5TermManager* d_tm = nullptr;
78 : : };
79 : :
80 : : /** Wrapper for cvc5 C++ parser. */
81 : : struct Cvc5InputParser
82 : : {
83 : : /**
84 : : * Constructor.
85 : : * @param cvc5 The associated solver instance.
86 : : */
87 : 117 : Cvc5InputParser(Cvc5* cvc5) : d_parser(&cvc5->d_solver), d_cvc5(cvc5)
88 : : {
89 : 234 : d_sm_wrapped.reset(new Cvc5SymbolManager(*d_parser.getSymbolManager(),
90 : 117 : cvc5_get_tm(d_cvc5)));
91 : 117 : d_sm = d_sm_wrapped.get();
92 : 117 : }
93 : : /**
94 : : * Constructor.
95 : : * @param cvc5 The associated solver instance.
96 : : * @param sm The associated symbol manager.
97 : : */
98 : 65 : Cvc5InputParser(Cvc5* cvc5, Cvc5SymbolManager* sm)
99 : 65 : : d_parser(&cvc5->d_solver, &sm->d_sm), d_cvc5(cvc5), d_sm(sm)
100 : : {
101 : 65 : }
102 : :
103 : : /**
104 : : * Export C++ command to C API.
105 : : * @param cmd The command to export.
106 : : */
107 : : Cvc5Command export_cmd(const cvc5::parser::Command& cmd);
108 : :
109 : : /** The associated input parser instance. */
110 : : cvc5::parser::InputParser d_parser;
111 : : /** The associated solver instance. */
112 : : Cvc5* d_cvc5 = nullptr;
113 : : /** The associated symbol manager instance. */
114 : : Cvc5SymbolManager* d_sm = nullptr;
115 : : /**
116 : : * Maintain Cvc5SymbolManager wrapper instance if symbol manager was not
117 : : * given via constructor but created by the parser.
118 : : */
119 : : std::unique_ptr<Cvc5SymbolManager> d_sm_wrapped;
120 : : /** The allocated command objects. */
121 : : std::vector<cvc5_cmd_t> d_alloc_cmds;
122 : : };
123 : :
124 : : /* -------------------------------------------------------------------------- */
125 : :
126 : 233 : Cvc5Command Cvc5InputParser::export_cmd(const cvc5::parser::Command& cmd)
127 : : {
128 [ - + ][ - + ]: 233 : Assert(!cmd.isNull());
[ - - ]
129 : 233 : d_alloc_cmds.emplace_back(this, cmd);
130 : 233 : return &d_alloc_cmds.back();
131 : : }
132 : :
133 : : /* -------------------------------------------------------------------------- */
134 : :
135 : 184 : Cvc5SymbolManager* cvc5_symbol_manager_new(Cvc5TermManager* tm)
136 : : {
137 : 184 : Cvc5SymbolManager* res = nullptr;
138 : : CVC5_CAPI_TRY_CATCH_BEGIN;
139 [ - + ][ - + ]: 184 : CVC5_CAPI_CHECK_NOT_NULL(tm);
[ - - ]
140 : 184 : res = new Cvc5SymbolManager(tm);
141 : 0 : CVC5_CAPI_TRY_CATCH_END;
142 : 184 : return res;
143 : : }
144 : :
145 : 152 : void cvc5_symbol_manager_delete(Cvc5SymbolManager* sm)
146 : : {
147 : : CVC5_CAPI_TRY_CATCH_BEGIN;
148 [ - + ][ - + ]: 152 : CVC5_CAPI_CHECK_NOT_NULL(sm);
[ - - ]
149 [ + - ]: 152 : delete sm;
150 : 0 : CVC5_CAPI_TRY_CATCH_END;
151 : 152 : }
152 : :
153 : 18 : bool cvc5_sm_is_logic_set(Cvc5SymbolManager* sm)
154 : : {
155 : 18 : bool res = false;
156 : : CVC5_CAPI_TRY_CATCH_BEGIN;
157 [ + + ][ + + ]: 18 : CVC5_CAPI_CHECK_NOT_NULL(sm);
[ - - ]
158 : 17 : res = sm->d_sm.isLogicSet();
159 : 1 : CVC5_CAPI_TRY_CATCH_END;
160 : 17 : return res;
161 : : }
162 : :
163 : 11 : const char* cvc5_sm_get_logic(Cvc5SymbolManager* sm)
164 : : {
165 [ + + ]: 11 : static thread_local std::string str;
166 : : CVC5_CAPI_TRY_CATCH_BEGIN;
167 [ + + ][ + + ]: 11 : CVC5_CAPI_CHECK_NOT_NULL(sm);
[ - - ]
168 : 10 : str = sm->d_sm.getLogic();
169 : 2 : CVC5_CAPI_TRY_CATCH_END;
170 : 9 : return str.c_str();
171 : : }
172 : :
173 : 8 : const Cvc5Sort* cvc5_sm_get_declared_sorts(Cvc5SymbolManager* sm, size_t* size)
174 : : {
175 [ + + ]: 8 : static thread_local std::vector<Cvc5Sort> res;
176 : : CVC5_CAPI_TRY_CATCH_BEGIN;
177 [ + + ][ + + ]: 8 : CVC5_CAPI_CHECK_NOT_NULL(sm);
[ - - ]
178 [ + + ][ + + ]: 7 : CVC5_CAPI_CHECK_NOT_NULL(size);
[ - - ]
179 : 6 : res.clear();
180 : 6 : auto sorts = sm->d_sm.getDeclaredSorts();
181 : 6 : auto tm = sm->d_tm;
182 [ + + ]: 7 : for (auto& s : sorts)
183 : : {
184 : 1 : res.push_back(tm->export_sort(s));
185 : : }
186 : 6 : *size = res.size();
187 : 2 : CVC5_CAPI_TRY_CATCH_END;
188 [ + + ]: 6 : return *size > 0 ? res.data() : nullptr;
189 : : }
190 : :
191 : 6 : const Cvc5Term* cvc5_sm_get_declared_terms(Cvc5SymbolManager* sm, size_t* size)
192 : : {
193 [ + + ]: 6 : static thread_local std::vector<Cvc5Term> res;
194 : : CVC5_CAPI_TRY_CATCH_BEGIN;
195 [ + + ][ + + ]: 6 : CVC5_CAPI_CHECK_NOT_NULL(sm);
[ - - ]
196 [ + + ][ + + ]: 5 : CVC5_CAPI_CHECK_NOT_NULL(size);
[ - - ]
197 : 4 : res.clear();
198 : 4 : auto terms = sm->d_sm.getDeclaredTerms();
199 : 4 : auto tm = sm->d_tm;
200 [ + + ]: 5 : for (auto& t : terms)
201 : : {
202 : 1 : res.push_back(tm->export_term(t));
203 : : }
204 : 4 : *size = res.size();
205 : 2 : CVC5_CAPI_TRY_CATCH_END;
206 [ + + ]: 4 : return *size > 0 ? res.data() : nullptr;
207 : : }
208 : :
209 : :
210 : 2 : void cvc5_sm_get_named_terms(Cvc5SymbolManager* sm,
211 : : size_t* size,
212 : : Cvc5Term* terms[],
213 : : const char** names[])
214 : : {
215 [ + + ]: 2 : static thread_local std::vector<Cvc5Term> rterms;
216 [ + + ]: 2 : static thread_local std::vector<const char*> rnames;
217 : : CVC5_CAPI_TRY_CATCH_BEGIN;
218 [ - + ][ - + ]: 2 : CVC5_CAPI_CHECK_NOT_NULL(sm);
[ - - ]
219 [ - + ][ - + ]: 2 : CVC5_CAPI_CHECK_NOT_NULL(size);
[ - - ]
220 [ - + ][ - + ]: 2 : CVC5_CAPI_CHECK_NOT_NULL(terms);
[ - - ]
221 [ - + ][ - + ]: 2 : CVC5_CAPI_CHECK_NOT_NULL(names);
[ - - ]
222 : 2 : rterms.clear();
223 : 2 : rnames.clear();
224 : 2 : auto res = sm->d_sm.getNamedTerms();
225 : 2 : auto tm = sm->d_tm;
226 [ + + ]: 3 : for (auto& t : res)
227 : : {
228 : 1 : rterms.push_back(tm->export_term(t.first));
229 : 1 : rnames.push_back(t.second.c_str());
230 : : }
231 : 2 : *size = rterms.size();
232 : 2 : *terms = rterms.data();
233 : 2 : *names = rnames.data();
234 : 0 : CVC5_CAPI_TRY_CATCH_END;
235 : 2 : }
236 : :
237 : : /* -------------------------------------------------------------------------- */
238 : :
239 : 231 : const char* cvc5_cmd_invoke(Cvc5Command cmd, Cvc5* cvc5, Cvc5SymbolManager* sm)
240 : : {
241 [ + + ]: 231 : static thread_local std::string str;
242 : : CVC5_CAPI_TRY_CATCH_BEGIN;
243 [ + + ][ + + ]: 231 : CVC5_CAPI_CHECK_CMD(cmd);
[ - - ]
244 [ + + ][ + + ]: 230 : CVC5_CAPI_CHECK_NOT_NULL(cvc5);
[ - - ]
245 [ + + ][ + + ]: 229 : CVC5_CAPI_CHECK_NOT_NULL(sm);
[ - - ]
246 : 228 : std::stringstream ss;
247 : 228 : cmd->d_cmd.invoke(&cvc5->d_solver, &sm->d_sm, ss);
248 : 228 : str = ss.str();
249 : 3 : CVC5_CAPI_TRY_CATCH_END;
250 : 228 : return str.c_str();
251 : : }
252 : :
253 : 4 : const char* cvc5_cmd_to_string(const Cvc5Command cmd)
254 : : {
255 [ + + ]: 4 : static thread_local std::string str;
256 : : CVC5_CAPI_TRY_CATCH_BEGIN;
257 [ + + ][ + + ]: 4 : CVC5_CAPI_CHECK_CMD(cmd);
[ - - ]
258 : 3 : str = cmd->d_cmd.toString();
259 : 1 : CVC5_CAPI_TRY_CATCH_END;
260 : 3 : return str.c_str();
261 : : }
262 : :
263 : 3 : const char* cvc5_cmd_get_name(const Cvc5Command cmd)
264 : : {
265 [ + + ]: 3 : static thread_local std::string str;
266 : : CVC5_CAPI_TRY_CATCH_BEGIN;
267 [ + + ][ + + ]: 3 : CVC5_CAPI_CHECK_CMD(cmd);
[ - - ]
268 : 2 : str = cmd->d_cmd.getCommandName();
269 : 1 : CVC5_CAPI_TRY_CATCH_END;
270 : 2 : return str.c_str();
271 : : }
272 : :
273 : : /* -------------------------------------------------------------------------- */
274 : :
275 : 183 : Cvc5InputParser* cvc5_parser_new(Cvc5* cvc5, Cvc5SymbolManager* sm)
276 : : {
277 : 183 : Cvc5InputParser* res = nullptr;
278 : : CVC5_CAPI_TRY_CATCH_BEGIN;
279 [ + + ][ + + ]: 183 : CVC5_CAPI_CHECK_NOT_NULL(cvc5);
[ - - ]
280 [ + + ]: 182 : if (sm)
281 : : {
282 : 65 : res = new Cvc5InputParser(cvc5, sm);
283 : : }
284 : : else
285 : : {
286 : 117 : res = new Cvc5InputParser(cvc5);
287 : : }
288 : 1 : CVC5_CAPI_TRY_CATCH_END;
289 : 182 : return res;
290 : : }
291 : :
292 : 154 : void cvc5_parser_delete(Cvc5InputParser* parser)
293 : : {
294 : : CVC5_CAPI_TRY_CATCH_BEGIN;
295 [ - + ][ - + ]: 154 : CVC5_CAPI_CHECK_NOT_NULL(parser);
[ - - ]
296 [ + - ]: 154 : delete parser;
297 : 0 : CVC5_CAPI_TRY_CATCH_END;
298 : 154 : }
299 : :
300 : 0 : void cvc5_parser_release(Cvc5InputParser* parser)
301 : : {
302 : : CVC5_CAPI_TRY_CATCH_BEGIN;
303 : 0 : CVC5_CAPI_CHECK_NOT_NULL(parser);
304 : 0 : parser->d_alloc_cmds.clear();
305 : 0 : CVC5_CAPI_TRY_CATCH_END;
306 : 0 : }
307 : :
308 : 21 : Cvc5* cvc5_parser_get_solver(Cvc5InputParser* parser)
309 : : {
310 : 21 : Cvc5* res = nullptr;
311 : : CVC5_CAPI_TRY_CATCH_BEGIN;
312 : 21 : res = parser->d_cvc5;
313 : : CVC5_CAPI_TRY_CATCH_END;
314 : 21 : return res;
315 : : }
316 : :
317 : 0 : Cvc5SymbolManager* cvc5_parser_get_sm(Cvc5InputParser* parser)
318 : : {
319 : 0 : Cvc5SymbolManager* res = nullptr;
320 : : CVC5_CAPI_TRY_CATCH_BEGIN;
321 : 0 : res = parser->d_sm;
322 : : CVC5_CAPI_TRY_CATCH_END;
323 : 0 : return res;
324 : : }
325 : :
326 : 23 : void cvc5_parser_set_file_input(Cvc5InputParser* parser,
327 : : Cvc5InputLanguage lang,
328 : : const char* filename)
329 : : {
330 : : CVC5_CAPI_TRY_CATCH_BEGIN;
331 [ + + ][ + + ]: 23 : CVC5_CAPI_CHECK_NOT_NULL(parser);
[ - - ]
332 [ + - ][ + - ]: 44 : CVC5_CAPI_CHECK_INPUT_LANGUAGE(lang);
[ - + ][ - - ]
333 [ + + ][ + + ]: 22 : CVC5_CAPI_CHECK_NOT_NULL(filename);
[ - - ]
334 : 23 : parser->d_parser.setFileInput(static_cast<cvc5::modes::InputLanguage>(lang),
335 : : filename);
336 : 3 : CVC5_CAPI_TRY_CATCH_END;
337 : 20 : }
338 : :
339 : 79 : void cvc5_parser_set_str_input(Cvc5InputParser* parser,
340 : : Cvc5InputLanguage lang,
341 : : const char* input,
342 : : const char* name)
343 : : {
344 : : CVC5_CAPI_TRY_CATCH_BEGIN;
345 [ + + ][ + + ]: 79 : CVC5_CAPI_CHECK_NOT_NULL(parser);
[ - - ]
346 [ + - ][ + - ]: 156 : CVC5_CAPI_CHECK_INPUT_LANGUAGE(lang);
[ - + ][ - - ]
347 [ + + ][ + + ]: 78 : CVC5_CAPI_CHECK_NOT_NULL(input);
[ - - ]
348 [ + + ][ + + ]: 77 : CVC5_CAPI_CHECK_NOT_NULL(name);
[ - - ]
349 : 76 : parser->d_parser.setStringInput(
350 : : static_cast<cvc5::modes::InputLanguage>(lang), input, name);
351 : 3 : CVC5_CAPI_TRY_CATCH_END;
352 : 76 : }
353 : :
354 : 62 : void cvc5_parser_set_inc_str_input(Cvc5InputParser* parser,
355 : : Cvc5InputLanguage lang,
356 : : const char* name)
357 : : {
358 : : CVC5_CAPI_TRY_CATCH_BEGIN;
359 [ + + ][ + + ]: 62 : CVC5_CAPI_CHECK_NOT_NULL(parser);
[ - - ]
360 [ + - ][ + - ]: 122 : CVC5_CAPI_CHECK_INPUT_LANGUAGE(lang);
[ - + ][ - - ]
361 [ + + ][ + + ]: 61 : CVC5_CAPI_CHECK_NOT_NULL(name);
[ - - ]
362 : 62 : parser->d_parser.setIncrementalStringInput(
363 : : static_cast<cvc5::modes::InputLanguage>(lang), name);
364 : 3 : CVC5_CAPI_TRY_CATCH_END;
365 : 59 : }
366 : :
367 : 126 : void cvc5_parser_append_inc_str_input(Cvc5InputParser* parser,
368 : : const char* input)
369 : : {
370 [ + + ]: 126 : static thread_local std::string error;
371 : : CVC5_CAPI_TRY_CATCH_BEGIN;
372 [ + + ][ + + ]: 126 : CVC5_CAPI_CHECK_NOT_NULL(parser);
[ - - ]
373 [ + + ][ + + ]: 125 : CVC5_CAPI_CHECK_NOT_NULL(input);
[ - - ]
374 : 126 : parser->d_parser.appendIncrementalStringInput(input);
375 : 3 : CVC5_CAPI_TRY_CATCH_END;
376 : 123 : }
377 : :
378 : 313 : Cvc5Command cvc5_parser_next_command(Cvc5InputParser* parser,
379 : : const char** error_msg)
380 : : {
381 : 313 : Cvc5Command res = nullptr;
382 [ + + ]: 313 : static thread_local std::string error;
383 : : CVC5_CAPI_TRY_CATCH_BEGIN;
384 [ + + ][ + + ]: 313 : CVC5_CAPI_CHECK_NOT_NULL(parser);
[ - - ]
385 [ + + ][ + + ]: 312 : CVC5_CAPI_CHECK_NOT_NULL(error_msg);
[ - - ]
386 : : try
387 : : {
388 : 311 : cvc5::parser::Command cres = parser->d_parser.nextCommand();
389 [ + + ]: 307 : res = cres.isNull() ? nullptr : parser->export_cmd(cres);
390 : 307 : error = "";
391 : 307 : *error_msg = nullptr;
392 : : }
393 : 3 : catch (cvc5::parser::ParserException& e)
394 : : {
395 : 3 : error = e.getMessage();
396 : 3 : *error_msg = error.c_str();
397 : : }
398 : 3 : CVC5_CAPI_TRY_CATCH_END;
399 : 310 : return res;
400 : : }
401 : :
402 : 47 : Cvc5Term cvc5_parser_next_term(Cvc5InputParser* parser, const char** error_msg)
403 : : {
404 : 47 : Cvc5Term res = nullptr;
405 [ + + ]: 47 : static thread_local std::string error;
406 : : CVC5_CAPI_TRY_CATCH_BEGIN;
407 [ + + ][ + + ]: 47 : CVC5_CAPI_CHECK_NOT_NULL(parser);
[ - - ]
408 [ + + ][ + + ]: 46 : CVC5_CAPI_CHECK_NOT_NULL(error_msg);
[ - - ]
409 : : try
410 : : {
411 : 45 : cvc5::Term cres = parser->d_parser.nextTerm();
412 [ + + ]: 41 : res = cres.isNull() ? nullptr : parser->d_cvc5->d_tm->export_term(cres);
413 : 41 : error = "";
414 : 41 : *error_msg = nullptr;
415 : : }
416 : 3 : catch (cvc5::parser::ParserException& e)
417 : : {
418 : 3 : error = e.getMessage();
419 : 3 : *error_msg = error.c_str();
420 : : }
421 : 3 : CVC5_CAPI_TRY_CATCH_END;
422 : 44 : return res;
423 : : }
424 : :
425 : 104 : bool cvc5_parser_done(Cvc5InputParser* parser)
426 : : {
427 : 104 : bool res = false;
428 : : CVC5_CAPI_TRY_CATCH_BEGIN;
429 [ - + ][ - + ]: 104 : CVC5_CAPI_CHECK_NOT_NULL(parser);
[ - - ]
430 : 104 : res = parser->d_parser.done();
431 : 0 : CVC5_CAPI_TRY_CATCH_END;
432 : 104 : return res;
433 : : }
|
