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-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 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 : 27082 : Implementation()
41 : 27082 : : 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 : 27082 : d_lastSynthName(&d_context)
49 : : {
50 : : // use an outermost push, to be able to clear all definitions
51 : 27082 : d_context.push();
52 : 27082 : }
53 : :
54 : 27033 : ~Implementation() { d_context.pop(); }
55 : 420379 : 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 : 4423 : SymManager::Implementation::getExpressionNames(bool areAssertions) const
186 : : {
187 : 4423 : std::map<cvc5::Term, std::string> emap;
188 : 8179 : for (TermStringMap::const_iterator it = d_names.begin(),
189 : 4423 : itend = d_names.end();
190 [ + + ]: 8179 : 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 : 4423 : 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 : 12100 : void SymManager::Implementation::addModelDeclarationSort(cvc5::Sort s)
224 : : {
225 [ + - ]: 24200 : Trace("sym-manager") << "SymManager: addModelDeclarationSort " << s
226 : 12100 : << std::endl;
227 : 12100 : d_declareSorts.push_back(s);
228 : 12100 : }
229 : :
230 : 344268 : void SymManager::Implementation::addModelDeclarationTerm(cvc5::Term t)
231 : : {
232 [ + - ]: 688536 : Trace("sym-manager") << "SymManager: addModelDeclarationTerm " << t
233 : 344268 : << std::endl;
234 : 344268 : d_declareTerms.push_back(t);
235 : 344268 : }
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 : 369450 : void SymManager::Implementation::pushScope(bool isUserContext)
245 : : {
246 [ + - ]: 738900 : Trace("sym-manager") << "SymManager: pushScope, isUserContext = "
247 : 369450 : << isUserContext << std::endl;
248 [ + + ][ - + ]: 369450 : Assert(!d_hasPushedScope.get() || !isUserContext)
[ - + ][ - - ]
249 : 0 : << "cannot push a user context within a scope context";
250 : 369450 : d_context.push();
251 [ + + ]: 369450 : if (!isUserContext)
252 : : {
253 : 340083 : d_hasPushedScope = true;
254 : : }
255 : 369450 : d_symtabAllocated.pushScope();
256 : 369450 : }
257 : :
258 : 345439 : void SymManager::Implementation::popScope()
259 : : {
260 [ + - ]: 345439 : Trace("sym-manager") << "SymManager: popScope" << std::endl;
261 : 345439 : d_symtabAllocated.popScope();
262 [ - + ]: 345439 : if (d_context.getLevel() == 0)
263 : : {
264 : 0 : throw ScopeException();
265 : : }
266 : 345439 : d_context.pop();
267 [ + - ]: 690878 : Trace("sym-manager-debug")
268 : 345439 : << "d_hasPushedScope is now " << d_hasPushedScope.get() << std::endl;
269 : 345439 : }
270 : :
271 : 175 : bool SymManager::Implementation::hasPushedScope() const
272 : : {
273 : 175 : return d_hasPushedScope.get();
274 : : }
275 : :
276 : 86 : void SymManager::Implementation::setLastSynthName(const std::string& name)
277 : : {
278 : 86 : d_lastSynthName = name;
279 : 86 : }
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 : 27082 : SymManager::SymManager(cvc5::TermManager& tm)
313 : : : d_tm(tm),
314 : 27082 : d_implementation(new SymManager::Implementation()),
315 : : d_globalDeclarations(false),
316 : : d_freshDeclarations(true),
317 : : d_logicIsForced(false),
318 : : d_logicIsSet(false),
319 : 54164 : d_logic()
320 : : {
321 : 27082 : }
322 : :
323 : 27033 : SymManager::~SymManager() {}
324 : :
325 : 23248 : SymbolTable* SymManager::getSymbolTable()
326 : : {
327 : 23248 : return &d_implementation->getSymbolTable();
328 : : }
329 : :
330 : 379518 : bool SymManager::bind(const std::string& name, cvc5::Term obj, bool doOverload)
331 : : {
332 : 379518 : return d_implementation->getSymbolTable().bind(name, obj, doOverload);
333 : : }
334 : :
335 : 4430 : void SymManager::bindType(const std::string& name, cvc5::Sort t)
336 : : {
337 : 4430 : return d_implementation->getSymbolTable().bindType(name, t);
338 : : }
339 : :
340 : 3525 : bool SymManager::bindMutualDatatypeTypes(
341 : : const std::vector<cvc5::Sort>& datatypes, bool bindTesters)
342 : : {
343 [ + + ]: 8131 : for (size_t i = 0, ntypes = datatypes.size(); i < ntypes; ++i)
344 : : {
345 : 4606 : Sort t = datatypes[i];
346 : 4606 : const Datatype& dt = t.getDatatype();
347 : 4606 : const std::string& name = dt.getName();
348 [ + - ]: 4606 : Trace("parser-idt") << "define " << name << " as " << t << std::endl;
349 [ + + ]: 4606 : if (dt.isParametric())
350 : : {
351 : 176 : std::vector<Sort> paramTypes = dt.getParameters();
352 : 176 : bindType(name, paramTypes, t);
353 : : }
354 : : else
355 : : {
356 : 4430 : bindType(name, t);
357 : : }
358 [ + + ]: 12880 : for (size_t j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
359 : : {
360 : 8274 : const DatatypeConstructor& ctor = dt[j];
361 : 8274 : Term constructor = ctor.getTerm();
362 [ + - ]: 8274 : Trace("parser-idt") << "+ define " << constructor << std::endl;
363 : 8274 : std::string constructorName = ctor.getName();
364 : : // A zero argument constructor is actually APPLY_CONSTRUCTOR for the
365 : : // constructor.
366 [ + + ]: 8274 : if (ctor.getNumSelectors() == 0)
367 : : {
368 : 7190 : constructor = d_tm.mkTerm(Kind::APPLY_CONSTRUCTOR, {constructor});
369 : : }
370 : : // always do overloading
371 [ - + ]: 8274 : if (!bind(constructorName, constructor, true))
372 : : {
373 : 0 : return false;
374 : : }
375 [ + - ]: 8274 : if (bindTesters)
376 : : {
377 : 8274 : std::stringstream testerName;
378 : 8274 : testerName << "is-" << constructorName;
379 : 8274 : Term tester = ctor.getTesterTerm();
380 [ + - ][ - + ]: 8274 : Trace("parser-idt") << "+ define " << testerName.str() << std::endl;
[ - - ]
381 : : // always do overloading
382 [ - + ]: 8274 : if (!bind(testerName.str(), tester, true))
383 : : {
384 : 0 : return false;
385 : : }
386 : : }
387 [ + + ]: 16140 : for (size_t k = 0, nargs = ctor.getNumSelectors(); k < nargs; k++)
388 : : {
389 : 7866 : const DatatypeSelector& sel = ctor[k];
390 : 7866 : Term selector = sel.getTerm();
391 [ + - ]: 7866 : Trace("parser-idt") << "+++ define " << selector << std::endl;
392 : 7866 : std::string selectorName = sel.getName();
393 : : // always do overloading
394 [ - + ]: 7866 : if (!bind(selectorName, selector, true))
395 : : {
396 : 0 : return false;
397 : : }
398 : : }
399 : : }
400 : : }
401 : 3525 : return true;
402 : : }
403 : :
404 : 13153 : void SymManager::bindType(const std::string& name,
405 : : const std::vector<cvc5::Sort>& params,
406 : : cvc5::Sort t)
407 : : {
408 : 13153 : return d_implementation->getSymbolTable().bindType(name, params, t);
409 : : }
410 : :
411 : 25592 : NamingResult SymManager::setExpressionName(cvc5::Term t,
412 : : const std::string& name,
413 : : bool isAssertion)
414 : : {
415 : 25592 : return d_implementation->setExpressionName(t, name, isAssertion);
416 : : }
417 : :
418 : 26 : bool SymManager::getExpressionName(cvc5::Term t,
419 : : std::string& name,
420 : : bool isAssertion) const
421 : : {
422 : 26 : return d_implementation->getExpressionName(t, name, isAssertion);
423 : : }
424 : :
425 : 33 : void SymManager::getExpressionNames(const std::vector<cvc5::Term>& ts,
426 : : std::vector<std::string>& names,
427 : : bool areAssertions) const
428 : : {
429 : 33 : return d_implementation->getExpressionNames(ts, names, areAssertions);
430 : : }
431 : :
432 : 4423 : std::map<cvc5::Term, std::string> SymManager::getExpressionNames(
433 : : bool areAssertions) const
434 : : {
435 : 4423 : return d_implementation->getExpressionNames(areAssertions);
436 : : }
437 : 163 : std::vector<cvc5::Sort> SymManager::getDeclaredSorts() const
438 : : {
439 : 163 : return d_implementation->getDeclaredSorts();
440 : : }
441 : 65 : std::vector<cvc5::Term> SymManager::getDeclaredTerms() const
442 : : {
443 : 65 : return d_implementation->getDeclaredTerms();
444 : : }
445 : :
446 : 20 : std::vector<cvc5::Term> SymManager::getFunctionsToSynthesize() const
447 : : {
448 : 20 : return d_implementation->getFunctionsToSynthesize();
449 : : }
450 : :
451 : 12100 : void SymManager::addModelDeclarationSort(cvc5::Sort s)
452 : : {
453 : 12100 : d_implementation->addModelDeclarationSort(s);
454 : 12100 : }
455 : :
456 : 344268 : void SymManager::addModelDeclarationTerm(cvc5::Term t)
457 : : {
458 : 344268 : d_implementation->addModelDeclarationTerm(t);
459 : 344268 : }
460 : :
461 : 1593 : void SymManager::addFunctionToSynthesize(cvc5::Term f)
462 : : {
463 : 1593 : d_implementation->addFunctionToSynthesize(f);
464 : 1593 : }
465 : :
466 : 16 : size_t SymManager::scopeLevel() const
467 : : {
468 : 16 : return d_implementation->getSymbolTable().getLevel();
469 : : }
470 : :
471 : 369557 : void SymManager::pushScope(bool isUserContext)
472 : : {
473 : : // we do not push user contexts when global declarations is true. This
474 : : // policy applies both to the symbol table and to the symbol manager.
475 [ + + ][ + + ]: 369557 : if (d_globalDeclarations && isUserContext)
476 : : {
477 : 107 : return;
478 : : }
479 : 369450 : d_implementation->pushScope(isUserContext);
480 : : }
481 : :
482 : 345459 : void SymManager::popScope()
483 : : {
484 : : // If global declarations is true, then if d_hasPushedScope is false, then
485 : : // the pop corresponds to a user context, which we did not push. Note this
486 : : // additionally relies on the fact that user contexts cannot be pushed
487 : : // within scope contexts. Hence, since we did not push the context, we
488 : : // do not pop a context here.
489 [ + + ][ + + ]: 345459 : if (d_globalDeclarations && !d_implementation->hasPushedScope())
[ + + ]
490 : : {
491 : 20 : return;
492 : : }
493 : 345439 : d_implementation->popScope();
494 : : }
495 : :
496 : 129 : void SymManager::setGlobalDeclarations(bool flag)
497 : : {
498 : 129 : d_globalDeclarations = flag;
499 : 129 : }
500 : :
501 : 7641 : bool SymManager::getGlobalDeclarations() const { return d_globalDeclarations; }
502 : :
503 : 6 : void SymManager::setFreshDeclarations(bool flag) { d_freshDeclarations = flag; }
504 : 356460 : bool SymManager::getFreshDeclarations() const { return d_freshDeclarations; }
505 : :
506 : 86 : void SymManager::setLastSynthName(const std::string& name)
507 : : {
508 : 86 : d_implementation->setLastSynthName(name);
509 : 86 : }
510 : :
511 : 13 : const std::string& SymManager::getLastSynthName() const
512 : : {
513 : 13 : return d_implementation->getLastSynthName();
514 : : }
515 : :
516 : 92 : void SymManager::reset() { d_implementation->reset(); }
517 : :
518 : 42 : void SymManager::resetAssertions()
519 : : {
520 : 42 : d_implementation->resetAssertions();
521 [ + + ]: 42 : if (!d_globalDeclarations)
522 : : {
523 : 14 : d_implementation->getSymbolTable().resetAssertions();
524 : : }
525 : 42 : }
526 : :
527 : 23081 : void SymManager::setLogic(const std::string& logic, bool isForced)
528 : : {
529 : : // if already forced and this isn't forced, ignore
530 [ + + ][ - + ]: 23081 : if (!d_logicIsForced || isForced)
531 : : {
532 : 23077 : d_logicIsForced = isForced;
533 : 23077 : d_logic = logic;
534 : : }
535 : 23081 : d_logicIsSet = true;
536 : 23081 : }
537 : 23075 : bool SymManager::isLogicForced() const { return d_logicIsForced; }
538 : :
539 : 46498 : bool SymManager::isLogicSet() const { return d_logicIsSet; }
540 : :
541 : 165 : const std::string& SymManager::getLogic() const { return d_logic; }
542 : :
543 : : } // namespace cvc5::parser
|
