Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/node_converter.cpp	Lines:	127	149	85.2 %
Date:	2021-11-07	Branches:	272	826	32.9 %


/******************************************************************************
 * 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.
 * ****************************************************************************
 *
 * Node converter utility
 */

#include "expr/node_converter.h"

#include "expr/attribute.h"

using namespace cvc5::kind;

namespace cvc5 {

NodeConverter::NodeConverter(bool forceIdem) : d_forceIdem(forceIdem) {}

Node NodeConverter::convert(Node n)
{
  if (n.isNull())
  {
    return n;
  }
  Trace("nconv-debug") << "NodeConverter::convert: " << n << std::endl;
  NodeManager* nm = NodeManager::currentNM();
  std::unordered_map<Node, Node>::iterator it;
  std::vector<TNode> visit;
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();
    it = d_cache.find(cur);
    Trace("nconv-debug2") << "convert " << cur << std::endl;
    if (it == d_cache.end())
    {
      d_cache[cur] = Node::null();
      Assert(d_preCache.find(cur) == d_preCache.end());
      Node curp = preConvert(cur);
      // If curp = cur, then we did not pre-rewrite. Hence, we should not
      // revisit cur, and instead set curp to null.
      curp = curp == cur ? Node::null() : curp;
      d_preCache[cur] = curp;
      if (!curp.isNull())
      {
        Trace("nconv-debug2")
            << "..pre-rewrite changed " << cur << " into " << curp << std::endl;
        visit.push_back(cur);
        visit.push_back(curp);
      }
      else
      {
        if (!shouldTraverse(cur))
        {
          addToCache(cur, cur);
        }
        else
        {
          visit.push_back(cur);
          if (cur.getMetaKind() == metakind::PARAMETERIZED)
          {
            visit.push_back(cur.getOperator());
          }
          visit.insert(visit.end(), cur.begin(), cur.end());
        }
      }
    }
    else if (it->second.isNull())
    {
      Trace("nconv-debug2") << "..post-visit " << cur << std::endl;
      it = d_preCache.find(cur);
      Assert(it != d_preCache.end());
      if (!it->second.isNull())
      {
        // it converts to what its prewrite converts to
        Assert(d_cache.find(it->second) != d_cache.end());
        Node ret = d_cache[it->second];
        addToCache(cur, ret);
        Trace("nconv-debug2")
            << "..from cache changed " << cur << " into " << ret << std::endl;
      }
      else
      {
        Node ret = cur;
        bool childChanged = false;
        std::vector<Node> children;
        if (ret.getMetaKind() == metakind::PARAMETERIZED)
        {
          it = d_cache.find(ret.getOperator());
          Assert(it != d_cache.end());
          Assert(!it->second.isNull());
          childChanged = childChanged || ret.getOperator() != it->second;
          children.push_back(it->second);
        }
        for (const Node& cn : ret)
        {
          it = d_cache.find(cn);
          Assert(it != d_cache.end());
          Assert(!it->second.isNull());
          childChanged = childChanged || cn != it->second;
          children.push_back(it->second);
        }
        if (childChanged)
        {
          ret = nm->mkNode(ret.getKind(), children);
          Trace("nconv-debug2") << "..from children changed " << cur << " into "
                                << ret << std::endl;
        }
        // run the callback for the current application
        Node cret = postConvert(ret);
        if (!cret.isNull() && ret != cret)
        {
          AlwaysAssert(cret.getType().isComparableTo(ret.getType()))
              << "Converting " << ret << " to " << cret << " changes type";
          Trace("nconv-debug2") << "..post-rewrite changed " << ret << " into "
                                << cret << std::endl;
          ret = cret;
        }
        addToCache(cur, ret);
      }
    }
  } while (!visit.empty());
  Assert(d_cache.find(n) != d_cache.end());
  Assert(!d_cache.find(n)->second.isNull());
  return d_cache[n];
}

