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