Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/term_registration_visitor.cpp	Lines:	115	142	81.0 %
Date:	2021-11-07	Branches:	235	570	41.2 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Dejan Jovanovic, Morgan Deters
 *
 * 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.
 * ****************************************************************************
 *
 * [[ Add lengthier description here ]]
 * \todo document this file
 */

#include "theory/term_registration_visitor.h"

#include "base/configuration.h"
#include "options/quantifiers_options.h"
#include "smt/logic_exception.h"
#include "theory/theory_engine.h"

using namespace cvc5::theory;

namespace cvc5 {

std::string PreRegisterVisitor::toString() const {
  std::stringstream ss;
  TNodeToTheorySetMap::const_iterator it = d_visited.begin();
  for (; it != d_visited.end(); ++ it) {
    ss << (*it).first << ": " << TheoryIdSetUtil::setToString((*it).second)
       << std::endl;
  }
  return ss.str();
}

/**
 * Return true if we already visited the term current with the given parent,
 * assuming that the set of theories in visitedTheories has already processed
 * current. This method is used by PreRegisterVisitor and SharedTermsVisitor
 * below.
 */
bool isAlreadyVisited(Env& env,
                      TheoryIdSet visitedTheories,
                      TNode current,
                      TNode parent)
{
  TheoryId currentTheoryId = Theory::theoryOf(current);
  if (!TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories))
  {
    // current theory not visited, return false
    return false;
  }

  if (current == parent)
  {
    // top-level and current visited, return true
    return true;
  }

  // The current theory has already visited it, so now it depends on the parent
  // and the type
  TheoryId parentTheoryId = Theory::theoryOf(parent);
  if (!TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories))
  {
    // parent theory not visited, return false
    return false;
  }

  // do we need to consider the type?
  TypeNode type = current.getType();
  if (currentTheoryId == parentTheoryId && !env.isFiniteType(type))
  {
    // current and parent are the same theory, and we are infinite, return true
    return true;
  }
  TheoryId typeTheoryId = Theory::theoryOf(type);
  return TheoryIdSetUtil::setContains(typeTheoryId, visitedTheories);
}

PreRegisterVisitor::PreRegisterVisitor(Env& env, TheoryEngine* engine)
    : EnvObj(env), d_engine(engine), d_visited(context())
{
}

bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {

  Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;

  if ((parent.isClosure()
       || parent.getKind() == kind::SEP_STAR
       || parent.getKind() == kind::SEP_WAND
       || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
       )
      && current != parent)
  {
    Debug("register::internal") << "quantifier:true" << std::endl;
    return true;
  }

  // Get the theories that have already visited this node
  TNodeToTheorySetMap::iterator find = d_visited.find(current);
  if (find == d_visited.end()) {
    // not visited at all, return false
    return false;
  }

  TheoryIdSet visitedTheories = (*find).second;
  return isAlreadyVisited(d_env, visitedTheories, current, parent);
}

void PreRegisterVisitor::visit(TNode current, TNode parent) {

  Debug("register") << "PreRegisterVisitor::visit(" << current << "," << parent << ")" << std::endl;
  if (Debug.isOn("register::internal")) {
    Debug("register::internal") << toString() << std::endl;
  }

  // get the theories we already preregistered with
  TheoryIdSet visitedTheories = d_visited[current];

  // call the preregistration on current, parent or type theories and update
  // visitedTheories. The set of preregistering theories coincides with
  // visitedTheories here.
  preRegister(
      d_env, d_engine, visitedTheories, current, parent, visitedTheories);

  Debug("register::internal")
      << "PreRegisterVisitor::visit(" << current << "," << parent
      << "): now registered with "
      << TheoryIdSetUtil::setToString(visitedTheories) << std::endl;
  // update the theories set for current
  d_visited[current] = visitedTheories;
  Assert(d_visited.find(current) != d_visited.end());
  Assert(alreadyVisited(current, parent));
}

