Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/symbol_manager.cpp	Lines:	144	149	96.6 %
Date:	2021-09-29	Branches:	127	236	53.8 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Aina Niemetz
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * The symbol manager.
 */

#include "expr/symbol_manager.h"

#include "context/cdhashmap.h"
#include "context/cdhashset.h"
#include "context/cdlist.h"
#include "context/cdo.h"

using namespace cvc5::context;

namespace cvc5 {

// ---------------------------------------------- SymbolManager::Implementation

class SymbolManager::Implementation
{
  using TermStringMap = CDHashMap<api::Term, std::string, std::hash<api::Term>>;
  using TermSet = CDHashSet<api::Term, std::hash<api::Term>>;
  using SortList = CDList<api::Sort>;
  using TermList = CDList<api::Term>;

 public:
  Implementation()
      : d_context(),
        d_names(&d_context),
        d_namedAsserts(&d_context),
        d_declareSorts(&d_context),
        d_declareTerms(&d_context),
        d_funToSynth(&d_context),
        d_hasPushedScope(&d_context, false)
  {
    // use an outermost push, to be able to clear all definitions
    d_context.push();
  }

  ~Implementation() { d_context.pop(); }
  /** set expression name */
  NamingResult setExpressionName(api::Term t,
                                 const std::string& name,
                                 bool isAssertion = false);
  /** get expression name */
  bool getExpressionName(api::Term t,
                         std::string& name,
                         bool isAssertion = false) const;
  /** get expression names */
  void getExpressionNames(const std::vector<api::Term>& ts,
                          std::vector<std::string>& names,
                          bool areAssertions = false) const;
  /** get expression names */
  std::map<api::Term, std::string> getExpressionNames(bool areAssertions) const;
  /** get model declare sorts */
  std::vector<api::Sort> getModelDeclareSorts() const;
  /** get model declare terms */
  std::vector<api::Term> getModelDeclareTerms() const;
  /** get functions to synthesize */
  std::vector<api::Term> getFunctionsToSynthesize() const;
  /** Add declared sort to the list of model declarations. */
  void addModelDeclarationSort(api::Sort s);
  /** Add declared term to the list of model declarations. */
  void addModelDeclarationTerm(api::Term t);
  /** Add function to the list of functions to synthesize. */
  void addFunctionToSynthesize(api::Term t);
  /** reset */
  void reset();
  /** reset assertions */
  void resetAssertions();
  /** Push a scope in the expression names. */
  void pushScope(bool isUserContext);
  /** Pop a scope in the expression names. */
  void popScope();
  /** Have we pushed a scope (e.g. let or quantifier) in the current context? */
  bool hasPushedScope() const;

