Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/substitutions.cpp	Lines:	93	109	85.3 %
Date:	2021-09-11	Branches:	218	530	41.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Dejan Jovanovic, Clark Barrett, 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.
 * ****************************************************************************
 *
 * A substitution mapping for theory simplification.
 */

#include "theory/substitutions.h"
#include "expr/node_algorithm.h"
#include "theory/rewriter.h"

using namespace std;

namespace cvc5 {
namespace theory {

SubstitutionMap::SubstitutionMap(context::Context* context)
    : d_context(),
      d_substitutions(context ? context : &d_context),
      d_substitutionCache(),
      d_cacheInvalidated(false),
      d_cacheInvalidator(context ? context : &d_context, d_cacheInvalidated)
{
}

struct substitution_stack_element {
  TNode d_node;
  bool d_children_added;
  substitution_stack_element(TNode node) : d_node(node), d_children_added(false)
  {
  }
};/* struct substitution_stack_element */

Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) {

  Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << ")" << endl;

  if (d_substitutions.empty()) {
    return t;
  }

  // Do a topological sort of the subexpressions and substitute them
  vector<substitution_stack_element> toVisit;
  toVisit.push_back((TNode) t);

  while (!toVisit.empty())
  {
    // The current node we are processing
    substitution_stack_element& stackHead = toVisit.back();
    TNode current = stackHead.d_node;

    Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): processing " << current << endl;

    // If node already in the cache we're done, pop from the stack
    NodeCache::iterator find = cache.find(current);
    if (find != cache.end()) {
      toVisit.pop_back();
      continue;
    }

    NodeMap::iterator find2 = d_substitutions.find(current);
    if (find2 != d_substitutions.end()) {
      Node rhs = (*find2).second;
      Assert(rhs != current);
      internalSubstitute(rhs, cache);
      d_substitutions[current] = cache[rhs];
      cache[current] = cache[rhs];
      toVisit.pop_back();
      continue;
    }

    // Not yet substituted, so process
    if (stackHead.d_children_added)
    {
      // Children have been processed, so substitute
      NodeBuilder builder(current.getKind());
      if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
        builder << Node(cache[current.getOperator()]);
      }
      for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
        Assert(cache.find(current[i]) != cache.end());
        builder << Node(cache[current[i]]);
      }
      // Mark the substitution and continue
      Node result = builder;
      if (result != current) {
        find = cache.find(result);
        if (find != cache.end()) {
          result = find->second;
        }
        else {
          find2 = d_substitutions.find(result);
          if (find2 != d_substitutions.end()) {
            Node rhs = (*find2).second;
            Assert(rhs != result);
            internalSubstitute(rhs, cache);
            d_substitutions[result] = cache[rhs];
            cache[result] = cache[rhs];
            result = cache[rhs];
          }
        }
      }
      Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << endl;
      cache[current] = result;
      toVisit.pop_back();
    }
    else
    {
      // Mark that we have added the children if any
      if (current.getNumChildren() > 0 || current.getMetaKind() == kind::metakind::PARAMETERIZED) {
        stackHead.d_children_added = true;
        // We need to add the operator, if any
        if(current.getMetaKind() == kind::metakind::PARAMETERIZED) {
          TNode opNode = current.getOperator();
          NodeCache::iterator opFind = cache.find(opNode);
          if (opFind == cache.end()) {
            toVisit.push_back(opNode);
          }
        }
        // We need to add the children
        for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
          TNode childNode = *child_it;
          NodeCache::iterator childFind = cache.find(childNode);
          if (childFind == cache.end()) {
            toVisit.push_back(childNode);
          }
        }
      } else {
        // No children, so we're done
        Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << current << endl;
        cache[current] = current;
        toVisit.pop_back();
      }
    }
  }

  // Return the substituted version
  return cache[t];
}/* SubstitutionMap::internalSubstitute() */


