Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/term_registration_visitor.cpp	Lines:	109	136	80.1 %
Date:	2021-09-13	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	6815813	bool isAlreadyVisited(TheoryEngine* te,
45		TheoryIdSet visitedTheories,
46		TNode current,
47		TNode parent)
48		{
49	6815813	TheoryId currentTheoryId = Theory::theoryOf(current);
50	6815813	if (!TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories))
51		{
52		// current theory not visited, return false
53		return false;
54		}
55
56	6815813	if (current == parent)
57		{
58		// top-level and current visited, return true
59	1083186	return true;
60		}
61
62		// The current theory has already visited it, so now it depends on the parent
63		// and the type
64	5732627	TheoryId parentTheoryId = Theory::theoryOf(parent);
65	5732627	if (!TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories))
66		{
67		// parent theory not visited, return false
68	102089	return false;
69		}
70
71		// do we need to consider the type?
72	11261076	TypeNode type = current.getType();
73	5630538	if (currentTheoryId == parentTheoryId && !te->isFiniteType(type))
74		{
75		// current and parent are the same theory, and we are infinite, return true
76	3383518	return true;
77		}
78	2247020	TheoryId typeTheoryId = Theory::theoryOf(type);
79	2247020	return TheoryIdSetUtil::setContains(typeTheoryId, visitedTheories);
80		}
81
82	1565153	bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
83
84	1565153	Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
85
86	3130306	if ((parent.isClosure()
87	1551790	\|\| parent.getKind() == kind::SEP_STAR
88	1551790	\|\| parent.getKind() == kind::SEP_WAND
89	3116943	\|\| (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
90		// parent.getKind() == kind::CARDINALITY_CONSTRAINT
91		)
92	3143669	&& 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	1559788	TNodeToTheorySetMap::iterator find = d_visited.find(current);
100	1559788	if (find == d_visited.end()) {
101		// not visited at all, return false
102	839463	return false;
103		}
104
105	720325	TheoryIdSet visitedTheories = (*find).second;
106	720325	return isAlreadyVisited(d_engine, visitedTheories, current, parent);
107		}
108
109	347550	void PreRegisterVisitor::visit(TNode current, TNode parent) {
110
111	347550	Debug("register") << "PreRegisterVisitor::visit(" << current << "," << parent << ")" << std::endl;
112	347550	if (Debug.isOn("register::internal")) {
113		Debug("register::internal") << toString() << std::endl;
114		}
115
116		// get the theories we already preregistered with
117	347550	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	347551	preRegister(d_engine, visitedTheories, current, parent, visitedTheories);
123
124	695098	Debug("register::internal")
125	347549	<< "PreRegisterVisitor::visit(" << current << "," << parent
126	347549	<< "): now registered with "
127	347549	<< TheoryIdSetUtil::setToString(visitedTheories) << std::endl;
128		// update the theories set for current
129	347549	d_visited[current] = visitedTheories;
130	347549	Assert(d_visited.find(current) != d_visited.end());
131	347549	Assert(alreadyVisited(current, parent));
132	347549	}
133
134	5593836	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	5593836	TheoryId currentTheoryId = Theory::theoryOf(current);
142	5593840	preRegisterWithTheory(
143		te, visitedTheories, currentTheoryId, current, parent, preregTheories);
144
145	5593832	if (current != parent)
146		{
147		// preregister with parent theory, if necessary
148	4512128	TheoryId parentTheoryId = Theory::theoryOf(parent);
149	4512128	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	9024256	TypeNode type = current.getType();
155	4512128	if (currentTheoryId != parentTheoryId \|\| te->isFiniteType(type))
156		{
157		// preregister with the type's theory, if necessary
158	1629537	TheoryId typeTheoryId = Theory::theoryOf(type);
159	1629537	preRegisterWithTheory(
160		te, visitedTheories, typeTheoryId, current, parent, preregTheories);
161		}
162		}
163	5593832	}
164	11735501	void PreRegisterVisitor::preRegisterWithTheory(TheoryEngine* te,
165		TheoryIdSet& visitedTheories,
166		TheoryId id,
167		TNode current,
168		TNode parent,
169		TheoryIdSet preregTheories)
170		{
171	11735501	if (TheoryIdSetUtil::setContains(id, visitedTheories))
172		{
173		// already visited
174	4930025	return;
175		}
176	6805476	visitedTheories = TheoryIdSetUtil::setInsert(id, visitedTheories);
177	6805476	if (TheoryIdSetUtil::setContains(id, preregTheories))
178		{
179		// already pregregistered
180	4758565	return;
181		}
182	2046911	if (Configuration::isAssertionBuild())
183		{
184	4093822	Debug("register::internal")
185	2046911	<< "PreRegisterVisitor::visit(" << current << "," << parent
186	2046911	<< "): 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	2046911	if (!options::finiteModelFind())
193		{
194	1961287	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	2046911	Theory* th = te->theoryOf(id);
212	2046915	th->preRegisterTerm(current);
213		}
214
215	205319	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	21185591	bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
228
229	21185591	Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
230
231	42371182	if ((parent.isClosure()
232	21031991	\|\| parent.getKind() == kind::SEP_STAR
233	21031326	\|\| parent.getKind() == kind::SEP_WAND
234	42216788	\|\| (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
235		// parent.getKind() == kind::CARDINALITY_CONSTRAINT
236		)
237	42528372	&& current != parent)
238		{
239	66724	Debug("register::internal") << "quantifier:true" << std::endl;
240	66724	return true;
241		}
242	21118867	TNodeVisitedMap::const_iterator find = d_visited.find(current);
243		// If node is not visited at all, just return false
244	21118867	if (find == d_visited.end()) {
245	15023379	Debug("register::internal") << "1:false" << std::endl;
246	15023379	return false;
247		}
248
249	6095488	TheoryIdSet visitedTheories = (*find).second;
250	6095488	return isAlreadyVisited(d_engine, visitedTheories, current, parent);
251		}
252
253	5246286	void SharedTermsVisitor::visit(TNode current, TNode parent) {
254
255	5246286	Debug("register") << "SharedTermsVisitor::visit(" << current << "," << parent << ")" << std::endl;
256	5246286	if (Debug.isOn("register::internal")) {
257		Debug("register::internal") << toString() << std::endl;
258		}
259	5246286	TheoryIdSet visitedTheories = d_visited[current];
260	5246286	TheoryIdSet preregTheories = d_preregistered[current];
261
262		// preregister the term with the current, parent or type theories, as needed
263	5246289	PreRegisterVisitor::preRegister(
264		d_engine, visitedTheories, current, parent, preregTheories);
265
266		// Record the new theories that we visited
267	5246283	d_visited[current] = visitedTheories;
268
269		// add visited theories to those who have preregistered
270	5246283	d_preregistered[current] =
271	10492566	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	5246283	TheoryId currentTheoryId = Theory::theoryOf(current);
275	10492566	if (TheoryIdSetUtil::setDifference(
276	5246283	visitedTheories, TheoryIdSetUtil::setInsert(currentTheoryId)))
277		{
278	1225217	d_sharedTerms.addSharedTerm(d_atom, current, visitedTheories);
279		}
280
281	5246283	Assert(d_visited.find(current) != d_visited.end());
282	5246283	Assert(alreadyVisited(current, parent));
283	5246283	}
284
285	877871	void SharedTermsVisitor::start(TNode node) {
286	877871	d_visited.clear();
287	877871	d_atom = node;
288	877871	}
289
290	877868	void SharedTermsVisitor::done(TNode node) {
291	877868	clear();
292	877868	}
293
294	877868	void SharedTermsVisitor::clear() {
295	877868	d_atom = TNode();
296	877868	d_visited.clear();
297	877868	}
298
299	29514	} // namespace cvc5