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