void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache)
{
  Debug("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << endl;
  Assert(d_substitutions.find(x) == d_substitutions.end());

  // this causes a later assert-fail (the rhs != current one, above) anyway
  // putting it here is easier to diagnose
  Assert(x != t) << "cannot substitute a term for itself";

  d_substitutions[x] = t;

  // Also invalidate the cache if necessary
  if (invalidateCache) {
    d_cacheInvalidated = true;
  }
  else {
    d_substitutionCache[x] = d_substitutions[x];
  }
}


void SubstitutionMap::addSubstitutions(SubstitutionMap& subMap, bool invalidateCache)
{
  SubstitutionMap::NodeMap::const_iterator it = subMap.begin();
  SubstitutionMap::NodeMap::const_iterator it_end = subMap.end();
  for (; it != it_end; ++ it) {
    Assert(d_substitutions.find((*it).first) == d_substitutions.end());
    d_substitutions[(*it).first] = (*it).second;
    if (!invalidateCache) {
      d_substitutionCache[(*it).first] = d_substitutions[(*it).first];
    }
  }
  if (invalidateCache) {
    d_cacheInvalidated = true;
  }
}

Node SubstitutionMap::apply(TNode t, bool doRewrite) {

  Debug("substitution") << "SubstitutionMap::apply(" << t << ")" << endl;

  // Setup the cache
  if (d_cacheInvalidated) {
    d_substitutionCache.clear();
    d_cacheInvalidated = false;
    Debug("substitution") << "-- reset the cache" << endl;
  }

  // Perform the substitution
  Node result = internalSubstitute(t, d_substitutionCache);
  Debug("substitution") << "SubstitutionMap::apply(" << t << ") => " << result << endl;

  if (doRewrite)
  {
    result = Rewriter::rewrite(result);
  }

  return result;
}

void SubstitutionMap::print(ostream& out) const {
  NodeMap::const_iterator it = d_substitutions.begin();
  NodeMap::const_iterator it_end = d_substitutions.end();
  for (; it != it_end; ++ it) {
    out << (*it).first << " -> " << (*it).second << endl;
  }
}

void SubstitutionMap::debugPrint() const { print(CVC5Message.getStream()); }

}  // namespace theory

