Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/node_converter.h	Lines:	1	1	100.0 %
Date:	2021-11-05	Branches:	0	0	0.0 %


/******************************************************************************
 * 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 "cvc5_private.h"

#ifndef CVC4__EXPR__NODE_CONVERTER_H
#define CVC4__EXPR__NODE_CONVERTER_H

#include <iostream>
#include <map>

#include "expr/node.h"
#include "expr/type_node.h"

namespace cvc5 {

/**
 * A node converter for terms and types. Implements term/type traversals,
 * calling the provided implementations of conversion methods (pre/postConvert
 * and pre/postConvertType) at pre-traversal and post-traversal.
 *
 * This class can be used as a generic method for converting terms/types, which
 * is orthogonal to methods for traversing nodes.
 */
class NodeConverter
{
 public:
  /**
   * @param forceIdem If true, this assumes that terms returned by postConvert
   * and postConvertType should not be converted again.
   */
  NodeConverter(bool forceIdem = true);
  virtual ~NodeConverter() {}
  /**
   * This converts node n based on the preConvert/postConvert methods that can
   * be overriden by instances of this class.
   *
   * If n is null, this always returns the null node.
   */
  Node convert(Node n);

  /**
   * This converts type node n based on the preConvertType/postConvertType
   * methods that can be overriden by instances of this class.
   */
  TypeNode convertType(TypeNode tn);

 protected:
  //------------------------- virtual interface
  /** Should we traverse n? */
  virtual bool shouldTraverse(Node n);
  /**
   * Run the conversion for n during pre-order traversal.
   * Returning null is equivalent to saying the node should not be changed.
   */
  virtual Node preConvert(Node n);
  /**
   * Run the conversion for post-order traversal, where notice n is a term
   * of the form:
   *   (f i_1 ... i_m)
   * where i_1, ..., i_m are terms that have been returned by previous calls
   * to postConvert.
   *
   * Returning null is equivalent to saying the node should not be changed.
   */
  virtual Node postConvert(Node n);
  /**
   * Run the conversion, same as `preConvert`, but for type nodes, which notice
   * can be built from children similar to Node.
   */
  virtual TypeNode preConvertType(TypeNode n);
  /**
   * Run the conversion, same as `postConvert`, but for type nodes, which notice
   * can be built from children similar to Node.
   */
  virtual TypeNode postConvertType(TypeNode n);
  //------------------------- end virtual interface
 private:
  /** Add to cache */
  void addToCache(TNode cur, TNode ret);
  /** Add to type cache */
  void addToTypeCache(TypeNode cur, TypeNode ret);
  /** Node cache for preConvert */
  std::unordered_map<Node, Node> d_preCache;
  /** Node cache for postConvert */
  std::unordered_map<Node, Node> d_cache;
  /** TypeNode cache for preConvert */
  std::unordered_map<TypeNode, TypeNode> d_preTCache;
  /** TypeNode cache for postConvert */
  std::unordered_map<TypeNode, TypeNode> d_tcache;
  /** Whether this node converter is idempotent. */
  bool d_forceIdem;
};

}  // namespace cvc5

#endif


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 "cvc5_private.h"
17
18		#ifndef CVC4__EXPR__NODE_CONVERTER_H
19		#define CVC4__EXPR__NODE_CONVERTER_H
20
21		#include <iostream>
22		#include <map>
23
24		#include "expr/node.h"
25		#include "expr/type_node.h"
26
27		namespace cvc5 {
28
29		/**
30		* A node converter for terms and types. Implements term/type traversals,
31		* calling the provided implementations of conversion methods (pre/postConvert
32		* and pre/postConvertType) at pre-traversal and post-traversal.
33		*
34		* This class can be used as a generic method for converting terms/types, which
35		* is orthogonal to methods for traversing nodes.
36		*/
37		class NodeConverter
38		{
39		public:
40		/**
41		* @param forceIdem If true, this assumes that terms returned by postConvert
42		* and postConvertType should not be converted again.
43		*/
44		NodeConverter(bool forceIdem = true);
45	1	virtual ~NodeConverter() {}
46		/**
47		* This converts node n based on the preConvert/postConvert methods that can
48		* be overriden by instances of this class.
49		*
50		* If n is null, this always returns the null node.
51		*/
52		Node convert(Node n);
53
54		/**
55		* This converts type node n based on the preConvertType/postConvertType
56		* methods that can be overriden by instances of this class.
57		*/
58		TypeNode convertType(TypeNode tn);
59
60		protected:
61		//------------------------- virtual interface
62		/** Should we traverse n? */
63		virtual bool shouldTraverse(Node n);
64		/**
65		* Run the conversion for n during pre-order traversal.
66		* Returning null is equivalent to saying the node should not be changed.
67		*/
68		virtual Node preConvert(Node n);
69		/**
70		* Run the conversion for post-order traversal, where notice n is a term
71		* of the form:
72		* (f i_1 ... i_m)
73		* where i_1, ..., i_m are terms that have been returned by previous calls
74		* to postConvert.
75		*
76		* Returning null is equivalent to saying the node should not be changed.
77		*/
78		virtual Node postConvert(Node n);
79		/**
80		* Run the conversion, same as `preConvert`, but for type nodes, which notice
81		* can be built from children similar to Node.
82		*/
83		virtual TypeNode preConvertType(TypeNode n);
84		/**
85		* Run the conversion, same as `postConvert`, but for type nodes, which notice
86		* can be built from children similar to Node.
87		*/
88		virtual TypeNode postConvertType(TypeNode n);
89		//------------------------- end virtual interface
90		private:
91		/** Add to cache */
92		void addToCache(TNode cur, TNode ret);
93		/** Add to type cache */
94		void addToTypeCache(TypeNode cur, TypeNode ret);
95		/** Node cache for preConvert */
96		std::unordered_map<Node, Node> d_preCache;
97		/** Node cache for postConvert */
98		std::unordered_map<Node, Node> d_cache;
99		/** TypeNode cache for preConvert */
100		std::unordered_map<TypeNode, TypeNode> d_preTCache;
101		/** TypeNode cache for postConvert */
102		std::unordered_map<TypeNode, TypeNode> d_tcache;
103		/** Whether this node converter is idempotent. */
104		bool d_forceIdem;
105		};
106
107		} // namespace cvc5
108
109		#endif