Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/printer/let_binding.cpp	Lines:	103	105	98.1 %
Date:	2021-09-10	Branches:	169	362	46.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds
 *
 * 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 let binding utility.
 */

#include "printer/let_binding.h"

#include <sstream>

namespace cvc5 {

LetBinding::LetBinding(uint32_t thresh)
    : d_thresh(thresh),
      d_context(),
      d_visitList(&d_context),
      d_count(&d_context),
      d_letList(&d_context),
      d_letMap(&d_context)
{
}

uint32_t LetBinding::getThreshold() const { return d_thresh; }

void LetBinding::process(Node n)
{
  if (n.isNull() || d_thresh == 0)
  {
    // value of 0 means do not introduce let
    return;
  }
  // update the count of occurrences
  updateCounts(n);
}

void LetBinding::letify(Node n, std::vector<Node>& letList)
{
  // first, push the context
  pushScope();
  // process the node
  process(n);
  // now, letify
  letify(letList);
}

void LetBinding::letify(std::vector<Node>& letList)
{
  size_t prevSize = d_letList.size();
  // populate the d_letList and d_letMap
  convertCountToLet();
  // add the new entries to the letList
  letList.insert(letList.end(), d_letList.begin() + prevSize, d_letList.end());
}

void LetBinding::pushScope() { d_context.push(); }

void LetBinding::popScope() { d_context.pop(); }

uint32_t LetBinding::getId(Node n) const
{
  NodeIdMap::const_iterator it = d_letMap.find(n);
  if (it == d_letMap.end())
  {
    return 0;
  }
  return (*it).second;
}

Node LetBinding::convert(Node n, const std::string& prefix, bool letTop) const
{
  if (d_letMap.empty())
  {
    return n;
  }
  NodeManager* nm = NodeManager::currentNM();
  std::unordered_map<TNode, Node> visited;
  std::unordered_map<TNode, Node>::iterator it;
  std::vector<TNode> visit;
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();
    it = visited.find(cur);

    if (it == visited.end())
    {
      uint32_t id = getId(cur);
      // do not letify id 0, or n itself if letTop is false
      if (id > 0 && (cur != n || letTop))
      {
        // make the let variable
        std::stringstream ss;
        ss << prefix << id;
        visited[cur] = nm->mkBoundVar(ss.str(), cur.getType());
      }
      else if (cur.isClosure())
      {
        // do not convert beneath quantifiers
        visited[cur] = cur;
      }
      else
      {
        visited[cur] = Node::null();
        visit.push_back(cur);
        visit.insert(visit.end(), cur.begin(), cur.end());
      }
    }
    else if (it->second.isNull())
    {
      Node ret = cur;
      bool childChanged = false;
      std::vector<Node> children;
      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
      {
        children.push_back(cur.getOperator());
      }
      for (const Node& cn : cur)
      {
        it = visited.find(cn);
        Assert(it != visited.end());
        Assert(!it->second.isNull());
        childChanged = childChanged || cn != it->second;
        children.push_back(it->second);
      }
      if (childChanged)
      {
        ret = nm->mkNode(cur.getKind(), children);
      }
      visited[cur] = ret;
    }
  } while (!visit.empty());
  Assert(visited.find(n) != visited.end());
  Assert(!visited.find(n)->second.isNull());
  return visited[n];
}

void LetBinding::updateCounts(Node n)
{
  NodeIdMap::iterator it;
  std::vector<Node> visit;
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    it = d_count.find(cur);
    if (it == d_count.end())
    {
      // do not traverse beneath quantifiers
      if (cur.getNumChildren() == 0 || cur.isClosure())
      {
        d_visitList.push_back(cur);
        d_count[cur] = 1;
        visit.pop_back();
      }
      else
      {
        d_count[cur] = 0;
        visit.insert(visit.end(), cur.begin(), cur.end());
      }
    }
    else
    {
      if ((*it).second == 0)
      {
        d_visitList.push_back(cur);
      }
      d_count[cur] = (*it).second + 1;
      visit.pop_back();
    }
  } while (!visit.empty());
}

