Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/term_registration_visitor.cpp	Lines:	109	136	80.1 %
Date:	2021-09-10	Branches:	232	562	41.3 %


/******************************************************************************
 * 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(TheoryEngine* te,
                      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 && !te->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);
}

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())
       // parent.getKind() == kind::CARDINALITY_CONSTRAINT
       )
      && 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_engine, 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_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(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 || te->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.
    // These checks don't work with finite model finding, because it
    // uses Rational constants to represent cardinality constraints,
    // even though arithmetic isn't actually involved.
    if (!options::finiteModelFind())
    {
      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) {}

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())
       // parent.getKind() == kind::CARDINALITY_CONSTRAINT
       )
      && 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_engine, 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_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	6796241	bool isAlreadyVisited(TheoryEngine* te,
45		TheoryIdSet visitedTheories,
46		TNode current,
47		TNode parent)
48		{
49	6796241	TheoryId currentTheoryId = Theory::theoryOf(current);
50	6796241	if (!TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories))
51		{
52		// current theory not visited, return false
53		return false;
54		}
55
56	6796241	if (current == parent)
57		{
58		// top-level and current visited, return true
59	1079816	return true;
60		}
61
62		// The current theory has already visited it, so now it depends on the parent
63		// and the type
64	5716425	TheoryId parentTheoryId = Theory::theoryOf(parent);
65	5716425	if (!TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories))
66		{
67		// parent theory not visited, return false
68	101848	return false;
69		}
70
71		// do we need to consider the type?
72	11229154	TypeNode type = current.getType();
73	5614577	if (currentTheoryId == parentTheoryId && !te->isFiniteType(type))
74		{
75		// current and parent are the same theory, and we are infinite, return true
76	3376471	return true;
77		}
78	2238106	TheoryId typeTheoryId = Theory::theoryOf(type);
79	2238106	return TheoryIdSetUtil::setContains(typeTheoryId, visitedTheories);
80		}
81
82	1565537	bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
83
84	1565537	Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
85
86	3131074	if ((parent.isClosure()
87	1552174	\|\| parent.getKind() == kind::SEP_STAR
88	1552174	\|\| parent.getKind() == kind::SEP_WAND
89	3117711	\|\| (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
90		// parent.getKind() == kind::CARDINALITY_CONSTRAINT
91		)
92	3144437	&& current != parent)
93		{
94	5365	Debug("register::internal") << "quantifier:true" << std::endl;
95	5365	return true;
96		}
97
98		// Get the theories that have already visited this node
99	1560172	TNodeToTheorySetMap::iterator find = d_visited.find(current);
100	1560172	if (find == d_visited.end()) {
101		// not visited at all, return false
102	839655	return false;
103		}
104
105	720517	TheoryIdSet visitedTheories = (*find).second;
106	720517	return isAlreadyVisited(d_engine, visitedTheories, current, parent);
107		}
108
109	347646	void PreRegisterVisitor::visit(TNode current, TNode parent) {
110
111	347646	Debug("register") << "PreRegisterVisitor::visit(" << current << "," << parent << ")" << std::endl;
112	347646	if (Debug.isOn("register::internal")) {
113		Debug("register::internal") << toString() << std::endl;
114		}
115
116		// get the theories we already preregistered with
117	347646	TheoryIdSet visitedTheories = d_visited[current];
118
119		// call the preregistration on current, parent or type theories and update
120		// visitedTheories. The set of preregistering theories coincides with
121		// visitedTheories here.
122	347647	preRegister(d_engine, visitedTheories, current, parent, visitedTheories);
123
124	695290	Debug("register::internal")
125	347645	<< "PreRegisterVisitor::visit(" << current << "," << parent
126	347645	<< "): now registered with "
127	347645	<< TheoryIdSetUtil::setToString(visitedTheories) << std::endl;
128		// update the theories set for current
129	347645	d_visited[current] = visitedTheories;
130	347645	Assert(d_visited.find(current) != d_visited.end());
131	347645	Assert(alreadyVisited(current, parent));
132	347645	}
133
134	5574849	void PreRegisterVisitor::preRegister(TheoryEngine* te,
135		TheoryIdSet& visitedTheories,
136		TNode current,
137		TNode parent,
138		TheoryIdSet preregTheories)
139		{
140		// Preregister with the current theory, if necessary
141	5574849	TheoryId currentTheoryId = Theory::theoryOf(current);
142	5574853	preRegisterWithTheory(
143		te, visitedTheories, currentTheoryId, current, parent, preregTheories);
144
145	5574845	if (current != parent)
146		{
147		// preregister with parent theory, if necessary
148	4496511	TheoryId parentTheoryId = Theory::theoryOf(parent);
149	4496511	preRegisterWithTheory(
150		te, visitedTheories, parentTheoryId, current, parent, preregTheories);
151
152		// Note that if enclosed by different theories it's shared, for example,
153		// in read(a, f(a)), f(a) should be shared with integers.
154	8993022	TypeNode type = current.getType();
155	4496511	if (currentTheoryId != parentTheoryId \|\| te->isFiniteType(type))
156		{
157		// preregister with the type's theory, if necessary
158	1620743	TheoryId typeTheoryId = Theory::theoryOf(type);
159	1620743	preRegisterWithTheory(
160		te, visitedTheories, typeTheoryId, current, parent, preregTheories);
161		}
162		}
163	5574845	}
164	11692103	void PreRegisterVisitor::preRegisterWithTheory(TheoryEngine* te,
165		TheoryIdSet& visitedTheories,
166		TheoryId id,
167		TNode current,
168		TNode parent,
169		TheoryIdSet preregTheories)
170		{
171	11692103	if (TheoryIdSetUtil::setContains(id, visitedTheories))
172		{
173		// already visited
174	4914327	return;
175		}
176	6777776	visitedTheories = TheoryIdSetUtil::setInsert(id, visitedTheories);
177	6777776	if (TheoryIdSetUtil::setContains(id, preregTheories))
178		{
179		// already pregregistered
180	4735205	return;
181		}
182	2042571	if (Configuration::isAssertionBuild())
183		{
184	4085142	Debug("register::internal")
185	2042571	<< "PreRegisterVisitor::visit(" << current << "," << parent
186	2042571	<< "): adding " << id << std::endl;
187		// This should never throw an exception, since theories should be
188		// guaranteed to be initialized.
189		// These checks don't work with finite model finding, because it
190		// uses Rational constants to represent cardinality constraints,
191		// even though arithmetic isn't actually involved.
192	2042571	if (!options::finiteModelFind())
193		{
194	1956947	if (!te->isTheoryEnabled(id))
195		{
196		const LogicInfo& l = te->getLogicInfo();
197		LogicInfo newLogicInfo = l.getUnlockedCopy();
198		newLogicInfo.enableTheory(id);
199		newLogicInfo.lock();
200		std::stringstream ss;
201		ss << "The logic was specified as " << l.getLogicString()
202		<< ", which doesn't include " << id
203		<< ", but found a term in that theory." << std::endl
204		<< "You might want to extend your logic to "
205		<< newLogicInfo.getLogicString() << std::endl;
206		throw LogicException(ss.str());
207		}
208		}
209		}
210		// call the theory's preRegisterTerm method
211	2042571	Theory* th = te->theoryOf(id);
212	2042575	th->preRegisterTerm(current);
213		}
214
215	205415	void PreRegisterVisitor::start(TNode node) {}
216
217		std::string SharedTermsVisitor::toString() const {
218		std::stringstream ss;
219		TNodeVisitedMap::const_iterator it = d_visited.begin();
220		for (; it != d_visited.end(); ++ it) {
221		ss << (it).first << ": " << TheoryIdSetUtil::setToString((it).second)
222		<< std::endl;
223		}
224		return ss.str();
225		}
226
227	21112234	bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
228
229	21112234	Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
230
231	42224468	if ((parent.isClosure()
232	20958634	\|\| parent.getKind() == kind::SEP_STAR
233	20957969	\|\| parent.getKind() == kind::SEP_WAND
234	42070074	\|\| (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
235		// parent.getKind() == kind::CARDINALITY_CONSTRAINT
236		)
237	42381658	&& current != parent)
238		{
239	66724	Debug("register::internal") << "quantifier:true" << std::endl;
240	66724	return true;
241		}
242	21045510	TNodeVisitedMap::const_iterator find = d_visited.find(current);
243		// If node is not visited at all, just return false
244	21045510	if (find == d_visited.end()) {
245	14969786	Debug("register::internal") << "1:false" << std::endl;
246	14969786	return false;
247		}
248
249	6075724	TheoryIdSet visitedTheories = (*find).second;
250	6075724	return isAlreadyVisited(d_engine, visitedTheories, current, parent);
251		}
252
253	5227203	void SharedTermsVisitor::visit(TNode current, TNode parent) {
254
255	5227203	Debug("register") << "SharedTermsVisitor::visit(" << current << "," << parent << ")" << std::endl;
256	5227203	if (Debug.isOn("register::internal")) {
257		Debug("register::internal") << toString() << std::endl;
258		}
259	5227203	TheoryIdSet visitedTheories = d_visited[current];
260	5227203	TheoryIdSet preregTheories = d_preregistered[current];
261
262		// preregister the term with the current, parent or type theories, as needed
263	5227206	PreRegisterVisitor::preRegister(
264		d_engine, visitedTheories, current, parent, preregTheories);
265
266		// Record the new theories that we visited
267	5227200	d_visited[current] = visitedTheories;
268
269		// add visited theories to those who have preregistered
270	5227200	d_preregistered[current] =
271	10454400	TheoryIdSetUtil::setUnion(preregTheories, visitedTheories);
272
273		// If there is more than two theories and a new one has been added notify the shared terms database
274	5227200	TheoryId currentTheoryId = Theory::theoryOf(current);
275	10454400	if (TheoryIdSetUtil::setDifference(
276	5227200	visitedTheories, TheoryIdSetUtil::setInsert(currentTheoryId)))
277		{
278	1216423	d_sharedTerms.addSharedTerm(d_atom, current, visitedTheories);
279		}
280
281	5227200	Assert(d_visited.find(current) != d_visited.end());
282	5227200	Assert(alreadyVisited(current, parent));
283	5227200	}
284
285	874405	void SharedTermsVisitor::start(TNode node) {
286	874405	d_visited.clear();
287	874405	d_atom = node;
288	874405	}
289
290	874402	void SharedTermsVisitor::done(TNode node) {
291	874402	clear();
292	874402	}
293
294	874402	void SharedTermsVisitor::clear() {
295	874402	d_atom = TNode();
296	874402	d_visited.clear();
297	874402	}
298
299	29502	} // namespace cvc5