Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/symbol_manager.cpp	Lines:	132	137	96.4 %
Date:	2021-05-21	Branches:	117	216	54.2 %


/******************************************************************************
 * 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_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;
  /** 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);
  /** 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;
  /**
   * 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;
}

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::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();
}

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

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

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