GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/term_canonize.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file term_canonize.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief Utilities for constructing canonical terms.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__EXPR__TERM_CANONIZE_H
18
#define CVC4__EXPR__TERM_CANONIZE_H
19
20
#include <map>
21
#include "expr/node.h"
22
23
namespace CVC4 {
24
namespace expr {
25
26
/** TermCanonize
27
 *
28
 * This class contains utilities for canonizing terms with respect to
29
 * free variables (which are of kind BOUND_VARIABLE). For example, this
30
 * class infers that terms like f(BOUND_VARIABLE_1) and f(BOUND_VARIABLE_2)
31
 * are effectively the same term.
32
 */
33
class TermCanonize
34
{
35
 public:
36
  TermCanonize();
37
6061
  ~TermCanonize() {}
38
39
  /** Maps operators to an identifier, useful for ordering. */
40
  int getIdForOperator(Node op);
41
  /** Maps types to an identifier, useful for ordering. */
42
  int getIdForType(TypeNode t);
43
  /** get term order
44
   *
45
   * Returns true if a <= b in the term ordering used by this class. The
46
   * term order is determined by the leftmost position in a and b whose
47
   * operators o_a and o_b are distinct at that position. Then a <= b iff
48
   * getIdForOperator( o_a ) <= getIdForOperator( o_b ).
49
   */
50
  bool getTermOrder(Node a, Node b);
51
  /** get canonical free variable #i of type tn */
52
  Node getCanonicalFreeVar(TypeNode tn, unsigned i);
53
  /** get canonical term
54
   *
55
   * This returns a canonical (alpha-equivalent) version of n, where
56
   * bound variables in n may be replaced by other ones, and arguments of
57
   * commutative operators of n may be sorted (if apply_torder is true). If
58
   * doHoVar is true, we also canonicalize bound variables that occur in
59
   * operators.
60
   *
61
   * In detail, we replace bound variables in n so the the leftmost occurrence
62
   * of a bound variable for type T is the first canonical free variable for T,
63
   * the second leftmost is the second, and so on, for each type T.
64
   */
65
  Node getCanonicalTerm(TNode n,
66
                        bool apply_torder = false,
67
                        bool doHoVar = true);
68
69
 private:
70
  /** the number of ids we have allocated for operators */
71
  int d_op_id_count;
72
  /** map from operators to id */
73
  std::map<Node, int> d_op_id;
74
  /** the number of ids we have allocated for types */
75
  int d_typ_id_count;
76
  /** map from type to id */
77
  std::map<TypeNode, int> d_typ_id;
78
  /** free variables for each type */
79
  std::map<TypeNode, std::vector<Node> > d_cn_free_var;
80
  /**
81
   * Map from each free variable above to their index in their respective vector
82
   */
83
  std::map<Node, size_t> d_fvIndex;
84
  /**
85
   * Return the range of the free variable in the above map, or 0 if it does not
86
   * exist.
87
   */
88
  size_t getIndexForFreeVariable(Node v) const;
89
  /** get canonical term
90
   *
91
   * This is a helper function for getCanonicalTerm above. We maintain a
92
   * counter of how many variables we have allocated for each type (var_count),
93
   * and a cache of visited nodes (visited).
94
   */
95
  Node getCanonicalTerm(TNode n,
96
                        bool apply_torder,
97
                        bool doHoVar,
98
                        std::map<TypeNode, unsigned>& var_count,
99
                        std::map<TNode, Node>& visited);
100
};
101
102
}  // namespace expr
103
}  // namespace CVC4
104
105
#endif /* CVC4__EXPR__TERM_CANONIZE_H */