Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/term_canonize.h	Lines:	1	1	100.0 %
Date:	2021-11-07	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.
 * ****************************************************************************
 *
 * Utilities for constructing canonical terms.
 */

#include "cvc5_private.h"

#ifndef CVC5__EXPR__TERM_CANONIZE_H
#define CVC5__EXPR__TERM_CANONIZE_H

#include <map>
#include "expr/node.h"

namespace cvc5 {
namespace expr {

/**
 * Generalization of types. This class is a simple callback for giving
 * identifiers to variables that may be a more fine-grained way of classifying
 * the variable than its type. An example usage of type classes are for
 * distinguishing "list variables" for rewrite rule reconstruction.
 */
class TypeClassCallback
{
 public:
  TypeClassCallback() {}
  virtual ~TypeClassCallback() {}
  /** Return the type class for variable v */
  virtual uint32_t getTypeClass(TNode v) = 0;
};

/** TermCanonize
 *
 * This class contains utilities for canonizing terms with respect to
 * free variables (which are of kind BOUND_VARIABLE). For example, this
 * class infers that terms like f(BOUND_VARIABLE_1) and f(BOUND_VARIABLE_2)
 * are effectively the same term.
 */
class TermCanonize
{
 public:
  /**
   * @param tcc The type class callback. This class will canonize variables in
   * a way that disinguishes variables that are given different type class
   * identifiers. Otherwise, this class will assume all variables of the
   * same type have the same type class.
   */
  TermCanonize(TypeClassCallback* tcc = nullptr);
  ~TermCanonize() {}

  /** Maps operators to an identifier, useful for ordering. */
  int getIdForOperator(Node op);
  /** Maps types to an identifier, useful for ordering. */
  int getIdForType(TypeNode t);
  /** get term order
   *
   * Returns true if a <= b in the term ordering used by this class. The
   * term order is determined by the leftmost position in a and b whose
   * operators o_a and o_b are distinct at that position. Then a <= b iff
   * getIdForOperator( o_a ) <= getIdForOperator( o_b ).
   */
  bool getTermOrder(Node a, Node b);
  /** get canonical free variable #i of type tn */
  Node getCanonicalFreeVar(TypeNode tn, unsigned i, uint32_t tc = 0);
  /** get canonical term
   *
   * This returns a canonical (alpha-equivalent) version of n, where
   * bound variables in n may be replaced by other ones, and arguments of
   * commutative operators of n may be sorted (if apply_torder is true). If
   * doHoVar is true, we also canonicalize bound variables that occur in
   * operators.
   *
   * In detail, we replace bound variables in n so the the leftmost occurrence
   * of a bound variable for type T is the first canonical free variable for T,
   * the second leftmost is the second, and so on, for each type T.
   */
  Node getCanonicalTerm(TNode n,
                        bool apply_torder = false,
                        bool doHoVar = true);
  /**
   * Same as above but tracks visited map, mapping subterms of n to their
   * canonical forms.
   */
  Node getCanonicalTerm(TNode n,
                        std::map<TNode, Node>& visited,
                        bool apply_torder = false,
                        bool doHoVar = true);

 private:
  /** The (optional) type class callback */
  TypeClassCallback* d_tcc;
  /** the number of ids we have allocated for operators */
  int d_op_id_count;
  /** map from operators to id */
  std::map<Node, int> d_op_id;
  /** the number of ids we have allocated for types */
  int d_typ_id_count;
  /** map from type to id */
  std::map<TypeNode, int> d_typ_id;
  /** free variables for each type / type class pair */
  std::map<std::pair<TypeNode, uint32_t>, std::vector<Node> > d_cn_free_var;
  /**
   * Map from each free variable above to their index in their respective vector
   */
  std::map<Node, size_t> d_fvIndex;
  /** Get type class */
  uint32_t getTypeClass(TNode v);
  /**
   * Return the range of the free variable in the above map, or 0 if it does not
   * exist.
   */
  size_t getIndexForFreeVariable(Node v) const;
  /** get canonical term
   *
   * This is a helper function for getCanonicalTerm above. We maintain a
   * counter of how many variables we have allocated for each type (var_count),
   * and a cache of visited nodes (visited).
   */
  Node getCanonicalTerm(
      TNode n,
      bool apply_torder,
      bool doHoVar,
      std::map<std::pair<TypeNode, uint32_t>, unsigned>& var_count,
      std::map<TNode, Node>& visited);
};

}  // namespace expr
}  // namespace cvc5