void LetBinding::convertCountToLet()
{
  Assert(d_thresh > 0);
  // Assign ids for those whose d_count is >= d_thresh, traverse in d_visitList
  // in order so that deeper nodes are assigned lower identifiers, which
  // ensures the let list can be printed.
  NodeIdMap::const_iterator itc;
  for (const Node& n : d_visitList)
  {
    if (n.getNumChildren() == 0)
    {
      // do not letify terms with no children
      continue;
    }
    else if (d_letMap.find(n) != d_letMap.end())
    {
      // already letified, perhaps at a lower context
      continue;
    }
    itc = d_count.find(n);
    Assert(itc != d_count.end());
    if ((*itc).second >= d_thresh)
    {
      d_letList.push_back(n);
      // start with id 1
      size_t id = d_letMap.size() + 1;
      d_letMap[n] = id;
    }
  }
}

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds
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 let binding utility.
14		*/
15
16		#include "printer/let_binding.h"
17
18		#include <sstream>
19
20		namespace cvc5 {
21
22	57511	LetBinding::LetBinding(uint32_t thresh)
23		: d_thresh(thresh),
24		d_context(),
25		d_visitList(&d_context),
26		d_count(&d_context),
27		d_letList(&d_context),
28	57511	d_letMap(&d_context)
29		{
30	57511	}
31
32	47	uint32_t LetBinding::getThreshold() const { return d_thresh; }
33
34	57511	void LetBinding::process(Node n)
35		{
36	57511	if (n.isNull() \|\| d_thresh == 0)
37		{
38		// value of 0 means do not introduce let
39		return;
40		}
41		// update the count of occurrences
42	57511	updateCounts(n);
43		}
44
45	57511	void LetBinding::letify(Node n, std::vector<Node>& letList)
46		{
47		// first, push the context
48	57511	pushScope();
49		// process the node
50	57511	process(n);
51		// now, letify
52	57511	letify(letList);
53	57511	}
54
55	57511	void LetBinding::letify(std::vector<Node>& letList)
56		{
57	57511	size_t prevSize = d_letList.size();
58		// populate the d_letList and d_letMap
59	57511	convertCountToLet();
60		// add the new entries to the letList
61	57511	letList.insert(letList.end(), d_letList.begin() + prevSize, d_letList.end());
62	57511	}
63
64	57511	void LetBinding::pushScope() { d_context.push(); }
65
66	57497	void LetBinding::popScope() { d_context.pop(); }
67
68	1638064	uint32_t LetBinding::getId(Node n) const
69		{
70	1638064	NodeIdMap::const_iterator it = d_letMap.find(n);
71	1638064	if (it == d_letMap.end())
72		{
73	1217171	return 0;
74		}
75	420893	return (*it).second;
76		}
77
78	178764	Node LetBinding::convert(Node n, const std::string& prefix, bool letTop) const
79		{
80	178764	if (d_letMap.empty())
81		{
82	14984	return n;
83		}
84	163780	NodeManager* nm = NodeManager::currentNM();
85	327560	std::unordered_map<TNode, Node> visited;
86	163780	std::unordered_map<TNode, Node>::iterator it;
87	327560	std::vector<TNode> visit;
88	327560	TNode cur;
89	163780	visit.push_back(n);
90	3144354	do
91		{
92	3308134	cur = visit.back();
93	3308134	visit.pop_back();
94	3308134	it = visited.find(cur);
95
96	3308134	if (it == visited.end())
97		{
98	1516811	uint32_t id = getId(cur);
99		// do not letify id 0, or n itself if letTop is false
100	1516811	if (id > 0 && (cur != n \|\| letTop))
101		{
102		// make the let variable
103	356774	std::stringstream ss;
104	178387	ss << prefix << id;
105	178387	visited[cur] = nm->mkBoundVar(ss.str(), cur.getType());
106		}
107	1338424	else if (cur.isClosure())
108		{
109		// do not convert beneath quantifiers
110	9	visited[cur] = cur;
111		}
112		else
113		{
114	1338415	visited[cur] = Node::null();
115	1338415	visit.push_back(cur);
116	1338415	visit.insert(visit.end(), cur.begin(), cur.end());
117		}
118		}
119	1791323	else if (it->second.isNull())
120		{
121	2676830	Node ret = cur;
122	1338415	bool childChanged = false;
123	2676830	std::vector<Node> children;
124	1338415	if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
125		{
126	43972	children.push_back(cur.getOperator());
127		}
128	3144354	for (const Node& cn : cur)
129		{
130	1805939	it = visited.find(cn);
131	1805939	Assert(it != visited.end());
132	1805939	Assert(!it->second.isNull());
133	1805939	childChanged = childChanged \|\| cn != it->second;
134	1805939	children.push_back(it->second);
135		}
136	1338415	if (childChanged)
137		{
138	575927	ret = nm->mkNode(cur.getKind(), children);
139		}
140	1338401	visited[cur] = ret;
141		}
142	3308120	} while (!visit.empty());
143	163766	Assert(visited.find(n) != visited.end());
144	163766	Assert(!visited.find(n)->second.isNull());
145	163766	return visited[n];
146		}
147
148	57511	void LetBinding::updateCounts(Node n)
149		{
150	57511	NodeIdMap::iterator it;
151	115022	std::vector<Node> visit;
152	115022	TNode cur;
153	57511	visit.push_back(n);
154	2622040	do
155		{
156	2679551	cur = visit.back();
157	2679551	it = d_count.find(cur);
158	2679551	if (it == d_count.end())
159		{
160		// do not traverse beneath quantifiers
161	1299790	if (cur.getNumChildren() == 0 \|\| cur.isClosure())
162		{
163	496451	d_visitList.push_back(cur);
164	496451	d_count[cur] = 1;
165	496451	visit.pop_back();
166		}
167		else
168		{
169	803339	d_count[cur] = 0;
170	803339	visit.insert(visit.end(), cur.begin(), cur.end());
171		}
172		}
173		else
174		{
175	1379761	if ((*it).second == 0)
176		{
177	803339	d_visitList.push_back(cur);
178		}
179	1379761	d_count[cur] = (*it).second + 1;
180	1379761	visit.pop_back();
181		}
182	2679551	} while (!visit.empty());
183	57511	}
184
185	57511	void LetBinding::convertCountToLet()
186		{
187	57511	Assert(d_thresh > 0);
188		// Assign ids for those whose d_count is >= d_thresh, traverse in d_visitList
189		// in order so that deeper nodes are assigned lower identifiers, which
190		// ensures the let list can be printed.
191	57511	NodeIdMap::const_iterator itc;
192	1357301	for (const Node& n : d_visitList)
193		{
194	1299790	if (n.getNumChildren() == 0)
195		{
196		// do not letify terms with no children
197	496409	continue;
198		}
199	803381	else if (d_letMap.find(n) != d_letMap.end())
200		{
201		// already letified, perhaps at a lower context
202		continue;
203		}
204	803381	itc = d_count.find(n);
205	803381	Assert(itc != d_count.end());
206	803381	if ((*itc).second >= d_thresh)
207		{
208	121253	d_letList.push_back(n);
209		// start with id 1
210	121253	size_t id = d_letMap.size() + 1;
211	121253	d_letMap[n] = id;
212		}
213		}
214	57511	}
215
216	29502	} // namespace cvc5