Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/node_converter.cpp	Lines:	1	138	0.7 %
Date:	2021-08-01	Branches:	2	756	0.3 %


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