void PreRegisterVisitor::preRegister(Env& env,
                                     TheoryEngine* te,
                                     TheoryIdSet& visitedTheories,
                                     TNode current,
                                     TNode parent,
                                     TheoryIdSet preregTheories)
{
  // Preregister with the current theory, if necessary
  TheoryId currentTheoryId = Theory::theoryOf(current);
  preRegisterWithTheory(
      te, visitedTheories, currentTheoryId, current, parent, preregTheories);

  if (current != parent)
  {
    // preregister with parent theory, if necessary
    TheoryId parentTheoryId = Theory::theoryOf(parent);
    preRegisterWithTheory(
        te, visitedTheories, parentTheoryId, current, parent, preregTheories);

    // Note that if enclosed by different theories it's shared, for example,
    // in read(a, f(a)), f(a) should be shared with integers.
    TypeNode type = current.getType();
    if (currentTheoryId != parentTheoryId || env.isFiniteType(type))
    {
      // preregister with the type's theory, if necessary
      TheoryId typeTheoryId = Theory::theoryOf(type);
      preRegisterWithTheory(
          te, visitedTheories, typeTheoryId, current, parent, preregTheories);
    }
  }
}
void PreRegisterVisitor::preRegisterWithTheory(TheoryEngine* te,
                                               TheoryIdSet& visitedTheories,
                                               TheoryId id,
                                               TNode current,
                                               TNode parent,
                                               TheoryIdSet preregTheories)
{
  if (TheoryIdSetUtil::setContains(id, visitedTheories))
  {
    // already visited
    return;
  }
  visitedTheories = TheoryIdSetUtil::setInsert(id, visitedTheories);
  if (TheoryIdSetUtil::setContains(id, preregTheories))
  {
    // already pregregistered
    return;
  }
  if (Configuration::isAssertionBuild())
  {
    Debug("register::internal")
        << "PreRegisterVisitor::visit(" << current << "," << parent
        << "): adding " << id << std::endl;
    // This should never throw an exception, since theories should be
    // guaranteed to be initialized.
    if (!te->isTheoryEnabled(id))
    {
      const LogicInfo& l = te->getLogicInfo();
      LogicInfo newLogicInfo = l.getUnlockedCopy();
      newLogicInfo.enableTheory(id);
      newLogicInfo.lock();
      std::stringstream ss;
      ss << "The logic was specified as " << l.getLogicString()
         << ", which doesn't include " << id
         << ", but found a term in that theory." << std::endl
         << "You might want to extend your logic to "
         << newLogicInfo.getLogicString() << std::endl;
      throw LogicException(ss.str());
    }
  }
  // call the theory's preRegisterTerm method
  Theory* th = te->theoryOf(id);
  th->preRegisterTerm(current);
}

void PreRegisterVisitor::start(TNode node) {}

SharedTermsVisitor::SharedTermsVisitor(Env& env,
                                       TheoryEngine* te,
                                       SharedTermsDatabase& sharedTerms)
    : EnvObj(env),
      d_engine(te),
      d_sharedTerms(sharedTerms),
      d_preregistered(context())
{
}

std::string SharedTermsVisitor::toString() const {
  std::stringstream ss;
  TNodeVisitedMap::const_iterator it = d_visited.begin();
  for (; it != d_visited.end(); ++ it) {
    ss << (*it).first << ": " << TheoryIdSetUtil::setToString((*it).second)
       << std::endl;
  }
  return ss.str();
}

bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {

  Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;

  if ((parent.isClosure()
       || parent.getKind() == kind::SEP_STAR
       || parent.getKind() == kind::SEP_WAND
       || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
       )
      && current != parent)
  {
    Debug("register::internal") << "quantifier:true" << std::endl;
    return true;
  }
  TNodeVisitedMap::const_iterator find = d_visited.find(current);
  // If node is not visited at all, just return false
  if (find == d_visited.end()) {
    Debug("register::internal") << "1:false" << std::endl;
    return false;
  }

  TheoryIdSet visitedTheories = (*find).second;
  return isAlreadyVisited(d_env, visitedTheories, current, parent);
}

