Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/printer/let_binding.cpp	Lines:	103	105	98.1 %
Date:	2021-05-21	Branches:	169	364	46.4 %


/******************************************************************************
 * 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	54063	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	54063	d_letMap(&d_context)
29		{
30	54063	}
31
32	41	uint32_t LetBinding::getThreshold() const { return d_thresh; }
33
34	54063	void LetBinding::process(Node n)
35		{
36	54063	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	54063	updateCounts(n);
43		}
44
45	54063	void LetBinding::letify(Node n, std::vector<Node>& letList)
46		{
47		// first, push the context
48	54063	pushScope();
49		// process the node
50	54063	process(n);
51		// now, letify
52	54063	letify(letList);
53	54063	}
54
55	54063	void LetBinding::letify(std::vector<Node>& letList)
56		{
57	54063	size_t prevSize = d_letList.size();
58		// populate the d_letList and d_letMap
59	54063	convertCountToLet();
60		// add the new entries to the letList
61	54063	letList.insert(letList.end(), d_letList.begin() + prevSize, d_letList.end());
62	54063	}
63
64	54063	void LetBinding::pushScope() { d_context.push(); }
65
66	54049	void LetBinding::popScope() { d_context.pop(); }
67
68	1254380	uint32_t LetBinding::getId(Node n) const
69		{
70	1254380	NodeIdMap::const_iterator it = d_letMap.find(n);
71	1254380	if (it == d_letMap.end())
72		{
73	936243	return 0;
74		}
75	318137	return (*it).second;
76		}
77
78	146479	Node LetBinding::convert(Node n, const std::string& prefix, bool letTop) const
79		{
80	146479	if (d_letMap.empty())
81		{
82	20951	return n;
83		}
84	125528	NodeManager* nm = NodeManager::currentNM();
85	251056	std::unordered_map<TNode, Node> visited;
86	125528	std::unordered_map<TNode, Node>::iterator it;
87	251056	std::vector<TNode> visit;
88	251056	TNode cur;
89	125528	visit.push_back(n);
90	2405154	do
91		{
92	2530682	cur = visit.back();
93	2530682	visit.pop_back();
94	2530682	it = visited.find(cur);
95
96	2530682	if (it == visited.end())
97		{
98	1161964	uint32_t id = getId(cur);
99		// do not letify id 0, or n itself if letTop is false
100	1161964	if (id > 0 && (cur != n \|\| letTop))
101		{
102		// make the let variable
103	266610	std::stringstream ss;
104	133305	ss << prefix << id;
105	133305	visited[cur] = nm->mkBoundVar(ss.str(), cur.getType());
106		}
107	1028659	else if (cur.isClosure())
108		{
109		// do not convert beneath quantifiers
110	9	visited[cur] = cur;
111		}
112		else
113		{
114	1028650	visited[cur] = Node::null();
115	1028650	visit.push_back(cur);
116	1028650	visit.insert(visit.end(), cur.begin(), cur.end());
117		}
118		}
119	1368718	else if (it->second.isNull())
120		{
121	2057300	Node ret = cur;
122	1028650	bool childChanged = false;
123	2057300	std::vector<Node> children;
124	1028650	if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
125		{
126	45295	children.push_back(cur.getOperator());
127		}
128	2405154	for (const Node& cn : cur)
129		{
130	1376504	it = visited.find(cn);
131	1376504	Assert(it != visited.end());
132	1376504	Assert(!it->second.isNull());
133	1376504	childChanged = childChanged \|\| cn != it->second;
134	1376504	children.push_back(it->second);
135		}
136	1028650	if (childChanged)
137		{
138	433717	ret = nm->mkNode(cur.getKind(), children);
139		}
140	1028636	visited[cur] = ret;
141		}
142	2530668	} while (!visit.empty());
143	125514	Assert(visited.find(n) != visited.end());
144	125514	Assert(!visited.find(n)->second.isNull());
145	125514	return visited[n];
146		}
147
148	54063	void LetBinding::updateCounts(Node n)
149		{
150	54063	NodeIdMap::iterator it;
151	108126	std::vector<Node> visit;
152	108126	TNode cur;
153	54063	visit.push_back(n);
154	2013410	do
155		{
156	2067473	cur = visit.back();
157	2067473	it = d_count.find(cur);
158	2067473	if (it == d_count.end())
159		{
160		// do not traverse beneath quantifiers
161	1012628	if (cur.getNumChildren() == 0 \|\| cur.isClosure())
162		{
163	394786	d_visitList.push_back(cur);
164	394786	d_count[cur] = 1;
165	394786	visit.pop_back();
166		}
167		else
168		{
169	617842	d_count[cur] = 0;
170	617842	visit.insert(visit.end(), cur.begin(), cur.end());
171		}
172		}
173		else
174		{
175	1054845	if ((*it).second == 0)
176		{
177	617842	d_visitList.push_back(cur);
178		}
179	1054845	d_count[cur] = (*it).second + 1;
180	1054845	visit.pop_back();
181		}
182	2067473	} while (!visit.empty());
183	54063	}
184
185	54063	void LetBinding::convertCountToLet()
186		{
187	54063	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	54063	NodeIdMap::const_iterator itc;
192	1066691	for (const Node& n : d_visitList)
193		{
194	1012628	if (n.getNumChildren() == 0)
195		{
196		// do not letify terms with no children
197	394750	continue;
198		}
199	617878	else if (d_letMap.find(n) != d_letMap.end())
200		{
201		// already letified, perhaps at a lower context
202		continue;
203		}
204	617878	itc = d_count.find(n);
205	617878	Assert(itc != d_count.end());
206	617878	if ((*itc).second >= d_thresh)
207		{
208	92416	d_letList.push_back(n);
209		// start with id 1
210	92416	size_t id = d_letMap.size() + 1;
211	92416	d_letMap[n] = id;
212		}
213		}
214	54063	}
215
216	27735	} // namespace cvc5