GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/printer/let_binding.cpp Lines: 103 105 98.1 %
Date: 2021-03-22 Branches: 169 364 46.4 %

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