#endif /* CVC5__EXPR__TERM_CANONIZE_H */


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		* Utilities for constructing canonical terms.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__EXPR__TERM_CANONIZE_H
19		#define CVC5__EXPR__TERM_CANONIZE_H
20
21		#include <map>
22		#include "expr/node.h"
23
24		namespace cvc5 {
25		namespace expr {
26
27		/**
28		* Generalization of types. This class is a simple callback for giving
29		* identifiers to variables that may be a more fine-grained way of classifying
30		* the variable than its type. An example usage of type classes are for
31		* distinguishing "list variables" for rewrite rule reconstruction.
32		*/
33		class TypeClassCallback
34		{
35		public:
36		TypeClassCallback() {}
37		virtual ~TypeClassCallback() {}
38		/** Return the type class for variable v */
39		virtual uint32_t getTypeClass(TNode v) = 0;
40		};
41
42		/** TermCanonize
43		*
44		* This class contains utilities for canonizing terms with respect to
45		* free variables (which are of kind BOUND_VARIABLE). For example, this
46		* class infers that terms like f(BOUND_VARIABLE_1) and f(BOUND_VARIABLE_2)
47		* are effectively the same term.
48		*/
49		class TermCanonize
50		{
51		public:
52		/**
53		* @param tcc The type class callback. This class will canonize variables in
54		* a way that disinguishes variables that are given different type class
55		* identifiers. Otherwise, this class will assume all variables of the
56		* same type have the same type class.
57		*/
58		TermCanonize(TypeClassCallback* tcc = nullptr);
59	12155	~TermCanonize() {}
60
61		/** Maps operators to an identifier, useful for ordering. */
62		int getIdForOperator(Node op);
63		/** Maps types to an identifier, useful for ordering. */
64		int getIdForType(TypeNode t);
65		/** get term order
66		*
67		* Returns true if a <= b in the term ordering used by this class. The
68		* term order is determined by the leftmost position in a and b whose
69		* operators o_a and o_b are distinct at that position. Then a <= b iff
70		* getIdForOperator( o_a ) <= getIdForOperator( o_b ).
71		*/
72		bool getTermOrder(Node a, Node b);
73		/** get canonical free variable #i of type tn */
74		Node getCanonicalFreeVar(TypeNode tn, unsigned i, uint32_t tc = 0);
75		/** get canonical term
76		*
77		* This returns a canonical (alpha-equivalent) version of n, where
78		* bound variables in n may be replaced by other ones, and arguments of
79		* commutative operators of n may be sorted (if apply_torder is true). If
80		* doHoVar is true, we also canonicalize bound variables that occur in
81		* operators.
82		*
83		* In detail, we replace bound variables in n so the the leftmost occurrence
84		* of a bound variable for type T is the first canonical free variable for T,
85		* the second leftmost is the second, and so on, for each type T.
86		*/
87		Node getCanonicalTerm(TNode n,
88		bool apply_torder = false,
89		bool doHoVar = true);
90		/**
91		* Same as above but tracks visited map, mapping subterms of n to their
92		* canonical forms.
93		*/
94		Node getCanonicalTerm(TNode n,
95		std::map<TNode, Node>& visited,
96		bool apply_torder = false,
97		bool doHoVar = true);
98
99		private:
100		/** The (optional) type class callback */
101		TypeClassCallback* d_tcc;
102		/** the number of ids we have allocated for operators */
103		int d_op_id_count;
104		/** map from operators to id */
105		std::map<Node, int> d_op_id;
106		/** the number of ids we have allocated for types */
107		int d_typ_id_count;
108		/** map from type to id */
109		std::map<TypeNode, int> d_typ_id;
110		/** free variables for each type / type class pair */
111		std::map<std::pair<TypeNode, uint32_t>, std::vector<Node> > d_cn_free_var;
112		/**
113		* Map from each free variable above to their index in their respective vector
114		*/
115		std::map<Node, size_t> d_fvIndex;
116		/** Get type class */
117		uint32_t getTypeClass(TNode v);
118		/**
119		* Return the range of the free variable in the above map, or 0 if it does not
120		* exist.
121		*/
122		size_t getIndexForFreeVariable(Node v) const;
123		/** get canonical term
124		*
125		* This is a helper function for getCanonicalTerm above. We maintain a
126		* counter of how many variables we have allocated for each type (var_count),
127		* and a cache of visited nodes (visited).
128		*/
129		Node getCanonicalTerm(
130		TNode n,
131		bool apply_torder,
132		bool doHoVar,
133		std::map<std::pair<TypeNode, uint32_t>, unsigned>& var_count,
134		std::map<TNode, Node>& visited);
135		};
136
137		} // namespace expr
138		} // namespace cvc5
139
140		#endif /* CVC5__EXPR__TERM_CANONIZE_H */