void SharedTermsVisitor::visit(TNode current, TNode parent) {

  Debug("register") << "SharedTermsVisitor::visit(" << current << "," << parent << ")" << std::endl;
  if (Debug.isOn("register::internal")) {
    Debug("register::internal") << toString() << std::endl;
  }
  TheoryIdSet visitedTheories = d_visited[current];
  TheoryIdSet preregTheories = d_preregistered[current];

  // preregister the term with the current, parent or type theories, as needed
  PreRegisterVisitor::preRegister(
      d_env, d_engine, visitedTheories, current, parent, preregTheories);

  // Record the new theories that we visited
  d_visited[current] = visitedTheories;

  // add visited theories to those who have preregistered
  d_preregistered[current] =
      TheoryIdSetUtil::setUnion(preregTheories, visitedTheories);

  // If there is more than two theories and a new one has been added notify the shared terms database
  TheoryId currentTheoryId = Theory::theoryOf(current);
  if (TheoryIdSetUtil::setDifference(
          visitedTheories, TheoryIdSetUtil::setInsert(currentTheoryId)))
  {
    d_sharedTerms.addSharedTerm(d_atom, current, visitedTheories);
  }

  Assert(d_visited.find(current) != d_visited.end());
  Assert(alreadyVisited(current, parent));
}

void SharedTermsVisitor::start(TNode node) {
  d_visited.clear();
  d_atom = node;
}

void SharedTermsVisitor::done(TNode node) {
  clear();
}