 private:
  /** The context manager for the scope maps. */
  Context d_context;
  /** Map terms to names */
  TermStringMap d_names;
  /** The set of terms with assertion names */
  TermSet d_namedAsserts;
  /** Declared sorts (for model printing) */
  SortList d_declareSorts;
  /** Declared terms (for model printing) */
  TermList d_declareTerms;
  /** Functions to synthesize (for response to check-synth) */
  TermList d_funToSynth;
  /**
   * Have we pushed a scope (e.g. a let or quantifier) in the current context?
   */
  CDO<bool> d_hasPushedScope;
};

NamingResult SymbolManager::Implementation::setExpressionName(
    api::Term t, const std::string& name, bool isAssertion)
{
  Trace("sym-manager") << "SymbolManager: set expression name: " << t << " -> "
                       << name << ", isAssertion=" << isAssertion << std::endl;
  if (d_hasPushedScope.get())
  {
    // cannot name subexpressions under binders
    return NamingResult::ERROR_IN_BINDER;
  }

  if (isAssertion)
  {
    d_namedAsserts.insert(t);
  }
  if (d_names.find(t) != d_names.end())
  {
    // already named assertion
    return NamingResult::ERROR_ALREADY_NAMED;
  }
  d_names[t] = name;
  return NamingResult::SUCCESS;
}

bool SymbolManager::Implementation::getExpressionName(api::Term t,
                                                      std::string& name,
                                                      bool isAssertion) const
{
  TermStringMap::const_iterator it = d_names.find(t);
  if (it == d_names.end())
  {
    return false;
  }
  if (isAssertion)
  {
    // must be an assertion name
    if (d_namedAsserts.find(t) == d_namedAsserts.end())
    {
      return false;
    }
  }
  name = (*it).second;
  return true;
}

void SymbolManager::Implementation::getExpressionNames(
    const std::vector<api::Term>& ts,
    std::vector<std::string>& names,
    bool areAssertions) const
{
  for (const api::Term& t : ts)
  {
    std::string name;
    if (getExpressionName(t, name, areAssertions))
    {
      names.push_back(name);
    }
  }
}

std::map<api::Term, std::string>
SymbolManager::Implementation::getExpressionNames(bool areAssertions) const
{
  std::map<api::Term, std::string> emap;
  for (TermStringMap::const_iterator it = d_names.begin(),
                                     itend = d_names.end();
       it != itend;
       ++it)
  {
    api::Term t = (*it).first;
    if (areAssertions && d_namedAsserts.find(t) == d_namedAsserts.end())
    {
      continue;
    }
    emap[t] = (*it).second;
  }
  return emap;
}

std::vector<api::Sort> SymbolManager::Implementation::getModelDeclareSorts()
    const
{
  std::vector<api::Sort> declareSorts(d_declareSorts.begin(),
                                      d_declareSorts.end());
  return declareSorts;
}

std::vector<api::Term> SymbolManager::Implementation::getModelDeclareTerms()
    const
{
  std::vector<api::Term> declareTerms(d_declareTerms.begin(),
                                      d_declareTerms.end());
  return declareTerms;
}

std::vector<api::Term> SymbolManager::Implementation::getFunctionsToSynthesize()
    const
{
  return std::vector<api::Term>(d_funToSynth.begin(), d_funToSynth.end());
}

void SymbolManager::Implementation::addModelDeclarationSort(api::Sort s)
{
  Trace("sym-manager") << "SymbolManager: addModelDeclarationSort " << s
                       << std::endl;
  d_declareSorts.push_back(s);
}

void SymbolManager::Implementation::addModelDeclarationTerm(api::Term t)
{
  Trace("sym-manager") << "SymbolManager: addModelDeclarationTerm " << t
                       << std::endl;
  d_declareTerms.push_back(t);
}

void SymbolManager::Implementation::addFunctionToSynthesize(api::Term f)
{
  Trace("sym-manager") << "SymbolManager: addFunctionToSynthesize " << f
                       << std::endl;
  d_funToSynth.push_back(f);
}

void SymbolManager::Implementation::pushScope(bool isUserContext)
{
  Trace("sym-manager") << "SymbolManager: pushScope, isUserContext = "
                       << isUserContext << std::endl;
  PrettyCheckArgument(!d_hasPushedScope.get() || !isUserContext,
                      "cannot push a user context within a scope context");
  d_context.push();
  if (!isUserContext)
  {
    d_hasPushedScope = true;
  }
}

void SymbolManager::Implementation::popScope()
{
  Trace("sym-manager") << "SymbolManager: popScope" << std::endl;
  if (d_context.getLevel() == 0)
  {
    throw ScopeException();
  }
  d_context.pop();
  Trace("sym-manager-debug")
      << "d_hasPushedScope is now " << d_hasPushedScope.get() << std::endl;
}

bool SymbolManager::Implementation::hasPushedScope() const
{
  return d_hasPushedScope.get();
}

void SymbolManager::Implementation::reset()
{
  Trace("sym-manager") << "SymbolManager: reset" << std::endl;
  // clear names by popping to context level 0
  while (d_context.getLevel() > 0)
  {
    d_context.pop();
  }
  // push the outermost context
  d_context.push();
}

void SymbolManager::Implementation::resetAssertions()
{
  Trace("sym-manager") << "SymbolManager: resetAssertions" << std::endl;
  // clear names by popping to context level 1
  while (d_context.getLevel() > 1)
  {
    d_context.pop();
  }
}

// ---------------------------------------------- SymbolManager

SymbolManager::SymbolManager(api::Solver* s)
    : d_solver(s),
      d_implementation(new SymbolManager::Implementation()),
      d_globalDeclarations(false)
{
}

SymbolManager::~SymbolManager() {}

SymbolTable* SymbolManager::getSymbolTable() { return &d_symtabAllocated; }

NamingResult SymbolManager::setExpressionName(api::Term t,
                                              const std::string& name,
                                              bool isAssertion)
{
  return d_implementation->setExpressionName(t, name, isAssertion);
}

bool SymbolManager::getExpressionName(api::Term t,
                                      std::string& name,
                                      bool isAssertion) const
{
  return d_implementation->getExpressionName(t, name, isAssertion);
}

void SymbolManager::getExpressionNames(const std::vector<api::Term>& ts,
                                       std::vector<std::string>& names,
                                       bool areAssertions) const
{
  return d_implementation->getExpressionNames(ts, names, areAssertions);
}

std::map<api::Term, std::string> SymbolManager::getExpressionNames(
    bool areAssertions) const
{
  return d_implementation->getExpressionNames(areAssertions);
}
std::vector<api::Sort> SymbolManager::getModelDeclareSorts() const
{
  return d_implementation->getModelDeclareSorts();
}
std::vector<api::Term> SymbolManager::getModelDeclareTerms() const
{
  return d_implementation->getModelDeclareTerms();
}

std::vector<api::Term> SymbolManager::getFunctionsToSynthesize() const
{
  return d_implementation->getFunctionsToSynthesize();
}

void SymbolManager::addModelDeclarationSort(api::Sort s)
{
  d_implementation->addModelDeclarationSort(s);
}

void SymbolManager::addModelDeclarationTerm(api::Term t)
{
  d_implementation->addModelDeclarationTerm(t);
}

void SymbolManager::addFunctionToSynthesize(api::Term f)
{
  d_implementation->addFunctionToSynthesize(f);
}

size_t SymbolManager::scopeLevel() const
{
  return d_symtabAllocated.getLevel();
}

void SymbolManager::pushScope(bool isUserContext)
{
  // we do not push user contexts when global declarations is true. This
  // policy applies both to the symbol table and to the symbol manager.
  if (d_globalDeclarations && isUserContext)
  {
    return;
  }
  d_implementation->pushScope(isUserContext);
  d_symtabAllocated.pushScope();
}

void SymbolManager::popScope()
{
  // If global declarations is true, then if d_hasPushedScope is false, then
  // the pop corresponds to a user context, which we did not push. Note this
  // additionally relies on the fact that user contexts cannot be pushed
  // within scope contexts. Hence, since we did not push the context, we
  // do not pop a context here.
  if (d_globalDeclarations && !d_implementation->hasPushedScope())
  {
    return;
  }
  d_symtabAllocated.popScope();
  d_implementation->popScope();
}

void SymbolManager::setGlobalDeclarations(bool flag)
{
  d_globalDeclarations = flag;
}

bool SymbolManager::getGlobalDeclarations() const
{
  return d_globalDeclarations;
}

void SymbolManager::reset()
{
  d_symtabAllocated.reset();
  d_implementation->reset();
}

void SymbolManager::resetAssertions()
{
  d_implementation->resetAssertions();
  d_symtabAllocated.resetAssertions();
}

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Aina Niemetz
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 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 "expr/symbol_manager.h"
17
18		#include "context/cdhashmap.h"
19		#include "context/cdhashset.h"
20		#include "context/cdlist.h"
21		#include "context/cdo.h"
22
23		using namespace cvc5::context;
24
25		namespace cvc5 {
26
27		// ---------------------------------------------- SymbolManager::Implementation
28
29		class SymbolManager::Implementation
30		{
31		using TermStringMap = CDHashMap<api::Term, std::string, std::hash<api::Term>>;
32		using TermSet = CDHashSet<api::Term, std::hash<api::Term>>;
33		using SortList = CDList<api::Sort>;
34		using TermList = CDList<api::Term>;
35
36		public:
37	6680	Implementation()
38	6680	: d_context(),
39		d_names(&d_context),
40		d_namedAsserts(&d_context),
41		d_declareSorts(&d_context),
42		d_declareTerms(&d_context),
43		d_funToSynth(&d_context),
44	6680	d_hasPushedScope(&d_context, false)
45		{
46		// use an outermost push, to be able to clear all definitions
47	6680	d_context.push();
48	6680	}
49
50	6680	~Implementation() { d_context.pop(); }
51		/** set expression name */
52		NamingResult setExpressionName(api::Term t,
53		const std::string& name,
54		bool isAssertion = false);
55		/** get expression name */
56		bool getExpressionName(api::Term t,
57		std::string& name,
58		bool isAssertion = false) const;
59		/** get expression names */
60		void getExpressionNames(const std::vector<api::Term>& ts,
61		std::vector<std::string>& names,
62		bool areAssertions = false) const;
63		/** get expression names */
64		std::map<api::Term, std::string> getExpressionNames(bool areAssertions) const;
65		/** get model declare sorts */
66		std::vector<api::Sort> getModelDeclareSorts() const;
67		/** get model declare terms */
68		std::vector<api::Term> getModelDeclareTerms() const;
69		/** get functions to synthesize */
70		std::vector<api::Term> getFunctionsToSynthesize() const;
71		/** Add declared sort to the list of model declarations. */
72		void addModelDeclarationSort(api::Sort s);
73		/** Add declared term to the list of model declarations. */
74		void addModelDeclarationTerm(api::Term t);
75		/** Add function to the list of functions to synthesize. */
76		void addFunctionToSynthesize(api::Term t);
77		/** reset */
78		void reset();
79		/** reset assertions */
80		void resetAssertions();
81		/** Push a scope in the expression names. */
82		void pushScope(bool isUserContext);
83		/** Pop a scope in the expression names. */
84		void popScope();
85		/** Have we pushed a scope (e.g. let or quantifier) in the current context? */
86		bool hasPushedScope() const;
87
88		private:
89		/** The context manager for the scope maps. */
90		Context d_context;
91		/** Map terms to names */
92		TermStringMap d_names;
93		/** The set of terms with assertion names */
94		TermSet d_namedAsserts;
95		/** Declared sorts (for model printing) */
96		SortList d_declareSorts;
97		/** Declared terms (for model printing) */
98		TermList d_declareTerms;
99		/** Functions to synthesize (for response to check-synth) */
100		TermList d_funToSynth;
101		/**
102		* Have we pushed a scope (e.g. a let or quantifier) in the current context?
103		*/
104		CDO<bool> d_hasPushedScope;
105		};
106
107	4486	NamingResult SymbolManager::Implementation::setExpressionName(
108		api::Term t, const std::string& name, bool isAssertion)
109		{
110	8972	Trace("sym-manager") << "SymbolManager: set expression name: " << t << " -> "
111	4486	<< name << ", isAssertion=" << isAssertion << std::endl;
112	4486	if (d_hasPushedScope.get())
113		{
114		// cannot name subexpressions under binders
115	1	return NamingResult::ERROR_IN_BINDER;
116		}
117
118	4485	if (isAssertion)
119		{
120	2885	d_namedAsserts.insert(t);
121		}
122	4485	if (d_names.find(t) != d_names.end())
123		{
124		// already named assertion
125	1618	return NamingResult::ERROR_ALREADY_NAMED;
126		}
127	2867	d_names[t] = name;
128	2867	return NamingResult::SUCCESS;
129		}
130
131	9	bool SymbolManager::Implementation::getExpressionName(api::Term t,
132		std::string& name,
133		bool isAssertion) const
134		{
135	9	TermStringMap::const_iterator it = d_names.find(t);
136	9	if (it == d_names.end())
137		{
138	2	return false;
139		}
140	7	if (isAssertion)
141		{
142		// must be an assertion name
143	7	if (d_namedAsserts.find(t) == d_namedAsserts.end())
144		{
145		return false;
146		}
147		}
148	7	name = (*it).second;
149	7	return true;
150		}
151
152	4	void SymbolManager::Implementation::getExpressionNames(
153		const std::vector<api::Term>& ts,
154		std::vector<std::string>& names,
155		bool areAssertions) const
156		{
157	13	for (const api::Term& t : ts)
158		{
159	18	std::string name;
160	9	if (getExpressionName(t, name, areAssertions))
161		{
162	7	names.push_back(name);
163		}
164		}
165	4	}
166
167		std::map<api::Term, std::string>
168	10	SymbolManager::Implementation::getExpressionNames(bool areAssertions) const
169		{
170	10	std::map<api::Term, std::string> emap;
171	22	for (TermStringMap::const_iterator it = d_names.begin(),
172	10	itend = d_names.end();
173	22	it != itend;
174		++it)
175		{
176	24	api::Term t = (*it).first;
177	12	if (areAssertions && d_namedAsserts.find(t) == d_namedAsserts.end())
178		{
179		continue;
180		}
181	12	emap[t] = (*it).second;
182		}
183	10	return emap;
184		}
185
186	29	std::vector<api::Sort> SymbolManager::Implementation::getModelDeclareSorts()
187		const
188		{
189		std::vector<api::Sort> declareSorts(d_declareSorts.begin(),
190	29	d_declareSorts.end());
191	29	return declareSorts;
192		}
193
194	29	std::vector<api::Term> SymbolManager::Implementation::getModelDeclareTerms()
195		const
196		{
197		std::vector<api::Term> declareTerms(d_declareTerms.begin(),
198	29	d_declareTerms.end());
199	29	return declareTerms;
200		}
201
202	3	std::vector<api::Term> SymbolManager::Implementation::getFunctionsToSynthesize()
203		const
204		{
205	3	return std::vector<api::Term>(d_funToSynth.begin(), d_funToSynth.end());
206		}
207
208	1646	void SymbolManager::Implementation::addModelDeclarationSort(api::Sort s)
209		{
210	3292	Trace("sym-manager") << "SymbolManager: addModelDeclarationSort " << s
211	1646	<< std::endl;
212	1646	d_declareSorts.push_back(s);
213	1646	}
214
215	134166	void SymbolManager::Implementation::addModelDeclarationTerm(api::Term t)
216		{
217	268332	Trace("sym-manager") << "SymbolManager: addModelDeclarationTerm " << t
218	134166	<< std::endl;
219	134166	d_declareTerms.push_back(t);
220	134166	}
221
222	348	void SymbolManager::Implementation::addFunctionToSynthesize(api::Term f)
223		{
224	696	Trace("sym-manager") << "SymbolManager: addFunctionToSynthesize " << f
225	348	<< std::endl;
226	348	d_funToSynth.push_back(f);
227	348	}
228
229	54723	void SymbolManager::Implementation::pushScope(bool isUserContext)
230		{
231	109446	Trace("sym-manager") << "SymbolManager: pushScope, isUserContext = "
232	54723	<< isUserContext << std::endl;
233	54723	PrettyCheckArgument(!d_hasPushedScope.get() \|\| !isUserContext,
234		"cannot push a user context within a scope context");
235	54723	d_context.push();
236	54723	if (!isUserContext)
237		{
238	52856	d_hasPushedScope = true;
239		}
240	54723	}
241
242	54386	void SymbolManager::Implementation::popScope()
243		{
244	54386	Trace("sym-manager") << "SymbolManager: popScope" << std::endl;
245	54386	if (d_context.getLevel() == 0)
246		{
247		throw ScopeException();
248		}
249	54386	d_context.pop();
250	108772	Trace("sym-manager-debug")
251	54386	<< "d_hasPushedScope is now " << d_hasPushedScope.get() << std::endl;
252	54386	}
253
254	16	bool SymbolManager::Implementation::hasPushedScope() const
255		{
256	16	return d_hasPushedScope.get();
257		}
258
259	25	void SymbolManager::Implementation::reset()
260		{
261	25	Trace("sym-manager") << "SymbolManager: reset" << std::endl;
262		// clear names by popping to context level 0
263	75	while (d_context.getLevel() > 0)
264		{
265	25	d_context.pop();
266		}
267		// push the outermost context
268	25	d_context.push();
269	25	}
270
271	24	void SymbolManager::Implementation::resetAssertions()
272		{
273	24	Trace("sym-manager") << "SymbolManager: resetAssertions" << std::endl;
274		// clear names by popping to context level 1
275	36	while (d_context.getLevel() > 1)
276		{
277	6	d_context.pop();
278		}
279	24	}
280
281		// ---------------------------------------------- SymbolManager
282
283	6680	SymbolManager::SymbolManager(api::Solver* s)
284		: d_solver(s),
285	6680	d_implementation(new SymbolManager::Implementation()),
286	13360	d_globalDeclarations(false)
287		{
288	6680	}
289
290	6680	SymbolManager::~SymbolManager() {}
291
292	4052	SymbolTable* SymbolManager::getSymbolTable() { return &d_symtabAllocated; }
293
294	4486	NamingResult SymbolManager::setExpressionName(api::Term t,
295		const std::string& name,
296		bool isAssertion)
297		{
298	4486	return d_implementation->setExpressionName(t, name, isAssertion);
299		}
300
301		bool SymbolManager::getExpressionName(api::Term t,
302		std::string& name,
303		bool isAssertion) const
304		{
305		return d_implementation->getExpressionName(t, name, isAssertion);
306		}
307
308	4	void SymbolManager::getExpressionNames(const std::vector<api::Term>& ts,
309		std::vector<std::string>& names,
310		bool areAssertions) const
311		{
312	4	return d_implementation->getExpressionNames(ts, names, areAssertions);
313		}
314
315	10	std::map<api::Term, std::string> SymbolManager::getExpressionNames(
316		bool areAssertions) const
317		{
318	10	return d_implementation->getExpressionNames(areAssertions);
319		}
320	29	std::vector<api::Sort> SymbolManager::getModelDeclareSorts() const
321		{
322	29	return d_implementation->getModelDeclareSorts();
323		}
324	29	std::vector<api::Term> SymbolManager::getModelDeclareTerms() const
325		{
326	29	return d_implementation->getModelDeclareTerms();
327		}
328
329	3	std::vector<api::Term> SymbolManager::getFunctionsToSynthesize() const
330		{
331	3	return d_implementation->getFunctionsToSynthesize();
332		}
333
334	1646	void SymbolManager::addModelDeclarationSort(api::Sort s)
335		{
336	1646	d_implementation->addModelDeclarationSort(s);
337	1646	}
338
339	134166	void SymbolManager::addModelDeclarationTerm(api::Term t)
340		{
341	134166	d_implementation->addModelDeclarationTerm(t);
342	134166	}
343
344	348	void SymbolManager::addFunctionToSynthesize(api::Term f)
345		{
346	348	d_implementation->addFunctionToSynthesize(f);
347	348	}
348
349	1381	size_t SymbolManager::scopeLevel() const
350		{
351	1381	return d_symtabAllocated.getLevel();
352		}
353
354	54728	void SymbolManager::pushScope(bool isUserContext)
355		{
356		// we do not push user contexts when global declarations is true. This
357		// policy applies both to the symbol table and to the symbol manager.
358	54728	if (d_globalDeclarations && isUserContext)
359		{
360	5	return;
361		}
362	54723	d_implementation->pushScope(isUserContext);
363	54723	d_symtabAllocated.pushScope();
364		}
365
366	54389	void SymbolManager::popScope()
367		{
368		// If global declarations is true, then if d_hasPushedScope is false, then
369		// the pop corresponds to a user context, which we did not push. Note this
370		// additionally relies on the fact that user contexts cannot be pushed
371		// within scope contexts. Hence, since we did not push the context, we
372		// do not pop a context here.
373	54389	if (d_globalDeclarations && !d_implementation->hasPushedScope())
374		{
375	3	return;
376		}
377	54386	d_symtabAllocated.popScope();
378	54386	d_implementation->popScope();
379		}
380
381	13	void SymbolManager::setGlobalDeclarations(bool flag)
382		{
383	13	d_globalDeclarations = flag;
384	13	}
385
386	140324	bool SymbolManager::getGlobalDeclarations() const
387		{
388	140324	return d_globalDeclarations;
389		}
390
391	25	void SymbolManager::reset()
392		{
393	25	d_symtabAllocated.reset();
394	25	d_implementation->reset();
395	25	}
396
397	24	void SymbolManager::resetAssertions()
398		{
399	24	d_implementation->resetAssertions();
400	24	d_symtabAllocated.resetAssertions();
401	24	}
402
403	22746	} // namespace cvc5