std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i) {
  return out << "[CDMap-iterator]";
}

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Dejan Jovanovic, Clark Barrett, 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		* A substitution mapping for theory simplification.
14		*/
15
16		#include "theory/substitutions.h"
17		#include "expr/node_algorithm.h"
18		#include "theory/rewriter.h"
19
20		using namespace std;
21
22		namespace cvc5 {
23		namespace theory {
24
25	116617	SubstitutionMap::SubstitutionMap(context::Context* context)
26		: d_context(),
27		d_substitutions(context ? context : &d_context),
28		d_substitutionCache(),
29		d_cacheInvalidated(false),
30	116617	d_cacheInvalidator(context ? context : &d_context, d_cacheInvalidated)
31		{
32	116617	}
33
34	12676150	struct substitution_stack_element {
35		TNode d_node;
36		bool d_children_added;
37	2974440	substitution_stack_element(TNode node) : d_node(node), d_children_added(false)
38		{
39	2974440	}
40		};/* struct substitution_stack_element */
41
42	1791371	Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) {
43
44	1791371	Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << ")" << endl;
45
46	1791371	if (d_substitutions.empty()) {
47	1070814	return t;
48		}
49
50		// Do a topological sort of the subexpressions and substitute them
51	1441114	vector<substitution_stack_element> toVisit;
52	720557	toVisit.push_back((TNode) t);
53
54	10465183	while (!toVisit.empty())
55		{
56		// The current node we are processing
57	4872313	substitution_stack_element& stackHead = toVisit.back();
58	9192057	TNode current = stackHead.d_node;
59
60	4872313	Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): processing " << current << endl;
61
62		// If node already in the cache we're done, pop from the stack
63	4872313	NodeCache::iterator find = cache.find(current);
64	5265665	if (find != cache.end()) {
65	393352	toVisit.pop_back();
66	393352	continue;
67		}
68
69	4478961	NodeMap::iterator find2 = d_substitutions.find(current);
70	4478961	if (find2 != d_substitutions.end()) {
71	318434	Node rhs = (*find2).second;
72	159217	Assert(rhs != current);
73	159217	internalSubstitute(rhs, cache);
74	159217	d_substitutions[current] = cache[rhs];
75	159217	cache[current] = cache[rhs];
76	159217	toVisit.pop_back();
77	159217	continue;
78		}
79
80		// Not yet substituted, so process
81	4319744	if (stackHead.d_children_added)
82		{
83		// Children have been processed, so substitute
84	3795746	NodeBuilder builder(current.getKind());
85	1897873	if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
86	189103	builder << Node(cache[current.getOperator()]);
87		}
88	6515144	for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
89	4617271	Assert(cache.find(current[i]) != cache.end());
90	4617271	builder << Node(cache[current[i]]);
91		}
92		// Mark the substitution and continue
93	3795746	Node result = builder;
94	1897873	if (result != current) {
95	723857	find = cache.find(result);
96	723857	if (find != cache.end()) {
97	4590	result = find->second;
98		}
99		else {
100	719267	find2 = d_substitutions.find(result);
101	719267	if (find2 != d_substitutions.end()) {
102		Node rhs = (*find2).second;
103		Assert(rhs != result);
104		internalSubstitute(rhs, cache);
105		d_substitutions[result] = cache[rhs];
106		cache[result] = cache[rhs];
107		result = cache[rhs];
108		}
109		}
110		}
111	1897873	Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << endl;
112	1897873	cache[current] = result;
113	1897873	toVisit.pop_back();
114		}
115		else
116		{
117		// Mark that we have added the children if any
118	2421871	if (current.getNumChildren() > 0 \|\| current.getMetaKind() == kind::metakind::PARAMETERIZED) {
119	1897873	stackHead.d_children_added = true;
120		// We need to add the operator, if any
121	1897873	if(current.getMetaKind() == kind::metakind::PARAMETERIZED) {
122	378206	TNode opNode = current.getOperator();
123	189103	NodeCache::iterator opFind = cache.find(opNode);
124	189103	if (opFind == cache.end()) {
125	51959	toVisit.push_back(opNode);
126		}
127		}
128		// We need to add the children
129	6515144	for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
130	9234542	TNode childNode = *child_it;
131	4617271	NodeCache::iterator childFind = cache.find(childNode);
132	4617271	if (childFind == cache.end()) {
133	2201924	toVisit.push_back(childNode);
134		}
135		}
136		} else {
137		// No children, so we're done
138	523998	Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << current << endl;
139	523998	cache[current] = current;
140	523998	toVisit.pop_back();
141		}
142		}
143		}
144
145		// Return the substituted version
146	720557	return cache[t];
147		}/* SubstitutionMap::internalSubstitute() */
148
149
150	2470813	void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache)
151		{
152	2470813	Debug("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << endl;
153	2470813	Assert(d_substitutions.find(x) == d_substitutions.end());
154
155		// this causes a later assert-fail (the rhs != current one, above) anyway
156		// putting it here is easier to diagnose
157	2470813	Assert(x != t) << "cannot substitute a term for itself";
158
159	2470813	d_substitutions[x] = t;
160
161		// Also invalidate the cache if necessary
162	2470813	if (invalidateCache) {
163	2470701	d_cacheInvalidated = true;
164		}
165		else {
166	112	d_substitutionCache[x] = d_substitutions[x];
167		}
168	2470813	}
169
170
171	8198	void SubstitutionMap::addSubstitutions(SubstitutionMap& subMap, bool invalidateCache)
172		{
173	8198	SubstitutionMap::NodeMap::const_iterator it = subMap.begin();
174	8198	SubstitutionMap::NodeMap::const_iterator it_end = subMap.end();
175	94156	for (; it != it_end; ++ it) {
176	42979	Assert(d_substitutions.find((*it).first) == d_substitutions.end());
177	42979	d_substitutions[(it).first] = (it).second;
178	42979	if (!invalidateCache) {
179		d_substitutionCache[(it).first] = d_substitutions[(it).first];
180		}
181		}
182	8198	if (invalidateCache) {
183	8198	d_cacheInvalidated = true;
184		}
185	8198	}
186
187	1632154	Node SubstitutionMap::apply(TNode t, bool doRewrite) {
188
189	1632154	Debug("substitution") << "SubstitutionMap::apply(" << t << ")" << endl;
190
191		// Setup the cache
192	1632154	if (d_cacheInvalidated) {
193	75790	d_substitutionCache.clear();
194	75790	d_cacheInvalidated = false;
195	75790	Debug("substitution") << "-- reset the cache" << endl;
196		}
197
198		// Perform the substitution
199	1632154	Node result = internalSubstitute(t, d_substitutionCache);
200	1632154	Debug("substitution") << "SubstitutionMap::apply(" << t << ") => " << result << endl;
201
202	1632154	if (doRewrite)
203		{
204	1031137	result = Rewriter::rewrite(result);
205		}
206
207	1632152	return result;
208		}
209
210		void SubstitutionMap::print(ostream& out) const {
211		NodeMap::const_iterator it = d_substitutions.begin();
212		NodeMap::const_iterator it_end = d_substitutions.end();
213		for (; it != it_end; ++ it) {
214		out << (it).first << " -> " << (it).second << endl;
215		}
216		}
217
218		void SubstitutionMap::debugPrint() const { print(CVC5Message.getStream()); }
219
220		} // namespace theory
221
222		std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i) {
223		return out << "[CDMap-iterator]";
224		}
225
226	29511	} // namespace cvc5