Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/node_converter.h	Lines:	0	1	0.0 %
Date:	2021-09-06	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.
   */
  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		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		Node convert(Node n);
51
52		/**
53		* This converts type node n based on the preConvertType/postConvertType
54		* methods that can be overriden by instances of this class.
55		*/
56		TypeNode convertType(TypeNode tn);
57
58		protected:
59		//------------------------- virtual interface
60		/** Should we traverse n? */
61		virtual bool shouldTraverse(Node n);
62		/**
63		* Run the conversion for n during pre-order traversal.
64		* Returning null is equivalent to saying the node should not be changed.
65		*/
66		virtual Node preConvert(Node n);
67		/**
68		* Run the conversion for post-order traversal, where notice n is a term
69		* of the form:
70		* (f i_1 ... i_m)
71		* where i_1, ..., i_m are terms that have been returned by previous calls
72		* to postConvert.
73		*
74		* Returning null is equivalent to saying the node should not be changed.
75		*/
76		virtual Node postConvert(Node n);
77		/**
78		* Run the conversion, same as `preConvert`, but for type nodes, which notice
79		* can be built from children similar to Node.
80		*/
81		virtual TypeNode preConvertType(TypeNode n);
82		/**
83		* Run the conversion, same as `postConvert`, but for type nodes, which notice
84		* can be built from children similar to Node.
85		*/
86		virtual TypeNode postConvertType(TypeNode n);
87		//------------------------- end virtual interface
88		private:
89		/** Add to cache */
90		void addToCache(TNode cur, TNode ret);
91		/** Add to type cache */
92		void addToTypeCache(TypeNode cur, TypeNode ret);
93		/** Node cache for preConvert */
94		std::unordered_map<Node, Node> d_preCache;
95		/** Node cache for postConvert */
96		std::unordered_map<Node, Node> d_cache;
97		/** TypeNode cache for preConvert */
98		std::unordered_map<TypeNode, TypeNode> d_preTCache;
99		/** TypeNode cache for postConvert */
100		std::unordered_map<TypeNode, TypeNode> d_tcache;
101		/** Whether this node converter is idempotent. */
102		bool d_forceIdem;
103		};
104
105		} // namespace cvc5
106
107		#endif