TypeNode NodeConverter::convertType(TypeNode tn)
{
  if (tn.isNull())
  {
    return tn;
  }
  Trace("nconv-debug") << "NodeConverter::convertType: " << tn << std::endl;
  std::unordered_map<TypeNode, TypeNode>::iterator it;
  std::vector<TypeNode> visit;
  TypeNode cur;
  visit.push_back(tn);
  do
  {
    cur = visit.back();
    visit.pop_back();
    it = d_tcache.find(cur);
    Trace("nconv-debug2") << "convert type " << cur << std::endl;
    if (it == d_tcache.end())
    {
      d_tcache[cur] = TypeNode::null();
      Assert(d_preTCache.find(cur) == d_preTCache.end());
      TypeNode curp = preConvertType(cur);
      // if curp = cur, set null to avoid infinite loop
      curp = curp == cur ? TypeNode::null() : curp;
      d_preTCache[cur] = curp;
      if (!curp.isNull())
      {
        visit.push_back(cur);
        visit.push_back(curp);
      }
      else
      {
        curp = curp.isNull() ? cur : curp;
        if (cur.getNumChildren() == 0)
        {
          TypeNode ret = postConvertType(cur);
          addToTypeCache(cur, ret);
        }
        else
        {
          visit.push_back(cur);
          visit.insert(visit.end(), cur.begin(), cur.end());
        }
      }
    }
    else if (it->second.isNull())
    {
      it = d_preTCache.find(cur);
      Assert(it != d_preTCache.end());
      if (!it->second.isNull())
      {
        // it converts to what its prewrite converts to
        Assert(d_tcache.find(it->second) != d_tcache.end());
        TypeNode ret = d_tcache[it->second];
        addToTypeCache(cur, ret);
      }
      else
      {
        TypeNode ret = cur;
        // reconstruct using a node builder, which seems to be required for
        // type nodes.
        NodeBuilder nb(ret.getKind());
        if (ret.getMetaKind() == kind::metakind::PARAMETERIZED)
        {
          // push the operator
          nb << ret.getOperator();
        }
        for (TypeNode::const_iterator j = ret.begin(), iend = ret.end();
             j != iend;
             ++j)
        {
          it = d_tcache.find(*j);
          Assert(it != d_tcache.end());
          Assert(!it->second.isNull());
          nb << it->second;
        }
        // construct the type node
        ret = nb.constructTypeNode();
        Trace("nconv-debug") << cur << " <- " << ret << std::endl;
        // run the callback for the current application
        TypeNode cret = postConvertType(ret);
        if (!cret.isNull())
        {
          ret = cret;
        }
        Trace("nconv-debug")
            << cur << " <- " << ret << " (post-convert)" << std::endl;
        addToTypeCache(cur, ret);
      }
    }
  } while (!visit.empty());
  Assert(d_tcache.find(tn) != d_tcache.end());
  Assert(!d_tcache.find(tn)->second.isNull());
  Trace("nconv-debug") << "NodeConverter::convertType: returns " << d_tcache[tn]
                       << std::endl;
  return d_tcache[tn];
}

void NodeConverter::addToCache(TNode cur, TNode ret)
{
  d_cache[cur] = ret;
  // also force idempotency, if specified
  if (d_forceIdem)
  {
    d_cache[ret] = ret;
  }
}
void NodeConverter::addToTypeCache(TypeNode cur, TypeNode ret)
{
  d_tcache[cur] = ret;
  // also force idempotency, if specified
  if (d_forceIdem)
  {
    d_tcache[ret] = ret;
  }
}

Node NodeConverter::preConvert(Node n) { return Node::null(); }
Node NodeConverter::postConvert(Node n) { return Node::null(); }