void SharedTermsVisitor::clear() {
  d_atom = TNode();
  d_visited.clear();
}

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Dejan Jovanovic, Morgan Deters
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		* [[ Add lengthier description here ]]
14		* \todo document this file
15		*/
16
17		#include "theory/term_registration_visitor.h"
18
19		#include "base/configuration.h"
20		#include "options/quantifiers_options.h"
21		#include "smt/logic_exception.h"
22		#include "theory/theory_engine.h"
23
24		using namespace cvc5::theory;
25
26		namespace cvc5 {
27
28		std::string PreRegisterVisitor::toString() const {
29		std::stringstream ss;
30		TNodeToTheorySetMap::const_iterator it = d_visited.begin();
31		for (; it != d_visited.end(); ++ it) {
32		ss << (it).first << ": " << TheoryIdSetUtil::setToString((it).second)
33		<< std::endl;
34		}
35		return ss.str();
36		}
37
38		/**
39		* Return true if we already visited the term current with the given parent,
40		* assuming that the set of theories in visitedTheories has already processed
41		* current. This method is used by PreRegisterVisitor and SharedTermsVisitor
42		* below.
43		*/
44	7584909	bool isAlreadyVisited(Env& env,
45		TheoryIdSet visitedTheories,
46		TNode current,
47		TNode parent)
48		{
49	7584909	TheoryId currentTheoryId = Theory::theoryOf(current);
50	7584909	if (!TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories))
51		{
52		// current theory not visited, return false
53		return false;
54		}
55
56	7584909	if (current == parent)
57		{
58		// top-level and current visited, return true
59	1218857	return true;
60		}
61
62		// The current theory has already visited it, so now it depends on the parent
63		// and the type
64	6366052	TheoryId parentTheoryId = Theory::theoryOf(parent);
65	6366052	if (!TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories))
66		{
67		// parent theory not visited, return false
68	111247	return false;
69		}
70
71		// do we need to consider the type?
72	12509610	TypeNode type = current.getType();
73	6254805	if (currentTheoryId == parentTheoryId && !env.isFiniteType(type))
74		{
75		// current and parent are the same theory, and we are infinite, return true
76	3730180	return true;
77		}
78	2524625	TheoryId typeTheoryId = Theory::theoryOf(type);
79	2524625	return TheoryIdSetUtil::setContains(typeTheoryId, visitedTheories);
80		}
81
82	15273	PreRegisterVisitor::PreRegisterVisitor(Env& env, TheoryEngine* engine)
83	15273	: EnvObj(env), d_engine(engine), d_visited(context())
84		{
85	15273	}
86
87	1629470	bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
88
89	1629470	Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
90
91	3258940	if ((parent.isClosure()
92	1615321	\|\| parent.getKind() == kind::SEP_STAR
93	1615321	\|\| parent.getKind() == kind::SEP_WAND
94	3244791	\|\| (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
95		)
96	3273089	&& current != parent)
97		{
98	5680	Debug("register::internal") << "quantifier:true" << std::endl;
99	5680	return true;
100		}
101
102		// Get the theories that have already visited this node
103	1623790	TNodeToTheorySetMap::iterator find = d_visited.find(current);
104	1623790	if (find == d_visited.end()) {
105		// not visited at all, return false
106	873890	return false;
107		}
108
109	749900	TheoryIdSet visitedTheories = (*find).second;
110	749900	return isAlreadyVisited(d_env, visitedTheories, current, parent);
111		}
112
113	361213	void PreRegisterVisitor::visit(TNode current, TNode parent) {
114
115	361213	Debug("register") << "PreRegisterVisitor::visit(" << current << "," << parent << ")" << std::endl;
116	361213	if (Debug.isOn("register::internal")) {
117		Debug("register::internal") << toString() << std::endl;
118		}
119
120		// get the theories we already preregistered with
121	361213	TheoryIdSet visitedTheories = d_visited[current];
122
123		// call the preregistration on current, parent or type theories and update
124		// visitedTheories. The set of preregistering theories coincides with
125		// visitedTheories here.
126	361214	preRegister(
127		d_env, d_engine, visitedTheories, current, parent, visitedTheories);
128
129	722424	Debug("register::internal")
130	361212	<< "PreRegisterVisitor::visit(" << current << "," << parent
131	361212	<< "): now registered with "
132	361212	<< TheoryIdSetUtil::setToString(visitedTheories) << std::endl;
133		// update the theories set for current
134	361212	d_visited[current] = visitedTheories;
135	361212	Assert(d_visited.find(current) != d_visited.end());
136	361212	Assert(alreadyVisited(current, parent));
137	361212	}
138
139	6234429	void PreRegisterVisitor::preRegister(Env& env,
140		TheoryEngine* te,
141		TheoryIdSet& visitedTheories,
142		TNode current,
143		TNode parent,
144		TheoryIdSet preregTheories)
145		{
146		// Preregister with the current theory, if necessary
147	6234429	TheoryId currentTheoryId = Theory::theoryOf(current);
148	6234433	preRegisterWithTheory(
149		te, visitedTheories, currentTheoryId, current, parent, preregTheories);
150
151	6234425	if (current != parent)
152		{
153		// preregister with parent theory, if necessary
154	5017123	TheoryId parentTheoryId = Theory::theoryOf(parent);
155	5017123	preRegisterWithTheory(
156		te, visitedTheories, parentTheoryId, current, parent, preregTheories);
157
158		// Note that if enclosed by different theories it's shared, for example,
159		// in read(a, f(a)), f(a) should be shared with integers.
160	10034246	TypeNode type = current.getType();
161	5017123	if (currentTheoryId != parentTheoryId \|\| env.isFiniteType(type))
162		{
163		// preregister with the type's theory, if necessary
164	1828536	TheoryId typeTheoryId = Theory::theoryOf(type);
165	1828536	preRegisterWithTheory(
166		te, visitedTheories, typeTheoryId, current, parent, preregTheories);
167		}
168		}
169	6234425	}
170	13080088	void PreRegisterVisitor::preRegisterWithTheory(TheoryEngine* te,
171		TheoryIdSet& visitedTheories,
172		TheoryId id,
173		TNode current,
174		TNode parent,
175		TheoryIdSet preregTheories)
176		{
177	13080088	if (TheoryIdSetUtil::setContains(id, visitedTheories))
178		{
179		// already visited
180	5460309	return;
181		}
182	7619779	visitedTheories = TheoryIdSetUtil::setInsert(id, visitedTheories);
183	7619779	if (TheoryIdSetUtil::setContains(id, preregTheories))
184		{
185		// already pregregistered
186	5349142	return;
187		}
188	2270637	if (Configuration::isAssertionBuild())
189		{
190	4541274	Debug("register::internal")
191	2270637	<< "PreRegisterVisitor::visit(" << current << "," << parent
192	2270637	<< "): adding " << id << std::endl;
193		// This should never throw an exception, since theories should be
194		// guaranteed to be initialized.
195	2270637	if (!te->isTheoryEnabled(id))
196		{
197		const LogicInfo& l = te->getLogicInfo();
198		LogicInfo newLogicInfo = l.getUnlockedCopy();
199		newLogicInfo.enableTheory(id);
200		newLogicInfo.lock();
201		std::stringstream ss;
202		ss << "The logic was specified as " << l.getLogicString()
203		<< ", which doesn't include " << id
204		<< ", but found a term in that theory." << std::endl
205		<< "You might want to extend your logic to "
206		<< newLogicInfo.getLogicString() << std::endl;
207		throw LogicException(ss.str());
208		}
209		}
210		// call the theory's preRegisterTerm method
211	2270637	Theory* th = te->theoryOf(id);
212	2270641	th->preRegisterTerm(current);
213		}
214
215	211956	void PreRegisterVisitor::start(TNode node) {}
216
217	15273	SharedTermsVisitor::SharedTermsVisitor(Env& env,
218		TheoryEngine* te,
219	15273	SharedTermsDatabase& sharedTerms)
220		: EnvObj(env),
221		d_engine(te),
222		d_sharedTerms(sharedTerms),
223	15273	d_preregistered(context())
224		{
225	15273	}
226
227		std::string SharedTermsVisitor::toString() const {
228		std::stringstream ss;
229		TNodeVisitedMap::const_iterator it = d_visited.begin();
230		for (; it != d_visited.end(); ++ it) {
231		ss << (it).first << ": " << TheoryIdSetUtil::setToString((it).second)
232		<< std::endl;
233		}
234		return ss.str();
235		}
236
237	23707427	bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
238
239	23707427	Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
240
241	47414854	if ((parent.isClosure()
242	23548370	\|\| parent.getKind() == kind::SEP_STAR
243	23547705	\|\| parent.getKind() == kind::SEP_WAND
244	47255003	\|\| (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
245		)
246	47577501	&& current != parent)
247		{
248	69130	Debug("register::internal") << "quantifier:true" << std::endl;
249	69130	return true;
250		}
251	23638297	TNodeVisitedMap::const_iterator find = d_visited.find(current);
252		// If node is not visited at all, just return false
253	23638297	if (find == d_visited.end()) {
254	16803288	Debug("register::internal") << "1:false" << std::endl;
255	16803288	return false;
256		}
257
258	6835009	TheoryIdSet visitedTheories = (*find).second;
259	6835009	return isAlreadyVisited(d_env, visitedTheories, current, parent);
260		}
261
262	5873216	void SharedTermsVisitor::visit(TNode current, TNode parent) {
263
264	5873216	Debug("register") << "SharedTermsVisitor::visit(" << current << "," << parent << ")" << std::endl;
265	5873216	if (Debug.isOn("register::internal")) {
266		Debug("register::internal") << toString() << std::endl;
267		}
268	5873216	TheoryIdSet visitedTheories = d_visited[current];
269	5873216	TheoryIdSet preregTheories = d_preregistered[current];
270
271		// preregister the term with the current, parent or type theories, as needed
272	5873219	PreRegisterVisitor::preRegister(
273		d_env, d_engine, visitedTheories, current, parent, preregTheories);
274
275		// Record the new theories that we visited
276	5873213	d_visited[current] = visitedTheories;
277
278		// add visited theories to those who have preregistered
279	5873213	d_preregistered[current] =
280	11746426	TheoryIdSetUtil::setUnion(preregTheories, visitedTheories);
281
282		// If there is more than two theories and a new one has been added notify the shared terms database
283	5873213	TheoryId currentTheoryId = Theory::theoryOf(current);
284	11746426	if (TheoryIdSetUtil::setDifference(
285	5873213	visitedTheories, TheoryIdSetUtil::setInsert(currentTheoryId)))
286		{
287	1397679	d_sharedTerms.addSharedTerm(d_atom, current, visitedTheories);
288		}
289
290	5873213	Assert(d_visited.find(current) != d_visited.end());
291	5873213	Assert(alreadyVisited(current, parent));
292	5873213	}
293
294	1006905	void SharedTermsVisitor::start(TNode node) {
295	1006905	d_visited.clear();
296	1006905	d_atom = node;
297	1006905	}
298
299	1006902	void SharedTermsVisitor::done(TNode node) {
300	1006902	clear();
301	1006902	}
302
303	1006902	void SharedTermsVisitor::clear() {
304	1006902	d_atom = TNode();
305	1006902	d_visited.clear();
306	1006902	}
307
308	31137	} // namespace cvc5