1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
|
/******************************************************************************
* 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.
* ****************************************************************************
*
* A let binding.
*/
#include "cvc5_private.h"
#ifndef CVC5__PRINTER__LET_BINDING_H
#define CVC5__PRINTER__LET_BINDING_H
#include <vector>
#include "context/cdhashmap.h"
#include "context/cdlist.h"
#include "expr/node.h"
namespace cvc5 {
/**
* A flexible let binding class. This class provides functionalities for
* printing letified terms. A simple use case is the following for Node n
* and LetBinding lbind:
* ```
* std::vector<Node> letList;
* lbind.letify(n, letList);
* ```
* Now, letList contains a list of subterms of n that should be letified based
* on the threshold value passed to this class where a value n>0 indicates that
* terms with n or more occurrences should be letified.
*
* The above is equivalent to:
* ```
* std::vector<Node> letList;
* lbind.pushScope();
* lbind.process(n);
* lbind.letify(letList);
* ```
* In fact, multiple terms can be passed to calls to process, in which case the
* counting is cumulative.
*
* All quantified formulas are treated as black boxes. This class can be used
* to letify terms with quantifiers, where multiple calls to pushScope /
* popScope can be used. In particular, consider:
* ```
* std::vector<Node> letList1;
* lbind.letify(n1, letList1);
* std::vector<Node> letList2;
* lbind.letify(n2, letList2);
* ...
* lbind.popScope();
* lbind.popScope();
* ```
* In a typical use case, n2 is the body of a quantified formula that is a
* subterm of n1. We have that letList2 is the list of subterms of n2 that
* should be letified, assuming that we have already have let definitions
* given by letList1.
*
* Internally, a let binding is a list and a map that can be printed as a let
* expression. In particular, the list d_letList is ordered such that
* d_letList[i] does not contain subterm d_letList[j] for j>i.
* It is intended that d_letList contains only unique nodes. Each node
* in d_letList is mapped to a unique identifier in d_letMap.
*
* Notice that this class will *not* use introduced let symbols when converting
* the bodies of quantified formulas. Consider the formula:
* (let ((Q (forall ((x Int)) (= x (+ a a))))) (and (= (+ a a) (+ a a)) Q Q))
* where "let" above is from the user. When this is letified by this class,
* note that (+ a a) occurs as a subterm of Q, however it is not seen until
* after we have seen Q twice, since we traverse in reverse topological order.
* Since we do not traverse underneath quantified formulas, this means that Q
* may be marked as a term-to-letify before (+ a a), which leads to violation
* of the above invariant concerning containment. Thus, when converting, if
* a let symbol is introduced for (+ a a), we will not replace the occurence
* of (+ a a) within Q. Instead, the user of this class is responsible for
* letifying the bodies of quantified formulas independently.
*/
class LetBinding
{
using NodeList = context::CDList<Node>;
using NodeIdMap = context::CDHashMap<Node, uint32_t>;
public:
LetBinding(uint32_t thresh = 2);
/** Get threshold */
uint32_t getThreshold() const;
/**
* This updates this let binding to consider the counts for node n.
*/
void process(Node n);
/**
* This pushes a scope, computes the letification for n, adds the (new) terms
* that must be letified in this context to letList.
*
* Notice that this method does not traverse inside of closures.
*
* @param n The node to letify
* @param letList The list of terms that should be letified within n. This
* list is ordered in such a way that letList[i] does not contain subterm
* letList[j] for j>i.
*/
void letify(Node n, std::vector<Node>& letList);
/**
* Same as above, without a node to letify.
*/
void letify(std::vector<Node>& letList);
/** Push scope */
void pushScope();
/** Pop scope for n, reverts the state change of the above method */
void popScope();
/**
* @return the identifier for node n, or 0 if it does not have one.
*/
uint32_t getId(Node n) const;
/**
* Convert n based on the state of the let binding. This replaces all
* letified subterms of n with a fresh variable whose name prefix is the
* given one.
*
* @param n The node to convert
* @param prefix The prefix of variables to convert
* @param letTop Whether we letify n itself
* @return the converted node.
*/
Node convert(Node n, const std::string& prefix, bool letTop = true) const;
private:
/**
* Compute the count of sub nodes in n, store in d_count. Additionally,
* store each node in the domain of d_count in an order in d_visitList
* such that d_visitList[i] does not contain sub d_visitList[j] for j>i.
*/
void updateCounts(Node n);
/**
* Convert a count to a let binding.
*/
void convertCountToLet();
/** The dag threshold */
uint32_t d_thresh;
/** An internal context */
context::Context d_context;
/** Visit list */
NodeList d_visitList;
/** Count */
NodeIdMap d_count;
/** The let list */
NodeList d_letList;
/** The let map */
NodeIdMap d_letMap;
};
} // namespace cvc5
#endif
|