TypeNode NodeConverter::preConvertType(TypeNode tn) { return TypeNode::null(); }
TypeNode NodeConverter::postConvertType(TypeNode tn)
{
  return TypeNode::null();
}
bool NodeConverter::shouldTraverse(Node n) { return true; }

}  // 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		* Node converter utility
14		*/
15
16		#include "expr/node_converter.h"
17
18		#include "expr/attribute.h"
19
20		using namespace cvc5::kind;
21
22		namespace cvc5 {
23
24	1	NodeConverter::NodeConverter(bool forceIdem) : d_forceIdem(forceIdem) {}
25
26	144	Node NodeConverter::convert(Node n)
27		{
28	144	if (n.isNull())
29		{
30		return n;
31		}
32	144	Trace("nconv-debug") << "NodeConverter::convert: " << n << std::endl;
33	144	NodeManager* nm = NodeManager::currentNM();
34	144	std::unordered_map<Node, Node>::iterator it;
35	288	std::vector<TNode> visit;
36	288	TNode cur;
37	144	visit.push_back(n);
38	209	do
39		{
40	353	cur = visit.back();
41	353	visit.pop_back();
42	353	it = d_cache.find(cur);
43	353	Trace("nconv-debug2") << "convert " << cur << std::endl;
44	353	if (it == d_cache.end())
45		{
46	80	d_cache[cur] = Node::null();
47	80	Assert(d_preCache.find(cur) == d_preCache.end());
48	160	Node curp = preConvert(cur);
49		// If curp = cur, then we did not pre-rewrite. Hence, we should not
50		// revisit cur, and instead set curp to null.
51	80	curp = curp == cur ? Node::null() : curp;
52	80	d_preCache[cur] = curp;
53	80	if (!curp.isNull())
54		{
55		Trace("nconv-debug2")
56		<< "..pre-rewrite changed " << cur << " into " << curp << std::endl;
57		visit.push_back(cur);
58		visit.push_back(curp);
59		}
60		else
61		{
62	80	if (!shouldTraverse(cur))
63		{
64		addToCache(cur, cur);
65		}
66		else
67		{
68	80	visit.push_back(cur);
69	80	if (cur.getMetaKind() == metakind::PARAMETERIZED)
70		{
71	2	visit.push_back(cur.getOperator());
72		}
73	80	visit.insert(visit.end(), cur.begin(), cur.end());
74		}
75		}
76		}
77	273	else if (it->second.isNull())
78		{
79	80	Trace("nconv-debug2") << "..post-visit " << cur << std::endl;
80	80	it = d_preCache.find(cur);
81	80	Assert(it != d_preCache.end());
82	80	if (!it->second.isNull())
83		{
84		// it converts to what its prewrite converts to
85		Assert(d_cache.find(it->second) != d_cache.end());
86		Node ret = d_cache[it->second];
87		addToCache(cur, ret);
88		Trace("nconv-debug2")
89		<< "..from cache changed " << cur << " into " << ret << std::endl;
90		}
91		else
92		{
93	160	Node ret = cur;
94	80	bool childChanged = false;
95	160	std::vector<Node> children;
96	80	if (ret.getMetaKind() == metakind::PARAMETERIZED)
97		{
98	2	it = d_cache.find(ret.getOperator());
99	2	Assert(it != d_cache.end());
100	2	Assert(!it->second.isNull());
101	2	childChanged = childChanged \|\| ret.getOperator() != it->second;
102	2	children.push_back(it->second);
103		}
104	207	for (const Node& cn : ret)
105		{
106	127	it = d_cache.find(cn);
107	127	Assert(it != d_cache.end());
108	127	Assert(!it->second.isNull());
109	127	childChanged = childChanged \|\| cn != it->second;
110	127	children.push_back(it->second);
111		}
112	80	if (childChanged)
113		{
114	63	ret = nm->mkNode(ret.getKind(), children);
115	126	Trace("nconv-debug2") << "..from children changed " << cur << " into "
116	63	<< ret << std::endl;
117		}
118		// run the callback for the current application
119	160	Node cret = postConvert(ret);
120	80	if (!cret.isNull() && ret != cret)
121		{
122	84	AlwaysAssert(cret.getType().isComparableTo(ret.getType()))
123	42	<< "Converting " << ret << " to " << cret << " changes type";
124	84	Trace("nconv-debug2") << "..post-rewrite changed " << ret << " into "
125	42	<< cret << std::endl;
126	42	ret = cret;
127		}
128	80	addToCache(cur, ret);
129		}
130		}
131	353	} while (!visit.empty());
132	144	Assert(d_cache.find(n) != d_cache.end());
133	144	Assert(!d_cache.find(n)->second.isNull());
134	144	return d_cache[n];
135		}
136
137	6	TypeNode NodeConverter::convertType(TypeNode tn)
138		{
139	6	if (tn.isNull())
140		{
141		return tn;
142		}
143	6	Trace("nconv-debug") << "NodeConverter::convertType: " << tn << std::endl;
144	6	std::unordered_map<TypeNode, TypeNode>::iterator it;
145	12	std::vector<TypeNode> visit;
146	12	TypeNode cur;
147	6	visit.push_back(tn);
148	3	do
149		{
150	9	cur = visit.back();
151	9	visit.pop_back();
152	9	it = d_tcache.find(cur);
153	9	Trace("nconv-debug2") << "convert type " << cur << std::endl;
154	9	if (it == d_tcache.end())
155		{
156	3	d_tcache[cur] = TypeNode::null();
157	3	Assert(d_preTCache.find(cur) == d_preTCache.end());
158	6	TypeNode curp = preConvertType(cur);
159		// if curp = cur, set null to avoid infinite loop
160	3	curp = curp == cur ? TypeNode::null() : curp;
161	3	d_preTCache[cur] = curp;
162	3	if (!curp.isNull())
163		{
164		visit.push_back(cur);
165		visit.push_back(curp);
166		}
167		else
168		{
169	3	curp = curp.isNull() ? cur : curp;
170	3	if (cur.getNumChildren() == 0)
171		{
172	4	TypeNode ret = postConvertType(cur);
173	2	addToTypeCache(cur, ret);
174		}
175		else
176		{
177	1	visit.push_back(cur);
178	1	visit.insert(visit.end(), cur.begin(), cur.end());
179		}
180		}
181		}
182	6	else if (it->second.isNull())
183		{
184	1	it = d_preTCache.find(cur);
185	1	Assert(it != d_preTCache.end());
186	1	if (!it->second.isNull())
187		{
188		// it converts to what its prewrite converts to
189		Assert(d_tcache.find(it->second) != d_tcache.end());
190		TypeNode ret = d_tcache[it->second];
191		addToTypeCache(cur, ret);
192		}
193		else
194		{
195	2	TypeNode ret = cur;
196		// reconstruct using a node builder, which seems to be required for
197		// type nodes.
198	2	NodeBuilder nb(ret.getKind());
199	1	if (ret.getMetaKind() == kind::metakind::PARAMETERIZED)
200		{
201		// push the operator
202		nb << ret.getOperator();
203		}
204	3	for (TypeNode::const_iterator j = ret.begin(), iend = ret.end();
205	3	j != iend;
206		++j)
207		{
208	2	it = d_tcache.find(*j);
209	2	Assert(it != d_tcache.end());
210	2	Assert(!it->second.isNull());
211	2	nb << it->second;
212		}
213		// construct the type node
214	1	ret = nb.constructTypeNode();
215	1	Trace("nconv-debug") << cur << " <- " << ret << std::endl;
216		// run the callback for the current application
217	2	TypeNode cret = postConvertType(ret);
218	1	if (!cret.isNull())
219		{
220	1	ret = cret;
221		}
222	2	Trace("nconv-debug")
223	1	<< cur << " <- " << ret << " (post-convert)" << std::endl;
224	1	addToTypeCache(cur, ret);
225		}
226		}
227	9	} while (!visit.empty());
228	6	Assert(d_tcache.find(tn) != d_tcache.end());
229	6	Assert(!d_tcache.find(tn)->second.isNull());
230	12	Trace("nconv-debug") << "NodeConverter::convertType: returns " << d_tcache[tn]
231	6	<< std::endl;
232	6	return d_tcache[tn];
233		}
234
235	80	void NodeConverter::addToCache(TNode cur, TNode ret)
236		{
237	80	d_cache[cur] = ret;
238		// also force idempotency, if specified
239	80	if (d_forceIdem)
240		{
241	80	d_cache[ret] = ret;
242		}
243	80	}
244	3	void NodeConverter::addToTypeCache(TypeNode cur, TypeNode ret)
245		{
246	3	d_tcache[cur] = ret;
247		// also force idempotency, if specified
248	3	if (d_forceIdem)
249		{
250	3	d_tcache[ret] = ret;
251		}
252	3	}
253
254	80	Node NodeConverter::preConvert(Node n) { return Node::null(); }
255		Node NodeConverter::postConvert(Node n) { return Node::null(); }
256
257	3	TypeNode NodeConverter::preConvertType(TypeNode tn) { return TypeNode::null(); }
258		TypeNode NodeConverter::postConvertType(TypeNode tn)
259		{
260		return TypeNode::null();
261		}
262		bool NodeConverter::shouldTraverse(Node n) { return true; }
263
264	31137	} // namespace cvc5