GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/bound_var_manager.h Lines: 9 9 100.0 %
Date: 2021-03-23 Branches: 30 76 39.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bound_var_manager.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 Bound variable manager utility
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__EXPR__BOUND_VAR_MANAGER_H
18
#define CVC4__EXPR__BOUND_VAR_MANAGER_H
19
20
#include <string>
21
#include <unordered_set>
22
23
#include "expr/node.h"
24
25
namespace CVC4 {
26
27
/**
28
 * Bound variable manager.
29
 *
30
 * This class is responsible for constructing BOUND_VARIABLE that are
31
 * canonical based on cache keys (Node). It does this using expression
32
 * attributes on these nodes.
33
 */
34
class BoundVarManager
35
{
36
 public:
37
  BoundVarManager();
38
  ~BoundVarManager();
39
  /**
40
   * Enable or disable keeping cache values. If we keep cache values, then
41
   * the bound variables returned by the methods below are deterministic in the
42
   * lifetime of the NodeManager we are using.
43
   */
44
  void enableKeepCacheValues(bool isEnabled = true);
45
  /**
46
   * Make a bound variable of type tn and name tn, cached based on (T, n),
47
   * where T is an attribute class of the form:
48
   *   expr::Attribute<id, Node>
49
   * This variable is unique for (T, n) during the lifetime of n. If
50
   * this bound variable manager is configured to keep cache values, then
51
   * n is added to the d_cacheVals set and survives in the lifetime of the
52
   * current node manager.
53
   *
54
   * Returns the bound variable.
55
   */
56
  template <class T>
57
9186
  Node mkBoundVar(Node n, TypeNode tn)
58
  {
59
    T attr;
60
9186
    if (n.hasAttribute(attr))
61
    {
62
1523
      Assert(n.getAttribute(attr).getType() == tn);
63
1523
      return n.getAttribute(attr);
64
    }
65
15326
    Node v = NodeManager::currentNM()->mkBoundVar(tn);
66
7663
    n.setAttribute(attr, v);
67
    // if we are keeping cache values, insert it to the set
68
7663
    if (d_keepCacheVals)
69
    {
70
1722
      d_cacheVals.insert(n);
71
    }
72
7663
    return v;
73
  }
74
  /** Same as above, with a name for the bound variable. */
75
  template <class T>
76
  Node mkBoundVar(Node n, const std::string& name, TypeNode tn)
77
  {
78
    Node v = mkBoundVar<T>(n, tn);
79
    setNameAttr(n, name);
80
    return v;
81
  }
82
  //---------------------------------- utilities for computing Node hash
83
  /** get cache value from two nodes, returns SEXPR */
84
  static Node getCacheValue(TNode cv1, TNode cv2);
85
  /** get cache value from two nodes and a size_t, returns SEXPR */
86
  static Node getCacheValue(TNode cv1, TNode cv2, size_t i);
87
  /** get cache value, returns a constant rational node */
88
  static Node getCacheValue(size_t i);
89
  /** get cache value, return SEXPR of cv and constant rational node */
90
  static Node getCacheValue(TNode cv, size_t i);
91
  //---------------------------------- end utilities for computing Node hash
92
 private:
93
  /** Set name of bound variable to name */
94
  static void setNameAttr(Node v, const std::string& name);
95
  /** Whether we keep cache values */
96
  bool d_keepCacheVals;
97
  /** The set of cache values we have used */
98
  std::unordered_set<Node, NodeHashFunction> d_cacheVals;
99
};
100
101
}  // namespace CVC4
102
103
#endif /* CVC4__EXPR__BOUND_VAR_MANAGER_H */