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 symbol manager.
11 : : */
12 : :
13 : : #include "parser/sym_manager.h"
14 : :
15 : : #include "context/cdhashmap.h"
16 : : #include "context/cdhashset.h"
17 : : #include "context/cdlist.h"
18 : : #include "context/cdo.h"
19 : : #include "parser/symbol_table.h"
20 : :
21 : : using namespace cvc5::context;
22 : : using namespace cvc5::internal::parser;
23 : :
24 : : namespace cvc5::parser {
25 : :
26 : : // ---------------------------------------------- SymManager::Implementation
27 : :
28 : : class SymManager::Implementation
29 : : {
30 : : using TermStringMap =
31 : : CDHashMap<cvc5::Term, std::string, std::hash<cvc5::Term>>;
32 : : using TermSet = CDHashSet<cvc5::Term, std::hash<cvc5::Term>>;
33 : : using SortList = CDList<cvc5::Sort>;
34 : : using TermList = CDList<cvc5::Term>;
35 : :
36 : : public:
37 : 28553 : Implementation()
38 : 28553 : : d_context(),
39 : 28553 : d_names(&d_context),
40 : 28553 : d_namedAsserts(&d_context),
41 : 28553 : d_declareSorts(&d_context),
42 : 28553 : d_declareTerms(&d_context),
43 : 28553 : d_funToSynth(&d_context),
44 : 28553 : d_hasPushedScope(&d_context, false),
45 : 57106 : d_lastSynthName(&d_context)
46 : : {
47 : : // use an outermost push, to be able to clear all definitions
48 : 28553 : d_context.push();
49 : 28553 : }
50 : :
51 : 28504 : ~Implementation() { d_context.pop(); }
52 : 611509 : SymbolTable& getSymbolTable() { return d_symtabAllocated; }
53 : :
54 : : /** set expression name */
55 : : NamingResult setExpressionName(cvc5::Term t,
56 : : const std::string& name,
57 : : bool isAssertion = false);
58 : : /** get expression name */
59 : : bool getExpressionName(cvc5::Term t,
60 : : std::string& name,
61 : : bool isAssertion = false) const;
62 : : /** get expression names */
63 : : void getExpressionNames(const std::vector<cvc5::Term>& ts,
64 : : std::vector<std::string>& names,
65 : : bool areAssertions = false) const;
66 : : /** get expression names */
67 : : std::map<cvc5::Term, std::string> getExpressionNames(
68 : : bool areAssertions) const;
69 : : /** get model declare sorts */
70 : : std::vector<cvc5::Sort> getDeclaredSorts() const;
71 : : /** get model declare terms */
72 : : std::vector<cvc5::Term> getDeclaredTerms() const;
73 : : /** get functions to synthesize */
74 : : std::vector<cvc5::Term> getFunctionsToSynthesize() const;
75 : : /** Add declared sort to the list of model declarations. */
76 : : void addModelDeclarationSort(cvc5::Sort s);
77 : : /** Add declared term to the list of model declarations. */
78 : : void addModelDeclarationTerm(cvc5::Term t);
79 : : /** Add function to the list of functions to synthesize. */
80 : : void addFunctionToSynthesize(cvc5::Term t);
81 : : /** reset */
82 : : void reset();
83 : : /** reset assertions */
84 : : void resetAssertions();
85 : : /** Push a scope in the expression names. */
86 : : void pushScope(bool isUserContext);
87 : : /** Pop a scope in the expression names. */
88 : : void popScope();
89 : : /** Have we pushed a scope (e.g. let or quantifier) in the current context? */
90 : : bool hasPushedScope() const;
91 : : /** Set the last abduct-to-synthesize had the given name. */
92 : : void setLastSynthName(const std::string& name);
93 : : /** Get the name of the last abduct-to-synthesize */
94 : : const std::string& getLastSynthName() const;
95 : :
96 : : private:
97 : : /**
98 : : * The declaration scope that is "owned" by this symbol manager.
99 : : */
100 : : SymbolTable d_symtabAllocated;
101 : : /** The context manager for the scope maps. */
102 : : Context d_context;
103 : : /** Map terms to names */
104 : : TermStringMap d_names;
105 : : /** The set of terms with assertion names */
106 : : TermSet d_namedAsserts;
107 : : /** Declared sorts (for model printing) */
108 : : SortList d_declareSorts;
109 : : /** Declared terms (for model printing) */
110 : : TermList d_declareTerms;
111 : : /** Functions to synthesize (for response to check-synth) */
112 : : TermList d_funToSynth;
113 : : /**
114 : : * Have we pushed a scope (e.g. a let or quantifier) in the current context?
115 : : */
116 : : CDO<bool> d_hasPushedScope;
117 : : /** The last abduct or interpolant to synthesize name */
118 : : CDO<std::string> d_lastSynthName;
119 : : };
120 : :
121 : 22299 : NamingResult SymManager::Implementation::setExpressionName(
122 : : cvc5::Term t, const std::string& name, bool isAssertion)
123 : : {
124 [ + - ]: 44598 : Trace("sym-manager") << "SymManager: set expression name: " << t << " -> "
125 : 22299 : << name << ", isAssertion=" << isAssertion << std::endl;
126 [ + + ]: 22299 : if (d_hasPushedScope.get())
127 : : {
128 : : // cannot name subexpressions under binders
129 : 1 : return NamingResult::ERROR_IN_BINDER;
130 : : }
131 : :
132 [ + + ]: 22298 : if (isAssertion)
133 : : {
134 : 11038 : d_namedAsserts.insert(t);
135 : : }
136 [ + + ]: 22298 : if (d_names.find(t) != d_names.end())
137 : : {
138 : : // already named assertion
139 : 11949 : return NamingResult::ERROR_ALREADY_NAMED;
140 : : }
141 : 10349 : d_names[t] = name;
142 : 10349 : return NamingResult::SUCCESS;
143 : : }
144 : :
145 : 69 : bool SymManager::Implementation::getExpressionName(cvc5::Term t,
146 : : std::string& name,
147 : : bool isAssertion) const
148 : : {
149 : 69 : TermStringMap::const_iterator it = d_names.find(t);
150 [ + + ]: 69 : if (it == d_names.end())
151 : : {
152 : 25 : return false;
153 : : }
154 [ + - ]: 44 : if (isAssertion)
155 : : {
156 : : // must be an assertion name
157 [ - + ]: 44 : if (d_namedAsserts.find(t) == d_namedAsserts.end())
158 : : {
159 : 0 : return false;
160 : : }
161 : : }
162 : 44 : name = (*it).second;
163 : 44 : return true;
164 : : }
165 : :
166 : 26 : void SymManager::Implementation::getExpressionNames(
167 : : const std::vector<cvc5::Term>& ts,
168 : : std::vector<std::string>& names,
169 : : bool areAssertions) const
170 : : {
171 [ + + ]: 73 : for (const cvc5::Term& t : ts)
172 : : {
173 : 47 : std::string name;
174 [ + + ]: 47 : if (getExpressionName(t, name, areAssertions))
175 : : {
176 : 43 : names.push_back(name);
177 : : }
178 : 47 : }
179 : 26 : }
180 : :
181 : : std::map<cvc5::Term, std::string>
182 : 5234 : SymManager::Implementation::getExpressionNames(bool areAssertions) const
183 : : {
184 : 5234 : std::map<cvc5::Term, std::string> emap;
185 : 10468 : for (TermStringMap::const_iterator it = d_names.begin(),
186 : 5234 : itend = d_names.end();
187 [ + + ]: 8993 : it != itend;
188 : 3759 : ++it)
189 : : {
190 : 3759 : cvc5::Term t = (*it).first;
191 [ + + ][ + + ]: 3759 : if (areAssertions && d_namedAsserts.find(t) == d_namedAsserts.end())
[ + + ]
192 : : {
193 : 81 : continue;
194 : : }
195 : 3678 : emap[t] = (*it).second;
196 [ + + ]: 3759 : }
197 : 5234 : return emap;
198 : 0 : }
199 : :
200 : 177 : std::vector<cvc5::Sort> SymManager::Implementation::getDeclaredSorts() const
201 : : {
202 : : std::vector<cvc5::Sort> declareSorts(d_declareSorts.begin(),
203 : 177 : d_declareSorts.end());
204 : 177 : return declareSorts;
205 : : }
206 : :
207 : 66 : std::vector<cvc5::Term> SymManager::Implementation::getDeclaredTerms() const
208 : : {
209 : : std::vector<cvc5::Term> declareTerms(d_declareTerms.begin(),
210 : 66 : d_declareTerms.end());
211 : 66 : return declareTerms;
212 : : }
213 : :
214 : 20 : std::vector<cvc5::Term> SymManager::Implementation::getFunctionsToSynthesize()
215 : : const
216 : : {
217 : 20 : return std::vector<cvc5::Term>(d_funToSynth.begin(), d_funToSynth.end());
218 : : }
219 : :
220 : 11374 : void SymManager::Implementation::addModelDeclarationSort(cvc5::Sort s)
221 : : {
222 [ + - ]: 22748 : Trace("sym-manager") << "SymManager: addModelDeclarationSort " << s
223 : 11374 : << std::endl;
224 : 11374 : d_declareSorts.push_back(s);
225 : 11374 : }
226 : :
227 : 332160 : void SymManager::Implementation::addModelDeclarationTerm(cvc5::Term t)
228 : : {
229 [ + - ]: 664320 : Trace("sym-manager") << "SymManager: addModelDeclarationTerm " << t
230 : 332160 : << std::endl;
231 : 332160 : d_declareTerms.push_back(t);
232 : 332160 : }
233 : :
234 : 1609 : void SymManager::Implementation::addFunctionToSynthesize(cvc5::Term f)
235 : : {
236 [ + - ]: 3218 : Trace("sym-manager") << "SymManager: addFunctionToSynthesize " << f
237 : 1609 : << std::endl;
238 : 1609 : d_funToSynth.push_back(f);
239 : 1609 : }
240 : :
241 : 352876 : void SymManager::Implementation::pushScope(bool isUserContext)
242 : : {
243 [ + - ]: 705752 : Trace("sym-manager") << "SymManager: pushScope, isUserContext = "
244 : 352876 : << isUserContext << std::endl;
245 [ + + ][ + - ]: 352876 : Assert(!d_hasPushedScope.get() || !isUserContext)
[ - + ][ - + ]
[ - - ]
246 : 0 : << "cannot push a user context within a scope context";
247 : 352876 : d_context.push();
248 [ + + ]: 352876 : if (!isUserContext)
249 : : {
250 : 323229 : d_hasPushedScope = true;
251 : : }
252 : 352876 : d_symtabAllocated.pushScope();
253 : 352876 : }
254 : :
255 : 327907 : void SymManager::Implementation::popScope()
256 : : {
257 [ + - ]: 327907 : Trace("sym-manager") << "SymManager: popScope" << std::endl;
258 : 327907 : d_symtabAllocated.popScope();
259 [ - + ]: 327907 : if (d_context.getLevel() == 0)
260 : : {
261 : 0 : throw ScopeException();
262 : : }
263 : 327907 : d_context.pop();
264 [ + - ]: 655814 : Trace("sym-manager-debug")
265 : 327907 : << "d_hasPushedScope is now " << d_hasPushedScope.get() << std::endl;
266 : 327907 : }
267 : :
268 : 165 : bool SymManager::Implementation::hasPushedScope() const
269 : : {
270 : 165 : return d_hasPushedScope.get();
271 : : }
272 : :
273 : 89 : void SymManager::Implementation::setLastSynthName(const std::string& name)
274 : : {
275 : 89 : d_lastSynthName = name;
276 : 89 : }
277 : :
278 : 13 : const std::string& SymManager::Implementation::getLastSynthName() const
279 : : {
280 : 13 : return d_lastSynthName.get();
281 : : }
282 : :
283 : 83 : void SymManager::Implementation::reset()
284 : : {
285 [ + - ]: 83 : Trace("sym-manager") << "SymManager: reset" << std::endl;
286 : : // reset resets the symbol table even when global declarations are true
287 : 83 : d_symtabAllocated.reset();
288 : : // clear names by popping to context level 0
289 [ + + ]: 189 : while (d_context.getLevel() > 0)
290 : : {
291 : 106 : d_context.pop();
292 : : }
293 : : // push the outermost context
294 : 83 : d_context.push();
295 : 83 : }
296 : :
297 : 36 : void SymManager::Implementation::resetAssertions()
298 : : {
299 [ + - ]: 36 : Trace("sym-manager") << "SymManager: resetAssertions" << std::endl;
300 : : // clear names by popping to context level 1
301 [ + + ]: 60 : while (d_context.getLevel() > 1)
302 : : {
303 : 24 : d_context.pop();
304 : : }
305 : 36 : }
306 : :
307 : : // ---------------------------------------------- SymManager
308 : :
309 : 28553 : SymManager::SymManager(cvc5::TermManager& tm)
310 : 28553 : : d_tm(tm),
311 : 28553 : d_implementation(new SymManager::Implementation()),
312 : 28553 : d_globalDeclarations(false),
313 : 28553 : d_freshDeclarations(true),
314 : 28553 : d_termSortOverload(true),
315 : 28553 : d_logicIsForced(false),
316 : 28553 : d_logicIsSet(false),
317 : 28553 : d_logic()
318 : : {
319 : 28553 : }
320 : :
321 : 28504 : SymManager::~SymManager() {}
322 : :
323 : 24308 : SymbolTable* SymManager::getSymbolTable()
324 : : {
325 : 24308 : return &d_implementation->getSymbolTable();
326 : : }
327 : :
328 : 369371 : bool SymManager::bind(const std::string& name, cvc5::Term obj, bool doOverload)
329 : : {
330 : 369371 : return d_implementation->getSymbolTable().bind(name, obj, doOverload);
331 : : }
332 : :
333 : 205181 : bool SymManager::bindType(const std::string& name, cvc5::Sort t, bool isUser)
334 : : {
335 [ + + ][ - + ]: 205181 : if (isUser && !d_termSortOverload)
336 : : {
337 : : // if a user sort and d_termSortOverload is false, we bind a dummy constant
338 : : // to the term symbol table.
339 : 0 : cvc5::Sort dummyType = d_tm.mkUninterpretedSort("Type");
340 : 0 : cvc5::Term ts = d_tm.mkConst(dummyType, name);
341 [ - - ]: 0 : if (!d_implementation->getSymbolTable().bindDummySortTerm(name, ts))
342 : : {
343 : 0 : return false;
344 : : }
345 [ - - ][ - - ]: 0 : }
346 : 205181 : d_implementation->getSymbolTable().bindType(name, t);
347 : 205181 : return true;
348 : : }
349 : :
350 : 3869 : bool SymManager::bindMutualDatatypeTypes(
351 : : const std::vector<cvc5::Sort>& datatypes, bool bindTesters)
352 : : {
353 [ + + ]: 8756 : for (size_t i = 0, ntypes = datatypes.size(); i < ntypes; ++i)
354 : : {
355 : 4887 : Sort t = datatypes[i];
356 : 4887 : const Datatype& dt = t.getDatatype();
357 : 4887 : const std::string& name = dt.getName();
358 [ + - ]: 4887 : Trace("parser-idt") << "define " << name << " as " << t << std::endl;
359 [ + + ]: 4887 : if (dt.isParametric())
360 : : {
361 : 199 : std::vector<Sort> paramTypes = dt.getParameters();
362 [ - + ]: 199 : if (!bindType(name, paramTypes, t, true))
363 : : {
364 : 0 : return false;
365 : : }
366 [ + - ]: 199 : }
367 : : else
368 : : {
369 [ - + ]: 4688 : if (!bindType(name, t, true))
370 : : {
371 : 0 : return false;
372 : : }
373 : : }
374 [ + + ]: 13746 : for (size_t j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
375 : : {
376 : 8859 : const DatatypeConstructor& ctor = dt[j];
377 : 8859 : Term constructor = ctor.getTerm();
378 [ + - ]: 8859 : Trace("parser-idt") << "+ define " << constructor << std::endl;
379 : 8859 : std::string constructorName = ctor.getName();
380 : : // A zero argument constructor is actually APPLY_CONSTRUCTOR for the
381 : : // constructor.
382 [ + + ]: 8859 : if (ctor.getNumSelectors() == 0)
383 : : {
384 : 7842 : constructor = d_tm.mkTerm(Kind::APPLY_CONSTRUCTOR, {constructor});
385 : : }
386 : : // always do overloading
387 [ - + ]: 8859 : if (!bind(constructorName, constructor, true))
388 : : {
389 : 0 : return false;
390 : : }
391 [ + - ]: 8859 : if (bindTesters)
392 : : {
393 : 8859 : std::stringstream testerName;
394 : 8859 : testerName << "is-" << constructorName;
395 : 8859 : Term tester = ctor.getTesterTerm();
396 [ + - ][ - + ]: 8859 : Trace("parser-idt") << "+ define " << testerName.str() << std::endl;
[ - - ]
397 : : // always do overloading
398 [ - + ]: 8859 : if (!bind(testerName.str(), tester, true))
399 : : {
400 : 0 : return false;
401 : : }
402 [ + - ][ + - ]: 8859 : }
403 [ + + ]: 17185 : for (size_t k = 0, nargs = ctor.getNumSelectors(); k < nargs; k++)
404 : : {
405 : 8326 : const DatatypeSelector& sel = ctor[k];
406 : 8326 : Term selector = sel.getTerm();
407 [ + - ]: 8326 : Trace("parser-idt") << "+++ define " << selector << std::endl;
408 : 8326 : std::string selectorName = sel.getName();
409 : : // always do overloading
410 [ - + ]: 8326 : if (!bind(selectorName, selector, true))
411 : : {
412 : 0 : return false;
413 : : }
414 [ + - ][ + - ]: 8326 : }
[ + - ]
415 [ + - ][ + - ]: 8859 : }
[ + - ]
416 [ + - ][ + - ]: 4887 : }
[ + - ]
417 : 3869 : return true;
418 : : }
419 : :
420 : 12619 : bool SymManager::bindType(const std::string& name,
421 : : const std::vector<cvc5::Sort>& params,
422 : : cvc5::Sort t,
423 : : bool isUser)
424 : : {
425 [ + - ][ + + ]: 12619 : if (isUser && !d_termSortOverload)
426 : : {
427 : : // if a user sort and d_termSortOverload is false, we bind a dummy symbol
428 : : // to the term symbol table.
429 : 1 : cvc5::Sort dummyType = d_tm.mkUninterpretedSort("Type");
430 : 1 : cvc5::Term ts = d_tm.mkConst(dummyType, name);
431 [ - + ]: 1 : if (!d_implementation->getSymbolTable().bindDummySortTerm(name, ts))
432 : : {
433 : 0 : return false;
434 : : }
435 [ + - ][ + - ]: 1 : }
436 : 12619 : d_implementation->getSymbolTable().bindType(name, params, t);
437 : 12619 : return true;
438 : : }
439 : :
440 : 22299 : NamingResult SymManager::setExpressionName(cvc5::Term t,
441 : : const std::string& name,
442 : : bool isAssertion)
443 : : {
444 : 22299 : return d_implementation->setExpressionName(t, name, isAssertion);
445 : : }
446 : :
447 : 22 : bool SymManager::getExpressionName(cvc5::Term t,
448 : : std::string& name,
449 : : bool isAssertion) const
450 : : {
451 : 22 : return d_implementation->getExpressionName(t, name, isAssertion);
452 : : }
453 : :
454 : 26 : void SymManager::getExpressionNames(const std::vector<cvc5::Term>& ts,
455 : : std::vector<std::string>& names,
456 : : bool areAssertions) const
457 : : {
458 : 26 : return d_implementation->getExpressionNames(ts, names, areAssertions);
459 : : }
460 : :
461 : 5234 : std::map<cvc5::Term, std::string> SymManager::getExpressionNames(
462 : : bool areAssertions) const
463 : : {
464 : 5234 : return d_implementation->getExpressionNames(areAssertions);
465 : : }
466 : 177 : std::vector<cvc5::Sort> SymManager::getDeclaredSorts() const
467 : : {
468 : 177 : return d_implementation->getDeclaredSorts();
469 : : }
470 : 66 : std::vector<cvc5::Term> SymManager::getDeclaredTerms() const
471 : : {
472 : 66 : return d_implementation->getDeclaredTerms();
473 : : }
474 : :
475 : 20 : std::vector<cvc5::Term> SymManager::getFunctionsToSynthesize() const
476 : : {
477 : 20 : return d_implementation->getFunctionsToSynthesize();
478 : : }
479 : :
480 : 11374 : void SymManager::addModelDeclarationSort(cvc5::Sort s)
481 : : {
482 : 11374 : d_implementation->addModelDeclarationSort(s);
483 : 11374 : }
484 : :
485 : 332160 : void SymManager::addModelDeclarationTerm(cvc5::Term t)
486 : : {
487 : 332160 : d_implementation->addModelDeclarationTerm(t);
488 : 332160 : }
489 : :
490 : 1609 : void SymManager::addFunctionToSynthesize(cvc5::Term f)
491 : : {
492 : 1609 : d_implementation->addFunctionToSynthesize(f);
493 : 1609 : }
494 : :
495 : 16 : size_t SymManager::scopeLevel() const
496 : : {
497 : 16 : return d_implementation->getSymbolTable().getLevel();
498 : : }
499 : :
500 : 352979 : void SymManager::pushScope(bool isUserContext)
501 : : {
502 : : // we do not push user contexts when global declarations is true. This
503 : : // policy applies both to the symbol table and to the symbol manager.
504 [ + + ][ + + ]: 352979 : if (d_globalDeclarations && isUserContext)
505 : : {
506 : 103 : return;
507 : : }
508 : 352876 : d_implementation->pushScope(isUserContext);
509 : : }
510 : :
511 : 327926 : void SymManager::popScope()
512 : : {
513 : : // If global declarations is true, then if d_hasPushedScope is false, then
514 : : // the pop corresponds to a user context, which we did not push. Note this
515 : : // additionally relies on the fact that user contexts cannot be pushed
516 : : // within scope contexts. Hence, since we did not push the context, we
517 : : // do not pop a context here.
518 [ + + ][ + + ]: 327926 : if (d_globalDeclarations && !d_implementation->hasPushedScope())
[ + + ]
519 : : {
520 : 19 : return;
521 : : }
522 : 327907 : d_implementation->popScope();
523 : : }
524 : :
525 : 133 : void SymManager::setGlobalDeclarations(bool flag)
526 : : {
527 : 133 : d_globalDeclarations = flag;
528 : 133 : }
529 : :
530 : 7968 : bool SymManager::getGlobalDeclarations() const { return d_globalDeclarations; }
531 : :
532 : 6 : void SymManager::setFreshDeclarations(bool flag) { d_freshDeclarations = flag; }
533 : 343629 : bool SymManager::getFreshDeclarations() const { return d_freshDeclarations; }
534 : :
535 : 11 : void SymManager::setTermSortOverload(bool flag) { d_termSortOverload = flag; }
536 : 0 : bool SymManager::getTermSortOverload() const { return d_termSortOverload; }
537 : :
538 : 89 : void SymManager::setLastSynthName(const std::string& name)
539 : : {
540 : 89 : d_implementation->setLastSynthName(name);
541 : 89 : }
542 : :
543 : 13 : const std::string& SymManager::getLastSynthName() const
544 : : {
545 : 13 : return d_implementation->getLastSynthName();
546 : : }
547 : :
548 : 83 : void SymManager::reset() { d_implementation->reset(); }
549 : :
550 : 36 : void SymManager::resetAssertions()
551 : : {
552 : 36 : d_implementation->resetAssertions();
553 [ + + ]: 36 : if (!d_globalDeclarations)
554 : : {
555 : 13 : d_implementation->getSymbolTable().resetAssertions();
556 : : }
557 : 36 : }
558 : :
559 : 24132 : void SymManager::setLogic(const std::string& logic, bool isForced)
560 : : {
561 : : // if already forced and this isn't forced, ignore
562 [ + + ][ - + ]: 24132 : if (!d_logicIsForced || isForced)
563 : : {
564 : 24128 : d_logicIsForced = isForced;
565 : 24128 : d_logic = logic;
566 : : }
567 : 24132 : d_logicIsSet = true;
568 : 24132 : }
569 : 24126 : bool SymManager::isLogicForced() const { return d_logicIsForced; }
570 : :
571 : 48609 : bool SymManager::isLogicSet() const { return d_logicIsSet; }
572 : :
573 : 165 : const std::string& SymManager::getLogic() const { return d_logic; }
574 : :
575 : : } // namespace cvc5::parser
|
