Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/printer/let_binding.cpp	Lines:	103	105	98.1 %
Date:	2021-08-16	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	52797	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	52797	d_letMap(&d_context)
29		{
30	52797	}
31
32	47	uint32_t LetBinding::getThreshold() const { return d_thresh; }
33
34	52797	void LetBinding::process(Node n)
35		{
36	52797	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	52797	updateCounts(n);
43		}
44
45	52797	void LetBinding::letify(Node n, std::vector<Node>& letList)
46		{
47		// first, push the context
48	52797	pushScope();
49		// process the node
50	52797	process(n);
51		// now, letify
52	52797	letify(letList);
53	52797	}
54
55	52797	void LetBinding::letify(std::vector<Node>& letList)
56		{
57	52797	size_t prevSize = d_letList.size();
58		// populate the d_letList and d_letMap
59	52797	convertCountToLet();
60		// add the new entries to the letList
61	52797	letList.insert(letList.end(), d_letList.begin() + prevSize, d_letList.end());
62	52797	}
63
64	52797	void LetBinding::pushScope() { d_context.push(); }
65
66	52783	void LetBinding::popScope() { d_context.pop(); }
67
68	1445352	uint32_t LetBinding::getId(Node n) const
69		{
70	1445352	NodeIdMap::const_iterator it = d_letMap.find(n);
71	1445352	if (it == d_letMap.end())
72		{
73	1076182	return 0;
74		}
75	369170	return (*it).second;
76		}
77
78	159426	Node LetBinding::convert(Node n, const std::string& prefix, bool letTop) const
79		{
80	159426	if (d_letMap.empty())
81		{
82	14818	return n;
83		}
84	144608	NodeManager* nm = NodeManager::currentNM();
85	289216	std::unordered_map<TNode, Node> visited;
86	144608	std::unordered_map<TNode, Node>::iterator it;
87	289216	std::vector<TNode> visit;
88	289216	TNode cur;
89	144608	visit.push_back(n);
90	2774917	do
91		{
92	2919525	cur = visit.back();
93	2919525	visit.pop_back();
94	2919525	it = visited.find(cur);
95
96	2919525	if (it == visited.end())
97		{
98	1338723	uint32_t id = getId(cur);
99		// do not letify id 0, or n itself if letTop is false
100	1338723	if (id > 0 && (cur != n \|\| letTop))
101		{
102		// make the let variable
103	311824	std::stringstream ss;
104	155912	ss << prefix << id;
105	155912	visited[cur] = nm->mkBoundVar(ss.str(), cur.getType());
106		}
107	1182811	else if (cur.isClosure())
108		{
109		// do not convert beneath quantifiers
110	9	visited[cur] = cur;
111		}
112		else
113		{
114	1182802	visited[cur] = Node::null();
115	1182802	visit.push_back(cur);
116	1182802	visit.insert(visit.end(), cur.begin(), cur.end());
117		}
118		}
119	1580802	else if (it->second.isNull())
120		{
121	2365604	Node ret = cur;
122	1182802	bool childChanged = false;
123	2365604	std::vector<Node> children;
124	1182802	if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
125		{
126	45401	children.push_back(cur.getOperator());
127		}
128	2774917	for (const Node& cn : cur)
129		{
130	1592115	it = visited.find(cn);
131	1592115	Assert(it != visited.end());
132	1592115	Assert(!it->second.isNull());
133	1592115	childChanged = childChanged \|\| cn != it->second;
134	1592115	children.push_back(it->second);
135		}
136	1182802	if (childChanged)
137		{
138	505038	ret = nm->mkNode(cur.getKind(), children);
139		}
140	1182788	visited[cur] = ret;
141		}
142	2919511	} while (!visit.empty());
143	144594	Assert(visited.find(n) != visited.end());
144	144594	Assert(!visited.find(n)->second.isNull());
145	144594	return visited[n];
146		}
147
148	52797	void LetBinding::updateCounts(Node n)
149		{
150	52797	NodeIdMap::iterator it;
151	105594	std::vector<Node> visit;
152	105594	TNode cur;
153	52797	visit.push_back(n);
154	2313795	do
155		{
156	2366592	cur = visit.back();
157	2366592	it = d_count.find(cur);
158	2366592	if (it == d_count.end())
159		{
160		// do not traverse beneath quantifiers
161	1149540	if (cur.getNumChildren() == 0 \|\| cur.isClosure())
162		{
163	440622	d_visitList.push_back(cur);
164	440622	d_count[cur] = 1;
165	440622	visit.pop_back();
166		}
167		else
168		{
169	708918	d_count[cur] = 0;
170	708918	visit.insert(visit.end(), cur.begin(), cur.end());
171		}
172		}
173		else
174		{
175	1217052	if ((*it).second == 0)
176		{
177	708918	d_visitList.push_back(cur);
178		}
179	1217052	d_count[cur] = (*it).second + 1;
180	1217052	visit.pop_back();
181		}
182	2366592	} while (!visit.empty());
183	52797	}
184
185	52797	void LetBinding::convertCountToLet()
186		{
187	52797	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	52797	NodeIdMap::const_iterator itc;
192	1202337	for (const Node& n : d_visitList)
193		{
194	1149540	if (n.getNumChildren() == 0)
195		{
196		// do not letify terms with no children
197	440580	continue;
198		}
199	708960	else if (d_letMap.find(n) != d_letMap.end())
200		{
201		// already letified, perhaps at a lower context
202		continue;
203		}
204	708960	itc = d_count.find(n);
205	708960	Assert(itc != d_count.end());
206	708960	if ((*itc).second >= d_thresh)
207		{
208	106629	d_letList.push_back(n);
209		// start with id 1
210	106629	size_t id = d_letMap.size() + 1;
211	106629	d_letMap[n] = id;
212		}
213		}
214	52797	}
215
216	29340	} // namespace cvc5